不変式

コードロックとデータロックについて、複雑なロックを制御するためには「不変式」が重要な意味をもちます。不変式とは、常に真である条件または関係のことです。

不変式は、並行実行環境に対して次のように定義されます。すなわち不変式とは、関連するロックが行われるときに条件や関係が真になっていることです。ロックが行われた後は偽になってもかまいません。ただし、ロックを解除する前に真に戻す必要があります。

あるロックが行われるときに真となるような条件または関係も不変式です。条件変数では、条件という不変式を持っていると考えることができます。

例 9-4 assert(3X) による不変式のテスト

    mutex_lock(&lock);
    while((condition)==FALSE)
        cond_wait(&cv,&lock);
    assert((condition)==TRUE);
      .
      .
      .
    mutex_unlock(&lock);

上記の assert() 文は、不変式を評価しています。cond_wait() 関数は、不変式を保存しません。このため、スレッドが戻ったときに不変式をもう一度評価しなければなりません。

他の例は、双方向リンクリストを管理するモジュールです。双方向リンクリストでは、直前の項目の前向きポインタと直後の項目の後ろ向きポインタが同じものを指すという条件が成立します。これは不変式のよい例です。

このモジュールでコードロックを使用するものと仮定し、1 つの広域的な相互排他ロック (mutex ロック) でモジュールを保護することにします。項目を削除したり追加したりするときは相互排他ロックを獲得し、ポインタの変更後に相互排他ロックを解除します。明らかに、この不変式はポインタの変更中のある時点で偽になります。しかし、相互排他ロックを解除する前に真に戻されています。