以下は、２０１７年版の perfbook の１２章 Formal Verification, 12.3 Axiomatic Approaches 他のkanda.motohiro@gmail.com による訳です。perfbook の訳の他の部分は、親文書を参照。
１２．３ 公理論的アプローチ
PPCMEM ツールは、リスト１２．２８に示す、有名な、独立なライトを独立に読む「independent reads of
independent writes」(IRIW)リトマス試験を解くことができますが、そのためには、１４時間以上のCPU 時間が必要で、１０GB 以上の状態空間を生成します。とは言っても、この状況は、PPCMEM の出現前と比べると大きな改善です。当時は、この問題を解くためには、レファレンスマニュアルを何冊も熟読し、証明を試み、エキスパートと議論する必要があり、それでも最終的な解答に確信がおけませんでした。１４時間は長く思えるかもしれませんが、何週間、時には何ヶ月と比べるとずっと短いです。
しかし、リトマス試験の簡単さを考えると、必要な時間は少し驚くべきものです。それは、二つの独立した変数にストアする二つのスレッドと、これら二つの変数から逆の順序でロードする他の二つのスレッドしか持ちません。二つのロードするスレッドが、二つのストアの順序について意見が違うとアサーションが発火します。このリトマス試験は、標準的なメモリオーダーのリトマス試験から見ても、単純です。
消費される時間と空間が大きい一つの理由は、PPCMEM がトレースベースの完全な状態空間探索をするからです。それは、PPCMEM がアーキテクチャのレベルでの、全ての可能なオーダーとイベントの組み合わせを全て生成して評価する必要があることを意味します。このレベルでは、ロードもストアも、イベントとアクションの華々しい連続に対応し、完全に探索されなくてはいけない状態空間をとても大きくする結果となります。それはメモリとCPUの消費を大きくします。
もちろん、トレースの多くは互いにとても似ています。それは、似たトレースを一つとして扱うアプローチが性能を上げるだろうことを示唆します。そのようなアプローチの一つが、Alglave たちの公理論的アプローチ[AMT14] です。それは、メモリモデルを表現する公理の集合を作成し、次に、リトマス試験を、この公理の集合から証明あるいは反証することができるかもしれない理論に変換します。こうしてできたツールは、「herd」と呼ばれ、便利なことに、PPCMEM と同じリトマス試験を入力に取ります。それには、リスト１２．２８に示す IRIW リトマス試験も含まれます。
PPCMEM がIRIW を解くのに１４時間のCPU を必要とする一方、 herd はそれを１７ミリ秒で行います。それは、６桁以上の高速化です。とは言え、問題はその性質から指数的なので、より大きな問題に対しては、 herd が指数的に低速化すると思うのが適切です。そしてこれは実際に起きることです。例えば、リスト１２．２９に示すように、書き込みCPUごとに、さらに４つのライトを加えると、 herd は 50,000 以上のファクターで低速化し、１５分以上の CPU 時間を必要とします。スレッドを加えても、同様に、指数的な低速化が起きます[MS14]。
指数的な性質にもかかわらず、PPCMEM と herd はいずれも、鍵となる並列アルゴリズムのチェックに大いに役立つことを示してきました。それには、 x86 システムでの queued-lock handoff も含まれます。herd ツールの弱点は、１２．２．４節に書いた PPCMEM のそれに似ています。PPCMEM と herd ツールの結果が異なる、詳細不明な（しかしとても現実の）ケースがいくつかあります。２０１４年末の時点で、これらの不一致を解決する作業が続行中でした。
より長期的には、公理論的アプローチが、より高レベルのソフトウェア作品を記述する公理を取り入れることが期待されます。それは、潜在的に、より大きなソフトウェアシステムの公理論的検証を可能とするでしょう。他の案としては、ブール論理の公理に仕事をさせることです。それについては、次の節で。
１２．４ SAT ソルバ
有限のループと再帰を持つ有限のプログラムは全て、論理式に変換できます。その式は、入力に対するそのプログラムのアサーションを表現するかもしれません。そのような論理式が与えられた時に、入力の何らかの組み合わせが、アサーションの一つを発火させることが可能かを知ることはとても興味深いでしょう。もし論理式がブール変数の組み合わせで表現されている場合、これは単純に、SAT、別名、satisfiability problem 充足可能性問題です。SAT ソルバは、ハードウェアの検証に大いに使われており、それがその大きな進歩を動機付けてきました。１９９０年代初期の世界的クラスの SAT ソルバは、１００の独立したブール変数を持つ論理式を扱うことができたかもしれません。しかし、２０１０年代初期では、百万変数の SAT ソルバが直ちに利用可能です[KS08]。
さらに、SAT ソルバのフロントエンドプログラムは、C コードを自動的に論理式に翻訳することができます。アサーションを考慮に入れ、配列境界の誤りなどのエラー条件に対して、アサーションを生成します。その一つの例は、C bounded model checker あるいは cbmc です。これは、多くの Linux ディストリビューションの一部として利用可能です。このツールはとても使うのが簡単です。 cbmc test.c をすれば、test.c を検証するのに十分です。この使いやすさは、とても重要です。これは、形式的検証が回帰テストフレームワークに組み込まれるための扉を開くからです。それに対して、特定用途のための言語への自明でない翻訳を必要とする伝統的なツールは、設計時の検証に限られます。
より最近では、並列コードを扱う SAT ソルバが現れました。これらのソルバは、入力コードを、single static assignment (SSA) 形式に変換し、その後に全ての許されるアクセスオーダーを生成することで動作します。このアプローチは有望そうに見えます。しかし、実際にどの程度うまく行くかはまだわかりません。一つの、期待の持てるしるしは、２０１６年に、cbmc を、Linux-kernel RCU に適用した研究です[LMKM16, Roy17a]。この研究は、RCU の最小限の構成を使い、少数のスレッドでいくつかのシナリオを検証しました。しかしそれでも、 Linux-kernel C コードを消化することに成功し、有効な結果を生成しました。C コードから生成された論理式は、９千万の変数を持ち、４５億の句を持ち、何十GBものメモリを占有し、SAT ソルバが正しい結果を生成するまでに８０時間のCPU 時間を必要としました。
しかし、Linux カーネルハッカーが、彼あるいは彼女のコードが自動的に検証されたという主張に対して、懐疑的になるのは無理もないかもしれません。そのような疑いに対処する一つの方法は、問題のコードの、バグが挿入されたバージョンを提供することです。もし形式的検証ツールが全てのバグを見つけたら、ハッカーはそのツールの能力について、より信頼を持つでしょう。そしてまさにこれが、２０の変化形ブランチを持つ git アーカイブがある理由です。それぞれのブランチは、潜在的に、Linux-kernel RCU に挿入されたバグを持ちます[McK17]。形式的検証ツールをお持ちの方はどなたでも、そのツールをこの検証への挑戦のセットに対して試すよう、心からご招待します。
現在、 cbmc は挿入されたいくつかのバグを見つけることができます。しかしそれは、RCU のメンテナがまだ知らないバグを見つけることはできないでいます。とは言っても、いつの日か SAT ソルバが並列コードの同時実行バグを見つけるのに役に立つだろうと期待する理由はいくつかあります。
１２．５ ステートレスモデルチェッカー
前の節で述べた SAT ソルバアプローチは、とても便利でパワフルです。しかし、状態を含む全ての可能な実行を完全に追跡することは、かなりのオーバーヘッドを起こします。実際、メモリとCPU時間のオーバーヘッドは、実質的に検証できるプログラムの大きさを厳しく制限します。これは、より不正確なアプローチは、より大きなプログラムのバグを見つけることができるだろうかという疑問を起こさせます。
この疑問に対する判決はまだ出ていませんが、Nidhugg [LSLK14]のような、ステートレスモデルチェッカーは、ある場合には、より大きなプログラムを扱ってきました[KS17b]。さらに、Nidhugg は、ある Linux-kernel RCU 検証シナリオでは、cbmc に比べて、１桁以上速かったです。もちろん、Nidhugg の速さとスケーラビリティの優位性は、それが、データの非決定論を扱わない事実に関連しています。しかしこれは、前記の特定の検証シナリオでは、重要な要素ではありませんでした。
しかし、cbmc と同じく、Nidhugg は、RCU のメンテナがまだ知らないバグを見つけることはできないでいます。しかし、それは、Linux-kernel RCU の一つの歴史的なバグが、メンテナが考えていたのとは違うコミットで直されたことを示すことができました。これは、いつの日か、Nidhugg のようなステートレスモデルチェッカーが並列コードの同時実行バグを見つけるのに役に立つだろうという期待をいくぶんか増すものです。
１２．６ 形式的回帰テスト？
いくつかの場合に、形式的検証は役に立つことを示してきました。しかし、重要な未解決問題は、ハードコアの形式的検証が、Linux カーネルのような複雑な並列実行コードベースのための自動回帰テストスイートに含まれるようなことがあるだろうかということです。Linux-kernel SRCU に対する proof of concept は既にあります[Roy17a] が、このテストは、RCU 実装の中でも最も単純なものの小さな一部分に対するものです。そして、常に変化する Linux カーネルに追いついていくのが難しいことを証明しました。なので、形式的検証を、Linux カーネルの回帰テストの一級のメンバーとして取り入れるためには何が必要だろうかと問うことは意味があります。
以下の一覧は良い出発点です[McK15a, slide 34]。
１ 必要な翻訳は全部自動化されています。
２ 環境（メモリオーダリングを含む）は正しく扱われなくてはいけません。
３ メモリとCPU オーバーヘッドは許容可能な程度、ほどほどでなくてはいけません。
４ バグの位置を示すような具体的な情報が提供されなくてはいけません。
５ スコープにおいて、ソースコードと入力を超える情報はほどほどでなくてはいけません。
６ 見つかったバグは、コードの利用者に関連していなくてはいけません。
この一覧は増えていきます。しかし、Richard Bornat の格言よりはいくらか控えめです。「形式的検証の研究者は、開発者が書くコードを、開発者が書く言語で、そのコードが動いているその環境で、開発者がコードを書くのと同時に、検証するべきです。」以下の節は上記要件のそれぞれを議論します。その後、いくつかのツールがどの程度この要件を満たすかについてのスコアボードを示す節があります。
１２．６．１ 自動翻訳
Promela と spin は貴重な設計の補助ですが、あなたはご自分の C 言語のプログラムを形式的に回帰テストする必要があるならば、あなたはご自分のコードを再度、検証したい時に毎回、手でそれを Promela に翻訳しなくてはいけません。あなたのコードが Linux に含まれるなら、それは６０日から９０日ごとにリリースされるので、毎年、あなたは４から６回、手で翻訳が必要でしょう。時がすぎるにつれて、人の誤りは忍び込みます。ということは、検証はソースコードと一致せず、検証は役に立たなくなることを意味します。繰り返して検証をするためには、明らかに、形式的検証ツールがあなたのコードを直接入力とするか、あるいは、検証のために必要な形式にあなたのコードを自動的に翻訳するしかけが必要です。
PPCMEM と herd は、理論的には、アセンブリ言語と C++ コードを直接、入力できます。しかし、これらのツールはとても小さなリトマス試験に対してしか動きません。ということは普通は、あなたは、手で、あなたのメカニズムのコアを抽出する必要があることを意味します。Promela と spin と同様に、PPCMEM と herd はとても便利ですが、回帰スイートにはあまり向いていません。
それに対して、cbmc と Nidhugg は、かなりの（まだ、とても制限があるといえ）大きさの C プログラムを入力できます。そしてそれらの能力が向上し続けるとするなら、回帰スイートへの素晴らしい追加となることもあるでしょう。
C コードを入力とすることの一つの欠点は、それがコンパイラが正しいことを前提とすることです。別のアプローチは、C コンパイラが生成したバイナリを入力とすることです。そうすれば、関連するどんなコンパイラのバグも説明できます。このアプローチは、多くの検証の研究で使われてきました。多分、最も有名なのは、SEL4 プロジェクト [SM13] です。
クイッククイズ １２．２７
SEL4 プロジェクトで使われた多くの検証器の開拓者的な性質を考えると、なぜこの章で、それらをもっと詳しく述べないのですか？
しかし、ソースあるいはバイナリから直接、検証をすることは、人間の翻訳誤りを除く利点があります。それは信頼できる回帰テストにとって致命的に重要です。
１２．６．２ 環境
形式的検証ツールが、その環境を正しくモデリングすることは致命的に重要です。メモリモデルの欠落は、一つの、とてもよくある例です。Promela/spin を含むとても多くの検証ツールは sequential 一貫性に制限されています。１２．１．４．６節で述べた、QRCU の経験談は、重要な注意を喚起するでしょう。
Promela と spin は、sequential 一貫性を前提とします。それは、１５章で見るように、現代的計算機システムにとっては、良い合致ではありません。それに対して、PPCMEM と herd の素晴らしい利点の一つは、それらが多くのCPUファミリーのメモリモデルの詳細なモデリングが可能なことです。それには、x86, ARM, Power, そして、 herd の場合には、 Linux カーネルメモリモデルのプロトタイプまでも含まれます [AMM + 17a, AMM + 17b]。
cbmc と Nidhugg ツールはメモリモデルを選択するいくらかの機能を提供します。しかし、PPCMEM と herd ほどの多様性はありません。しかし、時が経つにつれ、より大きなスケールのツールがより多様なメモリモデルを採用することもありえるでしょう。
さらに先を考えると、形式的検証ツールが、I/O [MDR16a]を含むことはとても役に立つでしょう。しかしそれが起きるのはずいぶん先のことでしょう。
１２．６．３ オーバーヘッド
ほとんど全てのハードコア形式的検証ツールは指数的な性質を持ちます。しかし、その程度には差があります。
PPCMEM は、その設計思想により、最適化されていません。それは、問題のメモリモデルが実際に正確に表現されていることをより確実に保証するためです。herd ツールはよりアグレッシブに最適化をします。なので、１２．３節で述べたように、PPCMEM と比べて何桁も速いです。とは言っても、PPCMEM も herd も、大きなコードのボディではなくとても小さなリトマス試験を対象とします。
それに対して、Promela/spin, cbmc, そして Nidhugg は（いくらか）より大きなコードのボディのために設計されています。Promela/spin は、 Curiosity rover のファイルシステムを検証することに使われました [GHH + 14]。そして、以前に述べたように、 cbmc と Nidhugg は Linux カーネル RCU に適用されました。
ヒューリスティクスの進歩が、過去の四半世紀と同じ速度で続くならば、形式的検証のオーバーヘッドの大きな削減を期待できるでしょう。とは言っても、組み合わせ爆発はやはり組み合わせ爆発なので、ヒューリスティクスの進歩があってもなくても、検証できるプログラムの大きさは厳しく制限されるでしょう。
しかし、組み合わせ爆発の裏面は、マケドニア王 Philip II の普遍の格言です。「分割して統治せよ」。もし大きなプログラムを分割することができ、部品が検証できれば、その結果は、組み合わせ爆縮、combinatorial implosion [McK11d]です。分割をする一つの自然な場所は、API 境界です。例えば、ロックプリミティブの。検証が一つ通れば、ロック実装が正しいことを検証でき、もう一つ通れば、ロックAPI の使い方が正しいことを検証できます。
このアプローチの、性能利点は、Linux カーネルメモリモデルを使って示されました[AMM + 17a, AMM + 17b]。このモデルは spin_lock() と spin_unlock() プリミティブを提供します。しかしこれらのプリミティブは、リスト１２．３０(C-SB+l-o-o-u+l-o-o-*u.litmus と C-SB+l-o-o-u+l-o-o-u*-C.litmus)が示すように、cmpxchg_acquire() と smp_store_release() を使ってエミュレートすることもできます。表１２．３は、モデルの spin_lock() と spin_unlock() を使った時とこれらのプリミティブをリストに示すようにエミュレートした時の、性能とスケーラビリティを比べます。その差はかなりなものです。４プロセスで、このモデルは、エミュレーションよりも２桁以上、速いです！
クイッククイズ １２．２８
リスト１２．３０の２８行目で、なぜ、わざわざ、独立の filter コマンドを使うのですか？exists 句に、単純に条件を追加したらどうですか？そして、cmpxchg_acquire() でなく、xchg_acquire() を使うほうが、単純でないですか？
もちろん、ツールが自動的に大きなプログラムを分割し、部品を検証し、さらに部品の組み合わせを検証してくれるととても便利です。当分は、大きなプログラムの検証はかなりの人手の介入が必要でしょう。この介入は、可能ならばスクリプティングで補助され、リリース毎に繰り返して検証を実行することがより安定して行えるようになるでしょう。最終的には、継続的統合に適したように行えると良いでしょう。
いずれの場合も、形式的検証の能力は、時とともに増加し続けることが期待できます。
１２．６．４ バグを位置づける
ソフトウェア作品はどんな大きさのものでも、バグを持ちます。なので、バグがあるかないかだけを報告する形式的検証ツールはあまり便利ではありません。必要なのは、少なくても、バグがある場所と、そのバグの性質についてのなんらかの情報をくれるツールです。
cbmc の出力は、ソースコードへのトレースバックマッピングを含みます。これは、Promela/spin と、 Nidhugg の出力も同じです。もちろん、このトレースバックはとても長いことがあります。しかし、ほとんど常に、それを解析するのは価値のあることです。そうするのは大変かもしれませんが、普通は、古いやり方でバグを見つけるのに比べると、ずっと速く、楽しいです。
１２．６．５ 足場は最小に
昔は、形式的検証の研究者は、ソフトウェアが検証される対象の完全な仕様を要求しました。不幸にも、数学的に厳密な仕様書は、実際のコードよりもずっと大きいことがあり、仕様書のそれぞれの行は、コードの行と同じくらい、バグを含んでいる可能性がありました。コードが仕様書を忠実に実装したことを証明する形式的検証作業は、それら二つの間の、バグからバグへの互換性を証明することになることがあり、それは期待する結果ではないでしょう。
さらに悪いことに、Linux カーネル RCU を含む多くのソフトウェア作品の要件は、その性質から言って、経験的です[McK15e, McK15c, McK15d]。この一般的なソフトウェアのタイプにとっては、完全な仕様書は丁寧なフィクションです。
人々は、この状況を見て、実世界のソフトウェア製品に対する形式的検証の全ての望みをあきらめるかもしれません。しかし、できることがたくさんあることがわかりました。例えば、設計とコーディング規則は部分的な仕様として役立つことがあります。コードに含まれるアサーションもそうです。そして、実際、cbmc と Nidhugg のような形式的検証ツールはいずれも、発火する可能性のあるアサーションをチェックします。それらアサーションを、暗黙的な仕様の部分として扱います。しかし、アサーションはコードの一部でもあります。ということは、それは古臭くはなりにくいでしょう。特に、そのコードがストレステストも受けるときはです。
脚注
そして、あなたはご自分のコードを実際にストレステストしますよね？
cbmc ツールは、配列の範囲外参照もチェックします。このように、それを暗黙的に仕様に加えます。
この暗黙的仕様のアプローチは、かなり意味のあることです。あなたが形式的検証を、正しさの完全な証明ではなく、テストのような他の形式の検証とは異なる利点と欠点のセットを持つ代替的な検証の形式として考えているならば、余計にそのとおりです。この観点では、ソフトウェアは常にバグを持ち、どんな種類のどんなツールでも、そのバグを見つける助けになるものはとても良いということです。
１２．６．６ 関連するバグ
バグを見つけて直すのは、もちろん、どんな検証作業でも、そのそもそもの目的です。擬陽性は、明らかに、避けられるべきです。しかし、擬陽性がなくても、バグはたくさんあちこちにあります。
例えば、あるソフトウェア作品が残りちょうど１００のバグを持つとします。それらはそれぞれ、平均で、実行時間１００万年に一度、現れます。さらに、万能の形式的検証ツールが、全ての１００個のバグを見つけ、開発者はそれらを正しく直したとします。このソフトウェア作品の、信頼性はどうなるでしょう？
おそらく驚くべき答えは、信頼性は下がる、です。
これを考えるために、修正の約７％が新しいバグを作り出す[BJ12]という歴史的経験を思い出して下さい。なので、全体での 平均故障間隔(MTBF) 10,000 年を持つバグを１００個直した結果、７つのバグが新たにできたでしょう。歴史的な統計は新しいバグそれぞれは 70,000 年よりずっと短い MTBF を持つだろうことを示します。その結果、これらの新しい７つのバグの全体での MTBF は間違いなく 10,000 年よりずっと小さいことを示唆します。これはつまり、善意で行なった元の１００個のバグの修正が、ソフトウェア全体の MTBF を実際には下げたことを意味します。
クイッククイズ １２．２９
既知のバグの MTBF が、まだ見つかっていないバグの MTBF の良い推定になるのはどうしてわかりますか？
クイッククイズ １２．３０
でも、形式的検証ツールは、直ちに、修正によって導入された全てのバグを見つけるはずですよね。ならばなぜこれが問題ですか？
また、平均で毎日一回失敗する１つのバグと、それぞれ１００万年に一回失敗する９９の他のバグを持つ別のソフトウェア作品を想像しましょう。形式的検証ツールが、９９個の、１００万年のバグを見つけ、でも１日のバグを見つけられなかったとします。見つかった９９個のバグを直すのは、時間と努力が必要で、信頼性を少し下げる可能性があり、そして直近の問題である、不都合ともしかするとそれよりずっと困ったことを引き起こしている毎日の失敗には全く何も寄与しません。
なので、選択的に、最も問題となるバグを見つける検証ツールがあるのが最適でしょう。
これは要求し過ぎと思われるかもしれませんが、ソフトウェアの信頼性を実際に上げようとするならば、これこそが本当に必要なことです。
１２．６．７ 形式的回帰スコアボード
表１２．４は、大まかですが役に立つ、この章で紹介した形式的検証ツールのスコアボードです。短い波長は長いものより良いことを示します。
Promela は手作業の翻訳が必要で、sequential 一貫性だけをサポートします。なのでその最初の２つのセルは赤です。それはほどほどのオーバーヘッド（いずれにしても、形式検証としては）を持ち、トレースバックを提供します。なので、次の２つのセルは黄です。手作業の翻訳が必要ですが、Promela はアサーションを自然な方法で扱うので、５つ目のセルは緑です。
PPCMEM はそれがサポートするリトマス試験の大きさが小さいために、通常は手作業の翻訳が必要です。なので、最初のセルは橙です。それは複数のメモリモデルを扱います。なので、２つ目のセルは緑です。そのオーバーヘッドはとても高いです。なので３つ目のセルは赤です。それは操作の間の関係のグラフィカル表示を提供します。それはトレースバックに比べると役に立ちませんが、それでもとても便利なので、４つ目のセルは黄です。それは exists 句を作る必要があり、プロセス間のアサーションができないので、５つ目のセルも黄です。
herd ツールは、PPCMEM と同様の大きさの制限を持ちます。なので herd の最初のセルも橙です。それは多様なメモリモデルをサポートするので、２つ目のセルは青です。それはほどほどのオーバーヘッドを持つので、３つ目のセルは黄です。そのバグの位置づけとアサーション能力はとても、PPCMEM のそれらに似ているので、herd の次の２つのセルも黄です。
cbmc ツールは、C コードを直接入力します。なので、最初のセルは青です。それはいくつかのメモリモデルをサポートするので、２つ目のセルは黃です。それはほどほどのオーバーヘッドを持つので、３つ目のセルは黄です。しかし、SAT ソルバの性能は改善し続けるでしょう。それはトレースバックを提供するので、４つ目のセルは緑です。それは C コードから直接アサーションを得るので、５つ目のセルは青です。
Nidhugg も、C コードを直接入力します。なので、最初のセルは同様に青です。それはわずかのメモリモデルをサポートするだけなので、２つ目のセルは橙です。そのオーバーヘッドはとても小さい（形式検証としては）ので、３つ目のセルは緑です。それは C コードから直接アサーションを得るので、５つ目のセルは青です。
さて、６つ目と最後の行はどうでしょう？これらのツールが正しいバグを実際に見つけるかを判断するのはまだ早すぎます。なので、それは全部、黃で疑問符つきです。
クイッククイズ １２．３１
表１２．４のスコアボードにおいて、テストはどのように見えますか？
繰り返しますが、この表は、これらのツールを、回帰テストで使うことに関して評価することに注意下さい。それらの多くが、回帰テストには向いていないことは、それらが役に立たないことを全く意味しません。実際、それらの多くは、何度も、それらの価値を証明してきました。回帰テストのためでは無かったとしても。
脚注
いくらもあるうちの一つの例を上げれば、Promela はなんと、 Curiosty Rover のファイルシステムを検証するために使われました。あなたの形式的検証ツールは、火星の Rover で使われましたか？
クイッククイズの答え
クイッククイズ １２．２７
SEL4 プロジェクトで使われた検証器がとても強力であることに疑いはありません。しかし、SEL4 が、シングルCPUプロジェクト以外のものでなくなったのは、わずかに、ここ２，３年のことです（２０１７年時点で）。
そして、SEL4 がマルチプロセッサ能力を獲得しつつあるとしても、現在ではそれはとても粗い粒度のロック、Linux カーネルの古い Big Kernel Lock (BKL) に似たものを使っています。
並列プログラミングの本に、SEL4 の検証器を加えることが意味を持つ日が来ると良いですが、不幸なことに、まだ今はそうではありません。
クイッククイズ １２．２８
filter 句は、exists 句に比べて、処理のより早い段階で実行を破棄するように、herd ツールに指示します。それは大きな高速化をもたらします。
xchg_acquire() については、このアトミック操作は、ロック確保が成功しても失敗しても、ライトをします。それは、xchg_acquire() を使うモデルは、cmpxchg_acquire() を使うモデルよりもより多くの操作を持つことを意味します。後者は確保に失敗した場合はライトをしません。より多くのライトは、表 E.2 が示すように、(C-SB+l-o-o-u+l-o-o-*u.litmus, C-SB+l-o-o-u+l-o-o-u*-C.litmus, C-SB+l-o-o-u+l-o-o-u*-CE.litmus, C-SB+l-o-o-u+l-o-o-u*-X.litmus, そして C-SB+l-o-o-u+l-o-o-u*-XE.litmus)より多くの組み合わせ爆発を意味します。この表は明らかに、cmpxchg_acquire() が、xchg_acquire() より高性能で、filter 句の使用が、exists 句の使用より高性能なことを示します。
クイッククイズ １２．２９
わかりません。でも、かまいません。
これを考えるために、７％という数字は、挿入され、最終的に見つけられたバグに対してだけ適用されることに注意下さい。それは必然的に、決して見つからなかった、挿入されたバグは無視します。なので、既知のバグの MTBF 統計は、挿入され、最終的に見つけられたバグの良い近似となるでしょう。
この節全体の鍵となる点は、私達は、実際には決して表面化しないそれ以外のバグに比べて、使用者に不都合をもたらすバグに、より注意を払うべきだということです。これはもちろん、私達がまだ使用者に不都合をもたらしていないバグを完全に無視するべきだと言っているのではありません。私達は自分の作業を適切に優先度付けて、最も重要で緊急のバグをまず直すべきだということです。
クイッククイズ １２．３０
それは問題です。実世界の形式的検証ツールは、（形式的検証の騒々しい賛同者の空想の中にだけ存在するものとは違って）万能ではないからです。なので、ある種類のバグしか見つけることはできません。いくらもあるうちの一つの例を上げれば、形式的検証ツールは欠落したアサーションに対するバグ、あるいは、同じことですが、欠落した仕様の部分に対するバグを見つけることはほぼないでしょう。
クイッククイズ １２．３１
それは、全部、青でしょう。可能な例外は、３つ目の行（オーバーヘッド）で、起きそうにないバグを見つけるためのテストが難しいために、減点されるかもしれません。
一方、起きそうにないバグはしばしば、どうでもよいバグでもありますから、場合によります。
多くのことは、あなたのインストールベースの大きさに依存します。もしあなたのコードが（例えば）たったの 10,000 システムで動くことしかありえないならば、マーフィーは実際にとても素敵な人物でしょう。失敗する可能性のあることは必ず起きる。いずれは。たぶん、地質学的な時間の間には。
しかしあなたのコードが２００億のシステムで動いているならば、マーフィーは本当のばかものかもしれません。失敗する可能性のあることは必ず起きる。そしてとてもすぐに！！！
初出
[MS14] Paul E. McKenney and Alan Stern. Axiomatic validation of memory barriers and atomic instructions, August 2014.
http://lwn.net/Articles/608550/
以上