文献

J-GLOBAL ID：202202215159374629   整理番号：22A0691448

メタにおけるマイクロカーネルIPCへの形式的検証の適用【JST・京大機械翻訳】

Applying formal verification to microkernel IPC at meta

著者 (5件)： Carbonneaux Quentin (Meta, France) ,  Zilberstein Noam (Meta, USA / Cornell University, USA) ,  Klee Christoph (Meta, USA) ,  O’Hearn Peter W. (Meta, UK / University College London, UK) ,  Zappa Nardelli Francesco (Meta, France)
資料名： ACM Proceedings  (ACM Proceedings)
号： CPP 2022  ページ： 116-129  発行年： 2022年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： Coq証明支援における同時分離論理の実装であるIrisを用いて,開発中のオペレーティングシステムにおけるプロセス間通信に用いる2つの待ち行列データ構造を検証した。著者らの動機は2倍である。第1に,著者らは,多数の修正を受けた産業コードの繊細な部分における信頼を押し上げるために,形式的検証を活用することを望んだ。第2に,著者らは,著者らの産業設定において最先端の形式的検証ツールを適用するコスト便益トレードオフに関する情報を得ることを狙った。両フロントにおいて,著者らの努力は成功であった。検証努力は,待ち行列アルゴリズムが,クライアントコードにおけるバグと同様に,正しくて,4つのアルゴリズム簡素化を開示することを証明した。単純化は,2つのメモリ障壁の除去,1つの原子負荷,および1つのボアランチェックを含み,全てOSの性能に敏感な部分である。冗長なボレアチェックは,複数のデバイスドライバにおける非初期記憶の意図しない使用を明らかにし,それは固定されている。証明作業は,Irisとの事前の慣習性のない技術者によって,何年も,人月で完了した。これらの知見は,Metaでの検証の更なる使用を推進している。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  記憶装置 ,  待ち行列 ,  オペレーティングシステム ,  簡素化 ,  冗長性 ,  データ構造 ,  トレードオフ ,  ソフトウェア障害 ,  *検証 ,  プロセス間交信 ,  *マイクロカーネル
準シソーラス用語： *形式的検証 ,  便益 ,  デバイスドライバ , 【Automatic Indexing@JST】

著者キーワード (5件)： 円形待ち行列 ,  並行性 ,  プログラム検証 ,  分離論理 ,  システム

分類 (2件)： 計算機システム開発  (JD02010R) ,  オペレーティングシステム  (JD03020J)

タイトルに関連する用語 (3件)： マイクロカーネル ,  IPC ,  形式的検証