コードロックでもデータロックでも、複雑なロックを制御するためには「不変式」が重要な意味をもちます。不変式とは、常に真である条件または関係のことです。
不変式は、並行実行環境に対して次のように定義されます。 すなわち不変式とは、関連するロックが行われるときに条件や関係が真になっていることです。ロックが行われた後は偽になってもかまいません。ただし、ロックを解除する前に真に戻す必要があります。
あるロックが行われるときに真となるような条件または関係も不変式です。条件変数では、条件という不変式を持っていると考えることができます。
mutex_lock(&lock); while((condition)==FALSE) cond_wait(&cv,&lock); assert((condition)==TRUE); . . . mutex_unlock(&lock);
この assert() 文は、不変式を評価しています。cond_wait() 関数は、不変式を保存しません。このため、スレッドが戻ったときに不変式をもう一度評価しなければなりません。
ほかの例は、双方向リンクリストを管理するモジュールです。双方向リンクリストの各項目で、直前の項目の前向きポインタは不変式のよい例になります。この前向きポインタは、直後の項目の後ろ向きポインタと同じ要素を指します。
このモジュールでコードロックを使用するものと仮定し、1 つの大域的な相互排他ロックでモジュールを保護することにします。項目を削除したり追加したりするときは相互排他ロックを獲得し、ポインタの変更後に相互排他ロックを解除します。明らかに、この不変式はポインタ操作中のある時点で偽になります。しかし、相互排他ロックを解除する前に真に戻されています。