perfbook １２章の訳

以下は、perfbook の１２章の kanda.motohiro@gmail.com による全訳です。perfbook の訳の他の部分は、親文書を参照。

１２章 形式的検証

並列アルゴリズムは書くのが大変で、デバッグするのはさらに大変です。テストは、重要ですが、不十分です。致命的な競合条件はとても起きる確率が低いことがあるからです。正しさの証明は重要ですが、結局、元のアルゴリズムと同じくらい人間の誤りに左右されます。さらに、正しさの証明は、あなたの前提の誤り、要件の不足、元となるソフトウエアとハードウエアプリミティブの誤解を検出することは無理です。そもそも、あなたが証明を作ろうとしていない部分についての誤りは見つけられません。ということは、形式的方法は、テストの代わりとは決してならないということです。しかし、それでも形式的方法をあなたの検証道具箱に加えるのは価値のあることです。

なんとかして、すべての競合条件を位置づけることのできるツールがあったら、とても便利でしょう。そのようなツールはいくつもあります。例えば、 Promela 言語とそのコンパイラ Spin です。この章で説明します。１２．１節は、Promela と Spin の紹介です。１２．２節は、Promela と Spin を使って、アトミックでない加算の例で競合を見つけます。１２．３節は、Promela と Spin で同様のアトミック加算の例を検証します。１２．４節は Promela と Spin の使い方の概要です。１２．５節はスピンロックの Promela モデルを示します。１２．６節は、Promela と Spin を使って簡単な RCU 実装を検証します。１２．７節は、 Promela を使ってプリエンプティブ RCU と、Linux カーネルの dyntick-idle エネルギー節約機能のインタフェースを検証します。１２．８節は、形式的検証の必要ない、より簡単なインタフェースを示します。１２．９節は、ARM と Power のメモリオーダリングを理解する PPCMEM ツールを説明します。最後に、１２．１０節は並列アルゴリズムを検証するために形式的検証ツールを使うことについてまとめます。

１２．１ Promela と Spin は何ですか？

Promela は、プロトコルを検証することを助けるために設計された言語です。しかし、小さい並列アルゴリズムを検証するためにも使えます。あなたは、C に似た言語 Promela であなたのアルゴリズムと正しさの制約をコーディングし直します。そしてそれを、Spin を使って C に翻訳します。それはコンパイルして実行できます。結果となるプログラムはあなたのアルゴリズムの完全な状態空間探索をします。検証をし、あなたがご自分のPromelaプログラムに含めることのできるアサーションへの反例を探します。

完全な状態空間探索はとても強力でしょうが、両刃の剣でもあります。もしあなたのアルゴリズムがあまりに複雑であったり、あなたのPromela実装が注意を欠いている場合、メモリに入りきらないほどの状態ができることがあります。さらに、十分なメモリがあっても、状態空間探索は、宇宙の予測される寿命よりはるかに長く走ることがあります。なので、このツールは、コンパクトだが複雑なアルゴリズムに対して使って下さい。それを、何も考えずに、ほどほどのスケールのアルゴリズム(完全なLinux カーネルはとんでもない)に適用しようとする試みは悪い結果となるでしょう。

Promela と Spin は http://spinroot.com/spin/whatispin.html からダウンロードできます。

前記サイトには、Promela と Spin についての Gerard Holzmann の素晴らしい本 [Hol03] へのリンクや、http://www.spinroot.com/spin/Man/index.html で始まる、検索可能オンラインレファレンスへのリンクも有ります。

この節の残りは、Promela を使って並列アルゴリズムをデバッグするにはどうするかを述べます。単純な例から初めて、より複雑な使用に進みます。

１２．２ Promela の例: アトミックでない加算

図１２.１は、アトミックでない加算に起因する教科書的な競合条件を示します。１行目は走らせるプロセスの数を定義します(状態空間への影響を見るためにこれを変化させます)。３行目はカウンタを定義し、４行目は、２９から３９行目にあるアサーションを実装するために使います。

６から１３行目でカウンタをアトミックでなく加算するプロセスを定義します。引数 me は、プロセス番号で、コードの後の方の初期化ブロックで設定されます。単純なPromela文はそれぞれアトミックですから、加算は、１０と１１行目にある二つの文に分けなくてはいけません。１２行目の代入が、プロセスの完了をしるし付けます。Spin システムは、すべての可能な状態のシーケンスを含む状態空間の完全な探索を行うので、通常のテストで必要とされるループは要りません。

１５から４０行が初期化ブロックで、最初に実行されます。１９から２８行目は実際の初期化をします。そして、２９から３９行目はアサーションを実行します。不必要に状態空間を増やさないために、どちらもアトミックブロックです。これらはアルゴリズム自体の一部ではないので、それをアトミックにしても検証カバレッジは失われません。

２１から２７行目の do-od 構造は、Promela ループを実装します。それは、C のfor ( ; ; ) ループに switch 文があるものだと考えて良いです。case ラベルには、式が書けます。条件ブロック(:: でプレフィクスされます)は、非決定論的にスキャンされます。でもこの場合は一度には条件の一つだけが真となることができます。２２から２５行目にある do-od の最初のブロックは i 番目の加算者の進捗セルを初期化し、i 番目の加算者のプロセスを実行し、そして変数 i を加算します。２６行目の do-od の二つ目のブロックは、前記プロセスが全て開始したらループを抜けます。

２９から３９行目のアトミックブロックにも、類似の do-od ループがあり、進捗カウンタを合計します。３８行目の assert() 文は、全てのプロセスが完了したら全てのカウントが正しく記録されていることを確認します。

このプログラムをビルド、実行するにはこうします。

spin -a increment.spin # Translate the model to C

cc -DSAFETY -o pan pan.c # Compile the model

./pan # Run the model

これは、図１２．２に示した出力を出します。最初の行は、アサーションが破られた(アトミックでない加算ですから予期されたように！)ことを告げます。２行目は、アサーションがどのように破られたかを記述する trail ファイルが書かれたことを示します。"Warning" 行は、私たちのモデルに問題があったことを再び告げます。二つ目のパラグラフは、実行された状態探索の型を示します。今の場合、対象はアサーション発火と不正な終了状態です。三つ目のパラグラフは状態の大きさの統計です。この小さなモデルは４５の状態しか持ちません。最後の行はメモリの使用量です。

trail ファイルを人が読めるように展開するにはこうします。

spin -t -p increment.spin

すると図１２．３に示す出力が出ます。見てわかるように、初期化ブロックの最初の部分は二つの加算者プロセスを作成しました。その両方がまずカウンタをフェッチし、次に両方が加算と格納をした結果、カウントが失われました。するとアサーションが発火し、その後グローバルな状態が表示されました。

１２．３ Promela の例: アトミックな加算

この例をなおすのは簡単です。図１２．４に示すように、加算者プロセスのボディをアトミックブロックに入れます。単純に、文の対を counter = counter + 1 にしても良かったのです。Promela の文はアトミックですから。いずれにしても、この修正したモデルを走らせると、図１２．５に示す、エラーのない状態空間のトラバーサルができます。

１２．３．１ 組み合わせ爆発

表１２．１は、モデルされる加算者の数(NUMPROCS を定義し直します)の関数として、状態の数と使ったメモリを示します。

不必要に大きなモデルを走らせるのは、このように、あまりお勧めできません。６５２MBは、十分に現代のデスクトップやラップトップマシンの限界の範囲ですが。

この例をベルトにはさんで、Promela モデルを解析する時に使うコマンドをもっと詳しく見て、その次により洗練された例を調べましょう。

１２．４ Promela の使い方

ソースファイル qrcu.spin がある時、以下のコマンドを使うことができます。

• spin -a qrcu.spin

pan.c ファイルを作ります。これが、状態マシンを完全に探索します。

• cc -DSAFETY -o pan pan.c

生成された状態マシン探索をコンパイルします。-DSAFETY は、あなたがアサーションだけ(そしてもしかすると never 文も)を持つ時に適切な最適化を生成します。あなたが、 liveness, fairness, or forward-progress check を持つ時は、-DSAFETY なしでコンパイルする必要があるかもしれません。-DSAFETY を使うことができる時に、あなたがそれを付け忘れたら、プログラムが教えてくれます。

-DSAFETY が生成する最適化は、ものごとを大いに高速化します。なので、使える時には使うべきです。-DSAFETY を使うことができない状況とは例えば、-DNP でライブロック（「進行しないサイクル」とも言われます）をチェックする時です。

• ./pan

これが実際に状態空間を探索します。状態の数は、とても小さな状態マシンでも数千万に達することがあります。なので、たくさんのメモリのあるマシンが必要です。例えば、３リーダー、２更新者のある qrcu.spin は、2.7GBのメモリが必要でした。

あなたが、ご自分のマシンに十分なメモリがあるかわからない時は、一つのウィンドウで top を走らせ、もう一つで ./pan を走らせます。必要な時にすぐに実行を止められるように、フォーカスを ./pan ウィンドウに置いたままにします。CPU時間が、１００％よりもずっと落ちたらすぐに、 ./pan を止めなさい。 ./pan を走らせているウィンドウからフォーカスを外すと、ウィンドウシステムがあなたに何かをしてくれるために十分なメモリをかき集めるまで、長く待たないといけないことがあります。

出力をキャプチャするのを忘れないで下さい。特に、リモートマシンで作業している時は。

もしあなたのモデルが、forward-progress check を含む時は、./pan への -f コマンドライン引数を使って、“weak fairness” を有効にする必要があるでしょう。あなたの forward-progress check が、accept ラベルを含むなら、さらに、-a 引数も必要でしょう。

• spin -t -p qrcu.spin

エラーになった実行によって出力された trail ファイルを与えて、そのエラーになるステップのシーケンスを出力します。-g フラグは、変化したグローバル変数の値も含めます。-l フラグは、変化したローカル変数の値も含めます。

１２．４．１ Promela に特有なこと

全ての計算機言語はおおもとでは似たようなものですが、Promelaは C, C++, Java でコーディングすることに慣れた人が驚くことがいくつかあります。

１． C では、";" は文を終わらせます。Promelaでは、文を分離します。幸運なことに、より最近のバージョンのSpin は、「余分な」セミコロンに対してずっと寛容的になりました。

２． Promelaのループ構成である do 文は、条件を取ります。この do 文は、ループのある if-then-else 文にとてもよく似ています。

３． C の switch 文で、当てはまる case が無い場合は、文全体がスキップされます。Promelaの同等品、それはまぎらわしいことに if と呼ばれますが、当てはまる guard 式が無い時は、エラーになります。認知可能な対応するエラーメッセージはありません。なので、もしエラー出力がコードの無実な行を示していたら、if や do 文に条件を入れ忘れていないか調べましょう。

４． C でストレステストを作成する時、普通は、怪しい操作をお互いに繰り返し、競合させます。Promelaでは、その代わりに一つの競合を用意するだけです。Promelaは、一つの競合から全ての可能な出力を探索するからです。Promelaでループをする必要がある時も確かにあります。例えば、複数の操作がオーバーラップする時とか。でもそうすると状態空間の大きさがとても大きくなります。

５． C では、ループカウンタを維持して、進捗を追跡し、ループを終了するのは最も簡単なことです。Promelaでは、ループカウンタは悪疫のように避けられなくてはいけません。それは状態空間を爆発させるからです。その代わり、Promelaでは、単調増加あるいは減少する変数が無い限り、無限ループにペナルティはありません。Promelaはループを何回まわるのが現実的に重要かを考えて、それ以上の実行を自動的に枝刈りします。

６． C  の拷問テストコードでは、タスクごとの制御変数を維持するのはしばしば賢明なことです。読むのは安価で、テストコードをデバッグするのを大いに助けます。Promelaでは、タスクごとの制御変数はそれ以外の代わりがないときに限り使うべきです。これを見るために、５タスクの検証で、それぞれが完了したことを示すのに１ビットを使うとします。すると、３２状態になります。それに対して、単純なカウンタは６状態しか持ちません。５倍以上の節約です。この５倍のファクターは、あなたが、一億五千万以上の状態を処理し、１０GB以上のメモリを消費するプログラムの検証に苦しむようになるまでは大した問題とは思えないかもしれませんけど！

７． C の拷問テストコードでも、Promelaでも最も難しいことの一つは、良いアサーションを定式化することです。Promelaには他に、 never 要求も可能で、これはコードの全ての行に複製されたアサーションのように振る舞います。

８． Promelaでは、状態空間を制御の下におくために、分割して統治することはとても有効です。大きなモデルを分割して、ほぼ同じ大きさの半分づつにすることは、それぞれ半分の状態空間を、全体のほぼ二乗根の大きさにします。例えば、百万状態の複合モデルは、千状態のモデル二つに小さくできるかもしれません。Promelaは二つのより小さなモデルを、ずっと速く、ずっと少ないメモリで扱うことができるでしょう。それだけでなく、人々が理解するためにも、その二つの小さなアルゴリズムはより簡単でしょう。

１２．４．２ Promela コーディングトリック

Promelaはプロトコルを解析するために設計されました。なので、それを並列プログラムに使うことは少し乱用気味です。以下のトリックは、Promelaを安全に乱用する助けとなるでしょう。

１ メモリリオーダリング。

グローバル変数  x と y をローカル変数 r1 と r2 にコピーする文の対があったとします。オーダリングは重要（つまり、ロックで守られていません）ですが、メモリバリアは無いとします。これを Promela でモデルすると、こうなります。

1 if

2 :: 1 -> r1 = x;

3 r2 = y

4 :: 1 -> r2 = y;

5 r1 = x

6 fi

if 分の二つの分岐は非決定論的に選択されます。どちらも利用可能だからです。完全な状態空間探索がされますから、全ての場合に最終的には両方の選択が行われます。

もちろん、このトリックは、たくさん使うとあなたの状態空間を爆発させます。さらに、これはあなたが可能なリオーダリングを予想する必要があります。

２ 状態削減。

あなたが複雑なアサーションを持つ時は、それは atomic の元で評価しなさい。結局それらは、アルゴリズムの一部ではありません。図１２．６は、複雑なアサーションの例（あとで詳しく説明します）を示します。

このアサーションを、アトミックでなく評価する理由はありません。それは実際にアルゴリズムの一部ではないからです。それぞれの文は状態に寄与しますから、図１２．７のように、atomic ブロックにそれを囲い入れることで、不要な状態の数を減らすことができます。

３ Promela は関数を提供しません。あなたはその代わりに C プリプロセッサマクロを使わなくてはいけません。しかし、組み合わせ爆発を防ぐためには、それを注意深く使わなくてはいけません。

さて、もっと複雑な例に進む準備ができました。

１２．５ Promela の例：ロック

ロックは一般的に便利なので、lock.h には、spin_lock() と spin_unlock() マクロが提供されます。それは、図１２．８が示すように、複数の Promela モデルから引きこむことができます。spin_lock() マクロは、２から１１行目にわたる、無限の do-od ループを持ちます。これは、３行目の“1”という単一の guard 式のためです。このループのボディは、 if-fi 文を持つ単一のアトミックブロックです。 if-fi 構成は、do-od 構成と似ていますが、それはループでなくて単一のパスを取ります。５行目でロックが取られていない時は、６行目でそれを取り、７行目はそれを囲む do-od ループから抜けます（同時にアトミックブロックも抜けます）。そうでなく、８行目でロックが既に取られている時は、何もせず (skip)、if-fi とアトミックブロックを抜けて、外側のループをもう一度回ります。ロックが取れるまでこれを繰り返します。

spin_unlock() マクロは単純にロックが取られていないしるしをつけます。

メモリバリアはいらないことに注意下さい。Promela はフルオーダリングを前提とするからです。どの Promela 状態にあっても、全てのプロセスは、現在の状態と、我々をその現在の状態に至るようにした状態変更の順序の両方について合意しています。これは、いくつかの計算機システム（MIPS と PA-RISC のような）で使われている “sequentially consistent”メモリモデルに似ています。以前に述べたように、また、後の例でも出てきますが、弱いメモリオーダリングは明示的にコーディングされる必要があります。

これらのマクロは図１２．９に示す Promela コードでテストされます。このコードは加算のテストに使ったものと似ています。３行目は、N_LOCKERS マクロ定義で、ロックプロセスの数を定義します。mutex 自身は５行目で定義されます。ロック所有者を追跡するための配列が６行目、そして７行目は、一つのプロセスだけがロックを保持することを検証するためのアサーションコードで使われます。

ロッカープロセスは９から１８行目にあり、１３行目でロックを取り、１４行目でそれを示し、１５行目でそれを取り消し、１６行目でロックを放すというループを単純に無限に続けます。

２０から４４行目は初期化ブロックです。２６行目で現在スレッドの havelock 配列エントリを初期化して、２７行目で現在のロッカーを開始し、２８行目で次のロッカーに進みます。全てのロッカーを起動したら、do-od ループは２９行目に進み、アサーションをチェックします。３０と３１行は制御変数を初期化します。３２から４０行目はアトミックに havelock 配列エントリを合計します。４１行目がアサーションで、４２行目でループを抜けます。

このモデルを走らせるには、前記の二つのコード断片をそれぞれ lock.h と lock.spin というファイルに入れて、以下のコマンドを走らせます。

出力は、図１２．１０で示したようなものとなります。期待された通り、この実行はアサーション失敗はありません (“errors: 0”)でした。

クイッククイズ１２．１

ロッカーには、なぜ到達されない文があるのですか？結局、これは完全な状態空間探索ではないのですか？

クイッククイズ１２．２

この例にある、Promela コードスタイルの問題は何でしょう？

１２．６ Promela 例：QRCU

この最後の例は、Oleg Nesterov の QRCU [Nes06a, Nes06b] に対する Promela の実世界での使用を示します。ただし、synchronize_qrcu() 高速パスをスピードアップするように変更してあります。

でもまず、QRCU とは何ですか？

QRCU は SRCU [McK06b] の変種で、極端に低いグレースピリオドの遅延と引き換えに、ある程度高いリードオーバーヘッド（グローバル変数へのアトミックな加算と減算）を持ちます。リーダーがいない時は、グレースピリオドは１マイクロ秒以下のうちに検出されます。これは、ほとんどの他のRCU実装での複数ミリ秒のグレースピリオド遅延と比較されます。

１ QRCU ドメインを定義する qrcu_struct があります。SRCUと同じく（そして他のRCUの変種とは異なって）QRCU のアクションはグローバルではなく、特定の qrcu_struct にフォーカスしています。

２ QRCU リード側クリティカルセクションを区切る qrcu_read_lock() と qrcu_read_unlock() プリミティブがあります。対応する qrcu_struct をこのプリミティブに与えないといけません。そして qrcu_read_lock() の戻り値は、qrcu_read_unlock() に与えないといけません。

例えば、

idx = qrcu_read_lock(&my_qrcu_struct);

/* read-side critical section. */

qrcu_read_unlock(&my_qrcu_struct, idx);

３ synchronize_qrcu() プリミティブがあり、それは全ての既存のQRCU リード側クリティカルセクションが完了するまでブロックします。しかし、SRCU の synchronize_srcu() と同様に、 QRCU のsynchronize_qrcu() は、同じ qrcu_struct を使っているリード側クリティカルセクションだけを待てばよいです。

例えば、synchronize_qrcu(&your_qrcu_struct) は、以前のリード側クリティカルセクションを待つ必要はありません。それに対して、synchronize_qrcu(&my_qrcu_struct) は待つ必要があります。それは同じ qrcu_struct を共有するからです。

QRCU のためのLinuxカーネルパッチは、作成されました [McK07b] が、２００８年４月時点では、まだLinuxカーネルに取り込まれていません。

QRCU のための Promela コードに戻りましょう。図１２．１１にグローバル変数を示します。この例はロックを使います。なので、lock.h を引き込みます。リーダーとライターの数は両方とも、二つの #define 文で変えることができます。組み合わせ爆発を作る方法は、一つでなく二つあるわけです。idx 変数が、ctr 配列の二つの要素のうちリーダーがどちらを使うかを制御します。そして、readerprogress 変数は、アサーションで全てのリーダーが終了した時を決めることができるようにします（QRCU更新は、全ての既存のリーダーがそれぞれのQRCUリード側クリティカルセクションを完了するまで完了することが許されないからです）。readerprogress 配列要素は、以下の値を持ち、対応するリーダーの状態を示します。

０：まだ開始していません。

１：QRCUリード側クリティカルセクションにいます。

２：QRCUリード側クリティカルセクションを終わりました。

最後に、mutex 変数は、更新者の低速パスをシリアライズするために使われます。

QRCU リーダーは、図１２．１２の qrcu_reader() プロセスでモデルされます。５から１６行目に  do-od ループがあり、６行目の単一の “1”guard のために無限ループになります。７行目はグローバルインデックスの現在値を捉えます。そして８から１５行目は、アトミックに、その値がゼロでないかを見てそうならばそれを加算し（atomic_inc_not_zero()）（そして無限ループから抜け）ます。１７行目はRCUリード側クリティカルセクションに入ることをしるしづけ、１８行目でそのクリティカルセクションを抜けたことをしるしづけます。両方の行は、後に出てくる assert() のためです。１９行目は先ほど加算した同じカウンタをアトミックに減算して、RCUリード側クリティカルセクションを抜けます。

図１２．１３に示した C プリプロセッサマクロは、弱いメモリオーダリングをエミュレートするように、カウンタの対を合計します。２から１３行目でカウンタの一つをフェッチし、１４行目は対の反対側をフェッチしてそれらを加算します。アトミックブロックは単一の do-od 文からなります。この do-od 文（３から１２行目にあります）は、４と８行目に、 guard のある二つの無条件の分岐を持つ点が、特殊です。これにより Promela は、この二つのうち一つを非決定論的に選ぶ（しかし今回も、完全な状態空間探索の結果、Promela は最終的にはそれぞれ可能な状況における全ての可能な選択を行います）ことになります。最初の分岐は、ゼロ番目のカウンタをフェッチして、i を 1 にします（１４行目が最初のカウンタをフェッチするように）。一方、二つ目の分岐は反対をします。最初のカウンタをフェッチして、i を 0 にします（１４行目が二つ目のカウンタをフェッチするように）。

クイッククイズ１２．３

do-od 文をコードするもっと直裁的な方法はありませんか？

sum_unordered マクロを手にしたので私たちは、図の更新側プロセスに進むことができます。更新側プロセスは無限に繰り返します。対応する do-od ループは７から５７行目にわたります。ループのそれぞれのパスは、１２から２３行目で、まずグローバルな readerprogress 配列をローカルな readerstart 配列にスナップショットします。５３行目のアサーションでこのスナップショットを使います。２３行目は、sum_unordered を呼んで、２４から２７行目は、高速パスが潜在的に使えるならば再び sum_unordered を呼びます。

２８から４０行目は必要なら低速パスのコードを実行します。３０と３８行目で更新側ロックを取って、放します。３１から３３行目でインデックスをフリップし、３４から３７行目で全ての既存のリーダーが完了するのを待ちます。

４４から５６行目はその後 readerprogress 配列にある現在値を readerstart 配列に採取したものと比べます。この更新の前に開始したリーダーがまだ実行中であるならば、アサーション失敗を強制します。

クイッククイズ１２．４

１２から２１行目と、４４から５６行目にアトミックブロックがあるのはなぜですか？これらのアトミックブロック内の演算子は現在製造されているマイクロプロセッサのどれでもアトミックな実装はないにもかかわらず。

クイッククイズ１２．５

２４から２７行目でもう一度カウンタを合計するのは、本当に必要ですか？

あと残ったのは、図１２．１５の初期化ブロックだけです。このブロックは単純に５と６行目でカウンタの対を初期化し、７から１４行目でリーダープロセスを生成し、１５から２１行目で更新者プロセスを生成します。これは全部、状態空間を減らすために、アトミックブロック内で行われます。

１２．６．１ QRCU の例を実行する

QRCU の例を実行するには、前の節のコード断片を組み合わせて qrcu.spin という名前の単一ファイルに入れ、そして、spin_lock() と spin_unlock() の定義を lock.h という名前のファイルに入れます。そして以下のコマンドを使って、QRCU モデルをビルドして実行します。

spin -a qrcu.spin

cc -DSAFETY -o pan pan.c

./pan

結果となる出力は、このモデルが表１２．２に示す全ての場合で合格したことを示します。さて、３つのリーダーと３つの更新者のあるモデルを走らせられたら良いでしょうが、単純に外挿するとこれは最善でもテラバイトのオーダーのメモリが必要だとわかります。さて、どうしたらいいでしょう？以下は可能なアプローチの例です。

１ より小さな数のリーダーと更新者が、一般の場合を証明するのに十分であるかを調べる。

２ 手作業で、正しさの証明を構成する。

３ より強力なツールを使う。

４ 分割して統治する。

以下の節でこれらのアプローチをそれぞれ説明します。

１２．６．２ リーダーと更新者は実際にはいくつ必要ですか？

一つのアプローチは、qrcu_updater() の Promela コードを注意深く調べることです。すると、グローバルな状態変更はロックの下でだけ起きていることがわかります。なので、リーダーあるいは他の更新者に見える状態を変更することは、一度に一つの更新者だけがたぶんそれが可能です。ということは、状態変更のどのようなシーケンスであっても、単一の更新者によってシリアルに実行すればよいことを意味します。Promela は、完全な状態空間の探索をするからです。なので、最大でも二つの更新者があれば良いです。一つは状態を変更するもの、もう一つは、混乱させられるもの。

リーダーの状況はそれほど明確ではありません。それぞれのリーダーは単一のリード側クリティカルセクションを行なってそして終了するからです。高速パスは、最大でも一つのゼロと一つの１をカウンタに見なければいけないという事実を元に、意味のあるリーダーの数は限られていると主張することもできます。これは研究の実り多い道です。実際、それは、次の節で述べる正しさの完全な証明につながりました。

１２．６．３ 他のアプローチ：正しさの証明

以下は、正式ではない証明 [McK07b]です。

１ synchronize_qrcu() が早く終了しすぎるためには、定義により、少なくても一つのリーダーが synchronize_qrcu() の完全な実行の間に存在しなくてはいけません。

２ このリーダーに対応するカウンタは、この時間間隔の間、少なくても１であったはずです。

３ synchronize_qrcu() コードは、全ての時間において、数なくても一つのカウンタが少なくても１であることを強制します。

４ なので、時間のいかなる時点においても、カウンタの一つが少なくても２であるか、あるいはカウンタの両方が少なくても１であるかのとちらかのはずです。

５ しかし、synchronize_qrcu() 高速パスコードは、一度にはカウンタの一つだけしか読めません。なので、高速パスのコードが、最初のカウンタがゼロの時にそれをフェッチして、しかしカウンタのフリップとの競合のために、二つ目のカウンタが１であるのが見えることが可能です。

６ そのような競合条件の間、存在するのは、最大でも一つのリーダーだけです。そうでないならば、合計は２以上となり、その結果更新者は低速パスを取ることになるはずだからです。

７ しかしもしも競合が高速パスの最初のカウンタのリードで起き、そして再び、二度目のリードで起きたならば、二つのカウンタフリップがあったはずです。

８ ある更新者はカウンタを一度しかフリップしません。そして更新側のロックは、更新者の対が同時にカウンタをフリップするのを防ぐために、高速パスコードがフリップと二回競合することのできるただ一つの方法は、最初の更新者が完了することです。

９ しかし最初の更新者は、全ての既存のリーダーが完了してしまわないかぎり完了しません。

１０ なので、もしも高速パスが続けてカウンタフリップと二回競合するならば、全ての既存のリーダーが完了しているはずです。なので、高速パスを取るのは安全です。

もちろん、全ての並列アルゴリズムがこのような単純な証明ができるわけではありません。その場合、より強力なツールを使う必要があるかもしれません。

１２．６．４ 別のアプローチ:より強力なツール

Promela と Spin  はとても役に立ちますが、ずっと強力なツールが、特にハードウェアを検証するためには、存在します。これはつまり、あなたのアルゴリズムをハードウェア設計VHDL言語に翻訳できれば、そしてそれはしばしば低レベルの並列アルゴリズムなら可能でしょうし、これらのツールをあなたのコードに適用できるということです。(例えば、最初の実時間RCUアルゴリズムで私はこれをやりました。)しかしそういうツールはとても高価なことがあります。

コモディティとなったマルチプロセッシングの出現は、いずれは、素敵な状態空間削減能力を持った強力なフリーソフトウェアのモデルチェッカーを可能とするかもしれませんが、今のところはあまり役に立つものではありません。

一方、Spin には、有限の量のメモリしか必要としない近似的探索機能があります。しかし私は、並列アルゴリズムを検証するのに、近似というものを信じる様にはどうしてもなれないでいます。

別のアプローチは、分割して統治せよ、でしょう。

１２．６．５ 別のアプローチ：分割して統治せよ

大きな並列アルゴリズムを、それぞれが個別に証明できる、より小さな部品に分割することが可能であることがよくあります。例えば、１００億状態のモデルは、１０万状態のモデル二つに分割できるかもしれません。このアプローチをとれば、Promela のようなツールがあなたのアルゴリズムを証明するのがより簡単になるだけでなく、あなたのアルゴリズムをより理解しやすくすることもできるでしょう。

１２．７ Promela のお話：dyntick と、プリエンプト可能なRCU

２００８年初頭、RCUのプリエンプト可能な変種が、実時間ワークロードをサポートするために、メインラインLinuxに採用されました。それは、２００５年８月からある、-rt パッチセットにあるRCU実装に似た変種でした。実時間ワークロードのためには、プリエンプト可能なRCUが必要でした。古いRCU実装は、RCUリード側クリティカルセクションの間、プリエンプションを禁止したため、実時間遅延が大きすぎました。

しかし、古い -rt 実装(付録D.４にあります)の一つの欠点は、グレースピリオドは全て、それぞれのCPUである仕事が実行されることを必要としたことです。そのCPUが省電力の “dynticks-idle” 状態にあり、RCUリード側クリティカルセクションを実行することができなくてもです。dynticks-idle 状態の背後にある考えは、アイドルなCPUはエネルギーを節約するために、物理的に電力ダウンされるべきだということです。短く言えば、プリエンプト可能RCUは、最近のLinuxカーネルの、価値あるエネルギー節約機能を無効にすることがあるのです。Josh Triplett と Paul McKenney が、RCUグレースピリオドの間、CPUが省電力状態にとどまる(そしてLinuxカーネルのエネルギー節約能力をそのままとする)ことを許すいくつかのアプローチを議論しましたが、Steve Rostedt が、-rt パッチセットにおいて、新しい dyntick 実装をプリエンプト可能RCUと統合するまで、大きな進展はありませんでした。

この組み合わせは、Steve のシステムの一つを、ブート時にハングさせました。なので、１０月に、Paul は、プリエンプト可能RCUのグレースピリオド処理の、dyntick に優しい修正を書き上げました。Steve は、irq_enter() と irq_exit() 割り込み開始、終了関数から呼ばれる、rcu_irq_enter() と rcu_irq_exit() インタフェースを書き上げました。これら rcu_irq_enter() と rcu_irq_exit() 関数は、dyntick アイドルなCPUが一時的に電力アップされて、RCUリード側クリティカルセクションを含む割り込みハンドラを実行する状況を、RCU が安全に扱うことができるために必要です。これらの変更を入れたところ、Steve のシステムは安定してブートしました。しかし Paul は、最初の試みではコードを正しく書けないかもしれないという予想を持っていたので、定期的にコードを見直し続けました。

Paul は２００７年１０月から２００８年２月の間何度もコードをレビューし、ほとんど常に、少なくても一つのバグを見つけました。ある場合には、Paul は、バグが幻想であるとわかる前に、修正をコードし、テストしました。そして実際、全ての場合で、「バグ」は幻想でした。

２月の終わり近くになって Paul はこのゲームがいやになりました。なので彼は、ここで述べる、Promela と Spin の助けを借りる決断をしました。

訳注

described in Section 12 というのは、１２章の誤りでしょう。

以下に、７つの、順に現実的になっていく Promela モデルを示します。そのうち最後のが、状態空間に約40GB のメインメモリを使って合格しました。

もっと重要なことは、Promela と Spin は実際に、私の代わりにとてもわかりにくいバグを見つけてくれたことです！

クイッククイズ１２．６

ほう、それはすごいですね！さて、もし私が40GB のメインメモリのあるマシンなんて持ってない時はどうしろと言うんです？？？

でもそれより良いのは、より小さな状態空間を持ち、より単純でより高速なアルゴリズムを思いつくことでしょう。それより良いのは、あまりに単純なためにそれが正しいことが普通の傍観者にも自明であるアルゴリズムでしょう！

１２．７．１節は、プリエンプト可能なRCUの dyntick  インタフェースの概要を示します。１２．７．２と１２．７．３は、この作業の間に（再び）得られた、教訓を一覧にします。

１２．７．１ プリエンプト可能RCUと dyntick の紹介

CPUごとの、dynticks_progress_counter 変数が、 dyntick とプリエンプト可能RCUの間のインタフェースにとって最も重要です。この変数は、対応するCPUが dynticks-idle モードの時は必ず偶数値、そうでない時は奇数値を持ちます。CPUは以下の３つの理由で、dynticks-idle モードを抜けます。

１ タスクの実行を始めるため

２ ネストしているかもしれない割り込みハンドラのセットの一番外のに入る時

３ NMI ハンドラに入る時

プリエンプト可能RCUのグレースピリオド機構は、dynticks_progress_counter 変数の値をサンプリングして、dynticks-idle なCPUを無視しても安全な時を決定します。

以下の三つの節で、タスクインタフェース、割り込み／NMIインタフェース、そして、グレースピリオド機構での dynticks_progress_counter 変数の使い方の概要を示します。

１２．７．１．１ タスクインタフェース

あるCPUが実行するべきタスクがもう無いために dynticks-idle モードに入る時は、それは rcu_enter_nohz() を呼びます。

この関数は、単純に dynticks_progress_counter 変数を加算して、結果が偶数か調べます。なおその前にメモリバリアを実行します。これは、dynticks_progress_counter の新しい値を見た全ての他のCPUが、以前の全てのRCUリード側クリティカルセクションの完了も見ることを保証するためです。

同様に、dynticks-idle モードにあるCPUが、新しく実行可能になったタスクの実行を始める準備をする時、それは rcu_exit_nohz() を呼びます。

この関数も、dynticks_progress_counter を加算しますが、その後にメモリバリアを置いて、もし他のCPUのどれかが、以降のどれかのRCUリード側クリティカルセクションの結果を見るならば、そのCPUは dynticks_progress_counter の加算された値も見ることを保証します。最後に、rcu_exit_nohz() は加算の結果が奇数か調べます。

rcu_enter_nohz() と rcu_exit_nohz() 関数は、CPUが、タスク実行のために dynticks-idle モードに出入りする場合を扱いますが、割り込みは扱いません。それについては、次の節で。

１２．７．１．２ 割り込みインタフェース

rcu_irq_enter() と rcu_irq_exit() は、割り込み／NMIへの出入りをそれぞれ扱います。もちろん、ネストした割り込みもきちんと扱わないといけません。ネストした割り込みの可能性は、二つ目のCPUごとの変数である rcu_update_flag によって扱われます。

それは、割り込みあるいはNMIハンドラに入る時に(rcu_irq_enter() で)加算され、抜ける時に(rcu_irq_exit() で)減算されます。さらに、既存の in_interrupt() プリミティブが、割り込み／NMIの最も外側か、ネストしたものかを区別するのに使われます。

割り込みに入るのは、以下に示す rcu_irq_enter で扱われます。

３行目は現在のCPU番号をフェッチします。そして５から６行目は、rcu_update_flag ネストカウンタが既にゼロでない時にはそれを加算します。７から９行目はこれが最も外側のレベルの割り込みであるかを見て、そうならば dynticks_progress_counter を加算する必要があるかを見ます。そうならば、１０行目で dynticks_progress_counter を加算し、１１行目でメモリバリアを実行し、１２行目で rcu_update_flag を加算します。rcu_exit_nohz() の時と同様に、メモリバリアは割り込みハンドラ（rcu_irq_enter() 呼び出しの後に続く）内のRCUリード側クリティカルセクションの効果を見た他のCPUは全て、dynticks_progress_counter の加算も見ることを保証します。

クイッククイズ１２．７

単純に rcu_update_flag を加算して、rcu_update_flag の元の値がゼロであった時だけ dynticks_progress_counter を加算したらどうですか？？？

クイッククイズ１２．８

でももし７行目で最も外側のレベルの割り込みであることがわかったらならば、常に dynticks_progress_counter を加算しないといけないのではないですか？

割り込みから抜けるのは同様に、rcu_irq_exit() が扱います。

３行目は以前と同じく現在のCPU番号をフェッチします。５行目は rcu_update_flag がゼロでないかを見て、そうでないならすぐに戻り（関数の終わりに落ちます）ます。そうでない時は、６から１２行目の出番です。６行目は rcu_update_flag を減算して、結果がゼロでない時は戻ります。８行目は、我々が確かにネストした割り込みの最も外側のレベルから抜けるところであるのを確認します。９行目はメモリバリアを実行して、１０行目は dynticks_progress_counter を加算し、１１と１２行目でこの変数が偶数でないことを確認します。rcu_enter_nohz() と同様に、メモリバリアは、dynticks_progress_counter の加算を見た他のCPUは全て、割り込みハンドラ（rcu_irq_exit() 呼び出しの前にある）内のRCUリード側クリティカルセクションの効果も見ることを保証します。

以上の二つの節で、dynticks_progress_counter 変数が、タスク、割り込み、そしてNMI において、 dynticks-idle モードに入る時と出るときにどのように維持されているかを説明しました。以下の節はこの変数が、プリエンプト可能RCU のグレースピリオド機構によってどのように使われるかを説明します。

１２．７．１．３ グレースピリオドインタフェース

付録D.４、５６４ページの図D.63に示す４つのプリエンプト可能RCUのグレースピリオド状態のうち、rcu_try_flip_waitack_state() とrcu_try_ flip_waitmb_state() 状態だけが、他のCPUの応答を待つ必要があります。

もちろん、もしあるCPUが dynticks-idle 状態にあるなら、それを待ってはいけません。なので、前記二つの状態のどれかに入るすぐ前に、その前の状態でそれぞれのCPUの dynticks_progress_counter 変数のスナップショットを取り、それを別のCPUごと変数 rcu_dyntick_snapshot に置きます。これは、以下の dyntick_save_progress_counter を呼ぶことで行います。

rcu_try_flip_waitack_state() 状態は以下の rcu_try_flip_waitack_needed() を呼びます。

７と８行目はそれぞれ、 dynticks_progress_counter の現在とスナップショットのバージョンをピックアップします。９行目のメモリバリアは後の rcu_try_flip_waitzero_state でのカウンタのチェックがそれらカウンタのフェッチの後に来るのを保証します。１０と１１行目は、そのCPUがスナップショットが取られた時刻からずっと dynticks-idle 状態にあったならばゼロ（このCPUとの通信は必要ないことを意味します）を返します。同様に、１２と１３行目は、そのCPUが最初に dynticks-idle 状態にあったかあるいは、完全に dynticks-idle 状態を通り抜けたならばゼロを返します。このどちらの場合も、そのCPUがグレースピリオドカウンタの古い値を保持しているはずはありません。このどちらの条件も成り立たない場合は、１４行目で１を返し、そのCPUが明示的に応答しなくてはいけないことを示します。

一方、rcu_try_flip_waitmb_state は、以下の rcu_try_flip_waitmb_needed() を呼びます。

これは、rcu_try_flip_waitack_needed にとても似ています。違いは１２と１３行目で、dynticks-idle 状態からあるいはそれへの全ての遷移は、rcu_try_flip_waitmb_state() 状態が必要とするメモリバリアを実行するからです。

さてこれで私達は、RCU と dynticks-idle 状態の間のインタフェースに関する全てのコードを見ました。次の節は、このコードを検証することに使う Promela モデルを作り上げます。

クイッククイズ１２．９

この節のコードのどれかに、バグを見つけられますか？

１２．７．２ プリエンプト可能RCUと dynticks を検証する

この節は、dynticks と RCU の間のインタフェースのための Promela モデルを順を追って作り上げていきます。以下の節がそれぞれ一つのステップを説明します。まず、プロセスレベルのコードで始め、アサーション、割り込み、最後にNMIを加えます。

１２．７．２．１ 基本モデル

この節は、プロセスレベルの dynticks 出入りとグレースピリオド処理を Promela に翻訳します[Hol03]。最初に、2.6.25-rc4 カーネルの rcu_exit_nohz() と rcu_enter_nohz() を、単一の Promela プロセスに置きます。それは以下のように、 dynticks-idle モードに出入りしてループすることをモデルします。

６から２０行目はループを定義します。７行目はループカウンタ i が MAX_DYNTICK_LOOP_NOHZ 限界を超えたらループを終わります。８行目はループの構成に、ループのそれぞれのパスで９から１９行目を実行するように告げます。７と８行目にある条件は互いに排他的なので、通常の Promela の真の条件をランダムに選択する機能は無効になります。９と１１行目は、rcu_exit_nohz() の、dynticks_progress_counter のアトミックでない加算をモデルします。そして１２行目は WARN_ON() をモデルします。atomic 構成は、単純に Promela 状態空間を減らします。WARN_ON() は厳密にはアルゴリズムの一部ではないからです。１４から１８行目は同様に rcu_enter_nohz() の加算と WARN_ON() をモデルします。最後に、１９行目はループカウンタを加算します。

なので、ループのそれぞれのパスは、dynticks-idle モードを抜けて（例えば、タスク実行を始める）そして再度 dynticks-idle モードに入る（例えば、その同じタスクがブロックする）CPUをモデルします。

クイッククイズ１２．１０

なぜ Promela では、rcu_exit_nohz() と rcu_enter_nohz() にあるメモリバリアはモデルされないのですか？

クイッククイズ１２．１１

rcu_exit_nohz() の後に rcu_enter_nohz() が続くのをモデルするのは少し変でないですか？その代わりに、入って、出るのをモデルする方がより自然でないですか？

次のステップは、RCUのグレースピリオド処理へのインタフェースをモデルすることです。このために、2.6.25-rc4 kernel の、dyntick_save_progress_counter(), rcu_try_flip_waitack_needed(), rcu_try_flip_waitmb_needed(), そして、 rcu_try_flip_waitack() と rcu_try_flip_waitmb() の一部をモデルする必要があります。以下の、grace_period() Promela プロセスは、これらの関数が、単一のパススループリエンプト可能RCUのグレースピリオド処理の間に呼ばれることをモデルします。

６から９行目はループの限界を表示（ただし、エラーの時に .trail ファイルに対してだけ）して、rcu_try_flip_idle() の１行のコードとそこからの dyntick_save_progress_counter() 呼び出しをモデルします。それは現在CPUの dynticks_progress_counter 変数のスナップショットを取ります。この２行は、状態空間を減らすためにアトミックに実行されます。

１０から２２行目は rcu_try_flip_waitack() の関連するコードと、そこからの rcu_try_flip_waitack_needed() 呼び出しをモデルします。このループは、それぞれのCPUからのカウンタフリップ応答を待つグレースピリオド状態マシンをモデルします。ただし、 dynticks-idle CPU と相互作用する部分だけです。

２３行目は rcu_try_flip_waitzero() からの１行と、そこからの dyntick_save_progress_counter() をモデルします。ここでも、CPUの dynticks_progress_counter 変数のスナップショットを取ります。

最後に、２４から３６行目は、rcu_try_flip_waitmb_state() の関連するコードと、そこからの rcu_try_flip_waitmb_needed() 呼び出しをモデルします。

訳注

原文は rcu_try_flip_waitack() rcu_try_flip_waitack_needed() ですが、コピペの誤りです。

このループは、それぞれのCPUがメモリバリアを実行するのを待つグレースピリオド状態マシンをモデルします。ただしこれも、 dynticks-idle CPU と相互作用する部分だけです。

クイッククイズ１２．１２

待って下さい！Linuxカーネルでは、dynticks_progress_counter も rcu_dyntick_snapshot もCPUごとの変数です。なのになぜ、その代わりに単一のグローバル変数としてモデルされるのですか？

結果となるモデル (dyntickRCU-base.spin) を、 runspin.sh スクリプトで走らせると、６９１の状態を生成して、エラー無しに合格します。それは全然驚くことではありません。それは誤りを見つけることのできるアサーションが何もないからです。なので次の節は、安全のためのアサーションを追加します。

１２．７．２．２ 安全を検証する

安全なRCU実装は、決して、グレースピリオドが、そのグレースピリオドが始まる前に開始したRCUリーダーの全てが完了する前に完了するのを許してはいけません。これは、以下の３つの状態を持つ gp_state 変数でモデルされます。

grace_period() プロセスは、以下に示すように、グレースピリオドのフェーズを進むにつれてこの変数を設定します。

６，１０，２５，２６，２９ そして４４行目がこの変数を更新します（可能なときには、アルゴリズムの操作とアトミックに組み合わされます）。これにより、dyntick_nohz() プロセスが基本的なRCUの安全性を検証することができます。この検証の形式は、gp_state 変数の値が、RCUリーダーがたぶん存在する期間に、GP_IDLE から GP_DONE に飛ぶことはないのを確認することです。

クイッククイズ１２．１３

gp_state は、２５と２６行目で隣接して変更されます。２５行目の変更が失われることがないとどうしてわかりますか？

dyntick_nohz() Promela プロセスは、この検証を以下のように実装します。

１３行目はタスクの実行が始まった時に gp_state 変数の値が GP_IDLE ならば新しい old_gp_idle フラグを設定します。そして、１８と１９行目のアサーションは、タスク実行の間に gp_state 変数の値が GP_DONE に進んでいたら発火します。一つのRCUリード側クリティカルセクションはその間の期間ずっとに渡ることがあり得るので、それは非合法だからです。

結果となるモデル (dyntickRCU-base-s.spin)を、 runspin.sh スクリプトで走らせると、９６４の状態を生成して、エラー無しに合格します。それは心強いことです。とは言え、安全性は致命的に重要ですが、グレースピリオドが無限にストールするのを避けることもとても重要です。なので、次の節は生きていることの検証に移ります。

１２．７．２．３ 生きていることを検証する

生きていることを証明するのは難しいかもしれませんが、ここで使える単純なトリックがあります。最初のステップは、以下の２７行目に示すように、dyntick_nohz() が、dyntick_nohz_done 変数を使って、自分が終わったことを知らせるようにすることです。

この変数があれば、以下のように grace_period() にアサーションを加えて、不要なストールをチェックできます。

５行目に shouldexit 変数を加えました。これは、１０行目でゼロに初期化します。１７行目は、shouldexit がセットされていないことを確認します。そして１８行目は、dyntick_nohz() が維持する dyntick_nohz_done 変数を shouldexit に設定します。なので、このアサーションは、dyntick_nohz() が実行を完了した後、カウンタのフリップ応答を待つループを、１度よりたくさん回ろうとすると発火します。結局、dyntick_nohz() が終わったならば、私達がループを抜けるように強制する状態変更はそれ以上あり得ません。なので、この状態を二回りするのは無限ループを意味し、それは結局、グレースピリオドに終わりが無いことを意味します。

３２，３９そして４０行目も、二つ目の（メモリバリア）ループに関して同様にはたらきます。

しかしこのモデル (dyntickRCU-base-sl-busted.spin) を走らせると、失敗します。２３行目は、間違った変数が偶数であることをチェックしているからです。失敗すると、spin は“trail” ファイル (dyntickRCU-base-sl-busted.spin.trail) を書き出します。そこには、失敗に至った状態のシーケンスが記録されています。spin がこの状態のシーケンスを再追跡して、実行された文と変数の値(dyntickRCU-base-sl-busted.spin.trail.txt)を表示するようにするには、spin -t -p -g -l dyntickRCU-base-sl-busted.spin コマンドを使います。なお、spin が両方の関数を単一のファイルから得るために、行番号は前述のソースコードリストに一致しないのに注意下さい。しかし、行番号は、完全なモデルl (dyntickRCU-base-sl-busted.spin)と一致します。

dyntick_nohz() は、３４ステップで完了したことがわかります（“34:”を探して下さい）。しかし、grace_period() プロセスはそれでもループを抜けることに失敗しました。curr の値は６です（ステップ３５を参照）。そして snap の値は５です（ステップ１７を参照）。なので、前記２１行目の最初の条件は curr != snap のため成り立ちません。そして、２３行目の二つ目の条件も snap が奇数で、curr が  snap より一つ大きいだけなので成り立ちません。

なので、これら二つの条件のどちらかが誤っています。rcu_try_flip_waitack_needed() の、最初の条件のためのコメントブロックを見ると：

もし CPUが、この時間の間ずっと dynticks モードにとどまり、割り込み、NMI,SMI その他何も、受けない時には、rcu_read_lock() の中にいることはできません。なので、それが実行する次の rcu_read_lock() は、カウンタの新しい値を使わなくてはいけません。このため、このCPUは既にカウンタに応答したと安全にみなすことができます。

最初の条件は確かにこれに合います。なぜならば、curr == snap であり、curr が偶数ならば、対応するCPUはその間ずっと dynticks-idle モードにいたはずで、それは期待通りです。なので、二つ目の条件のためのコメントブロックを見ましょう。

もしCPUが dynticks idle フェーズを通り過ぎるかあるいは入った時にアクティブな割り込みハンドラがいなかったならば、前記と同じく、このCPUは既にカウンタに応答したと安全にみなすことができます。

条件の最初の部分は正しいです。なぜならば、curr と snap が二つ違うならば、その間には少なくても一つの偶数があるはずで、それは dynticks idle フェーズを完全に通り過ぎたことに対応します。しかし、条件の二つ目の部分は、dynticks-idle で開始したことに対応します。このモードで終わったことではありません。なので、snap ではなくて、curr の方を偶数であるか判定する必要があります。

正しい C コードは以下です。

すると１０から１３行は一緒にして簡単化でき、こうなります。同様の簡単化を、rcu_try_flip_waitmb_needed にも行えます。

モデルに対応する修正 (dyntickRCU-base-sl.spin)をすると、６６１の状態を持ち、エラー無しに合格する正しい検証ができます。しかし、生きていることの検証の最初のバージョンはこのバグを捉えることに失敗したことに注意するのは重要です。それは、生きていることの検証それ自体のバグのせいでした。この生きていることの検証のバグは、grace_period() プロセスに無限ループを挿入して、生きていることの検証コードがその問題を検出できないことによって発見されました！

さてこれで、安全性と生きていることの条件の両方の検証に成功しました。しかしこれは走ったりブロックしたりするプロセスに関してだけです。割り込みも扱う必要があります。次の節で取り上げる仕事です。

１２．７．２．４ 割り込み

Promela で割り込みをモデルするにはいくつかの方法があります。

１ C プリプロセッサのトリックを使って、dynticks_nohz() プロセスの全ての文の間に割り込みハンドラを挿入します。

２ 割り込みハンドラを別のプロセスでモデルします。

少し考えると、二つ目のアプローチがより小さい状態空間を持つだろうことがわかります。しかしそれは、割り込みハンドラがどうにかして、dynticks_nohz() プロセスに対してアトミックに走り、かつ、grace_period() プロセスに対してはそうでないことを要求します。

幸運にも、Promela では、アトミック文から分岐して出ることができることがわかりました。このトリックを使えば、dynticks_nohz()を書きなおして、割り込みハンドラがフラグをセットして、dynticks_nohz() がそのフラグをアトミックにチェックし、そのフラグがセットされていない時だけ走るようにすれば良いです。これは、以下の C プリプロセッサマクロで、ラベルと Promela 文を引数に取るもので実現できます。

1 #define EXECUTE_MAINLINE(label, stmt) \

2 label: skip; \

3 atomic { \

4 if \

5 :: in_dyntick_irq -> goto label; \

6 :: else -> stmt; \

7 fi; \

8 } \

このマクロは以下のように使います。

EXECUTE_MAINLINE(stmt1, tmp = dynticks_progress_counter)

マクロの２行目は指定された文のラベルを作成します。３から８行目は in_dyntick_irq 変数をテストするアトミックブロックです。そしてもしこの変数が設定されて（割り込みハンドラがアクティブであることを示します）いれば、アトミックブロックから分岐して抜けて、ラベルに戻ります。そうでない時は、６行目で指定された文を実行します。全体としての効果は、割り込みがアクティブである時にはいつでも、メインラインの実行はストールすることです。それは期待通りです。

１２．７．２．５ 割り込みハンドラを検証する

最初のステップは、以下のように、dyntick_nohz() を、EXECUTE_MAINLINE() 形式に変換することです。

１１から１４行目のように、文のグループが EXECUTE_MAINLINE() に渡された時は、そのグループの全ての文はアトミックに実行することに注意するのは重要です。

クイッククイズ１２．１４

でももし、単一の EXECUTE_MAINLINE() グループにある文を、アトミックでなく実行する必要がある時はどうしますか？

クイッククイズ１２．１５

でももし、dynticks_nohz() プロセスが条件を持つ “if” あるいは “do”文を持ち、これらの構成物の文のボディが、アトミックでなく実行する必要がある時はどうしますか？

次のステップは、割り込みハンドラをモデルする dyntick_irq() プロセスを書くことです。

７から４８行目のループは、MAX_DYNTICK_LOOP_IRQ 数までの割り込みをモデルします。８と９行目がループ条件を作って、４５行目が制御変数を加算します。１０行目は、dyntick_nohz() に、割り込みハンドラが実行中であると伝えます。そして４５行目は、dyntick_nohz() に、このハンドラが完了したことを伝えます。４９行目は生きていることの検証に使います。dyntick_nohz() の対応する行と同様です。

クイッククイズ１２．１６

なぜ、４５と４６行目 (in_dyntick_irq = 0; と i++;) はアトミックに実行されるのですか？

１１から２５行目は rcu_irq_enter() をモデルし、２６と２７行目は __irq_enter() の関連する部分をモデルします。２８と２９行目は dyntick_nohz() の対応する行と同様に安全性を検証します。３０と３１行目は __irq_exit() の関連する部分をモデルし、最後に３２から４３行目は rcu_irq_exit() をモデルします。

クイッククイズ１２．１７

この dynticks_irq() プロセスがモデルできない割り込みの性質は何でしょう？

すると、grace_period プロセスはこうなります。

grace_period() の実装は前のとほとんど同じです。変更点は、１０行目で新しい割り込みカウントパラメタを加えたこと、１９と３９行目で新しい dyntick_irq_done 変数を加えて、生きていることのチェックに使うこと、そしてもちろん、２２と４２行目の最適化です。

このモデル (dyntickRCU-irqnn-ssl.spin) は約５０万の状態を持ち、エラー無しに合格する正しい検証ができます。しかしこのバージョンのモデルは、ネストした割り込みを扱いません。次の節で取り上げます。

１２．７．２．６ ネストした割り込みハンドラを検証する

ネストした割り込みハンドラをモデルするには、以下のように、dyntick_irq() のループのボディを分割します。

これは、前の dynticks_irq() プロセスと似ています。それは、５行目で二つ目のカウンタ変数 j を加え、i が割り込みハンドラに入った数を数え、 j が出た回数を数えます。７行目の outermost 変数は、安全性チェックのために gp_state 変数をサンプルする必要がある時を決めるのを助けます。１０と１１行目のループを抜けるチェックは、変更されて、指定された数の割り込みハンドラが出て、かつ、入ったことを要求します。そして i の加算は４１行めに移動しました。そこは割り込みに入ることのモデルの終わりです。

１３から１６行目は、outermost 変数を設定して、これがネストした割り込みのセットの一番外側であるかを示します。そして、dyntick_nohz() プロセスで使う in_dyntick_irq 変数を設定します。３４から４０行目は gp_state 変数の状態を捕捉します。ただし、一番外側の割り込みハンドラにいる時だけです。

４２行目は割り込みを出ることのモデルの do-loop 条件です。割り込みに入ったよりも少ない数だけ出るうちは、もう一つの割り込みから出ることは合法です。４２から５０行目は安全性条件をチェックします。ただし、一番外側の割り込みレベルから出る時だけです。最後に、６５から６８行目は割り込みから出るカウンタ j を加算して、これが一番外側の割り込みレベルであるならば in_dyntick_irq をクリアします。

このモデル (dyntickRCU-irq-ssl.spin) は、５０万を少し越える状態を持ち、エラー無しに合格する正しい検証ができます。しかしこのバージョンのモデルは、NMIを扱いません。次の節で取り上げます。

１２．７．２．７ NMIハンドラを検証する

割り込みに対して行った同じ一般的なアプローチをNMIにも取ります。NMIはネストしないことに注意下さい。すると以下の、dyntick_nmi() プロセスになります。

もちろん、NMIがあるという事実のため、他のコンポーネントにも修正が必要です。例えば、EXECUTE_MAINLINE() マクロは今回は、割り込みハンドラ (in_dyntick_irq) だけでなく、NMIハンドラ (in_dyntick_nmi) にも注意する必要があります。それは以下のように、dyntick_nmi_done 変数をチェックして行います。

さらに、dyntick_irq() が dyntick_nmi() を排他するのを許すために、 in_dyntick_nmi をチェックする EXECUTE_IRQ() マクロを導入する必要があります。

さらに以下のように、dyntick_irq() を EXECUTE_IRQ() を使うように変換する必要があります。

“if” 文は、オープンコードしたことに（例えば、１７から２９行目）注意下さい。さらに、厳密にローカルな状態を処理する文（５８行目のように）は、dyntick_nmi() を排他する必要はありません。

最後に、grace_period() に必要な変更は少しだけです。

１１行目で、新しい MAX_DYNTICK_LOOP_NMI パラメタのために printf() を追加しました。そして、２２と４４行目に、shouldexit の設定に dyntick_nmi_done を加えました。

このモデル (dyntickRCU-irq-nmi-ssl.spin) は、数億の状態を持ち、エラー無しに合格する正しい検証ができます。

クイッククイズ１２．１８

Paul はいつでも彼のコードをこのように苦痛に満ちたインクリメンタルなやり方で書くのですか？

１２．７．３ (再び)得られた教訓

この作業で、いくつかの教訓が(再び)得られました。

１ Promela と Spin は、割り込み／NMIハンドラの相互作用も検証できます。

２ コードをドキュメント化するのは、バグを探す役に立ちます。この場合、図１２.１６で示したパッチにあるように、ドキュメント化の努力は、rcu_enter_nohz() と rcu_exit_ nohz() にある、メモリバリアの位置の誤りを見つけました。

３ あなたのコードを、早くから、しばしば、そしてそれを捨てるその時まで、検証しなさい。この努力は、図１２.１７で示したパッチにあるように、rcu_try_flip_waitack_needed() にある、テストとデバッグがとても難しい、一つのかすかなバグを見つけました。

４ 常にあなたの検証コードを検証しなさい。これを行う通常の方法は、注意深く作られたバグを入れて、検証コードがそれを捕まえるのを確認することです。もちろん、検証コードがこのバグを捕まえることができなかったら、そのバグ自体を見直さないといけません。などなど、これは永遠に続くかもしれません。しかし、あなたがこのような状況におちいったならば、一晩、ぐっすり眠るのがとても効果的なデバッグテクニックかもしれません。

５ アトミック命令を使うことで検証は簡単になることがあります。不幸にも、cmpxchg アトミック命令を使うのは、クリティカルな割り込みの高速パスを遅くしてしまうので、今の場合には適切ではありません。

６ 複雑な形式的検証が必要だということは、しばしば、あなたの設計を考え直す必要があることを示します。実際、この節で検証された設計は、ずっと単純な解決策があることがわかりました。それについては次の節で。

１２．８ 単純ならば形式的検証はいりません

プリエンプト可能RCUのための dynticks インタフェースが複雑なのは、主に、割り込みとNMIが同じコードパスと同じ変数を使っているからです。これは、割り込みとNMIで別々のコードパスと変数を使ったらどうかという考えに結びつきます。それは、階層RCUで行われたことであり、Manfred Spraul が間接的に示唆しました。

１２．８．１ 単純化された dynticks インタフェースのための状態変数

図１２.１８は、新しいCPUごとの状態変数です。これらの変数は、複数の独立したRCU実装(例えば、 rcu と rcu_bh )が、dynticks 状態を簡単かつ効率的に共用することができるように、構造体にグループされています。以下で、これらは独立のCPUごと変数と考えることができます。

dynticks_nesting, dynticks, と dynticks_snap 変数は、割り込みコードパスのためで、dynticks_nmi と dynticks_nmi_snap 変数はNMIコードパスのためです。なお、NMIコードパスは、dynticks_nesting 変数も参照(しかし更新はしません)します。これらの変数はこのように使います。

・dynticks_nesting: これは、対応するCPUがRCUリード側クリティカルセクションのために監視されるべき理由の数を数えます。そのCPUが dynticks-idle モードの時、これは割り込みネストレベルの数です。そうでない時は、割り込みネストレベルより一つ大きいです。

・dynticks: このカウンタの値は、対応するCPUが dynticks-idle モードにあって、そのCPUで現在実行中の割り込みハンドラがいない時に、偶数です。そうでない時、カウンタの値は奇数です。言葉を代えて言えば、このカウンタが奇数なら、対応するCPUはRCUリード側クリティカルセクションにいるかもしれません。

・dynticks_nmi:このカウンタの値は、対応するCPUがNMIハンドラにいる時に奇数です。ただし、そのCPUが dynticks-idle モードにあって割り込みハンドラが実行中でない時にNMIが届いた時に限ります。そうでない時、カウンタの値は偶数です。

・dynticks_snap: これは、dynticks カウンタのスナップショットです。ただし、現在のRCUグレースピリオドが長く走りすぎた時に限ります。

・dynticks_nmi_snap: これは、dynticks_nmi のスナップショットです。ただし、前と同じく現在のRCUグレースピリオドが長く走りすぎた時に限ります。

ある時間間隔の間に dynticks と dynticks_nmi の両方が偶数を持っていたら、対応するCPUはその時間の間に静止状態を通り過ぎました。

クイッククイズ１２．１９

でも、もしNMIハンドラがある割り込みハンドラが完了する前に走り出して、そのNMIハンドラが二つ目の割り込みハンドラが始まるまで走り続けたらどうなりますか？

１２．８．２ Dynticks-Idle モードに入ることと出ること

図１２．１９は rcu_enter_nohz() and rcu_exit_nohz() で、"nohz" モードとも呼ばれる dynticks-idle モードに出入りします。これら二つの関数はプロセスコンテキストから呼ばれます。

６行目は、以前の全てのメモリアクセス（それにはRCUリード側クリティカルセクションからのアクセスも含むかもしれません）が、以下の dynticks-idle モードに入ったことをしるしづける前に、他のCPUから見えることを保証します。７と１２行目は割り込みを無効にして、再度有効にします。８行目は、現在CPUの rcu_dynticks 構造体へのポインタを得て、９行目は現在CPUの dynticks カウンタを加算します。それは、私達がプロセスコンテキストから dynticks-idle モードに入っていることからして、偶数になったはずです。最後に、１０行目は dynticks_nesting を減算します。それはゼロになったはずです。

rcu_exit_nohz() 関数はとても似ていますが、dynticks_nesting を減算ではなく加算し、dynticks の極性も反対をチェックします。

１２．８．３ dynticks-idle モードからNMI

図１２．２０は、rcu_nmi_enter() と rcu_nmi_exit() です。これはそれぞれ、dynticks-idle モードからNMIに出入りするのをRCUに伝えます。しかし、もしNMIが割り込みハンドラの実行中に届いたら、RCUは既にこのCPUのRCUリード側クリティカルセクションの監視にあたっていますから、rcu_nmi_enter の６と７行目と、rcu_nmi_exit の１８と１９行目は、dynticks が奇数なら、静かに戻ります。そうでない時は、２つの関数は dynticks_nmi を加算します。rcu_nmi_enter() はそれを奇数に、rcu_nmi_exit() はそれを偶数にします。どちらの関数もそれぞれ１０と２０行目で、この加算と潜在的なRCUリード側クリティカルセクションの間にメモリバリアを実行します。

１２．８．４ dynticks-idle モードから割り込み

図１２．２１は、rcu_irq_enter() と rcu_irq_exit() です。それは、RCUに、割り込みコンテキストへの出入りをそれぞれ伝えます。rcu_irq_enter() の６行目は dynticks_nesting を加算して、もしこの変数が既にゼロでないならば、７行目は静かに戻ります。そうでない時は、８行目は dynticks を加算します。するとそれは奇数を持ちます。このCPUがRCUリード側クリティカルセクションを実行できるようになったこととつじつまが合います。なので１０行目はメモリバリアを実行して、dynticks の加算が、以下の割り込みハンドラが実行するかもしれない全てのRCUリード側クリティカルセクションの前に見える事を保証します。

rcu_irq_exit の１８行目は dynticks_nesting を減算して、結果がゼロでないならば、１９行目は静かに戻ります。そうでない時は、２０行目はメモリバリアを実行して、２１行目の dynticks の加算が以前の割り込みハンドラが実行したかもしれない全てのRCUリード側クリティカルセクションの後に見えることを保証します。２２行目は、dynticks が偶数になったことを確認します。それは、dynticks-idle モードではRCUリード側クリティカルセクションが現れないこととつじつまが合います。２３から２５行目は以前の割り込みハンドラがRCUコールバックをエンキューしたかをチェックします。もしそうならば、再スケジュール IPI を使って、このCPUを強制的に dynticks-idle モードから抜けさせます。

１２．８．５ dynticks 静止状態を判定する

図１２．２２は、dyntick_save_progress_counter() です。これは、指定したCPUのdynticks と dynticks_nmi カウンタのスナップショットを取ります。８と９行目でこの二つの変数をローカル変数にスナップショットします。１０行目でメモリバリアを実行します。これは、図１２．１９，１２．２０，１２．２１にある関数のメモリバリアと対になるものです。１１と１２行目で、後で使うためにスナップショットをrcu_implicit_dynticks_qs に記録します。そして１３と１４行目でそのCPUがdynticks-idle モードにあって、割り込みもNMIも実行中でない（言葉を代えて言えば、どちらのスナップショットも偶数値を持つ）ため、拡張された静止状態にあることをチェックします。そうならば、１５と１６行目でこのイベントを数え、１７行目はCPUが静止状態にあったならば真を返します。