プログレス保証
多くの並行アルゴリズムは、ウェイト・フリーダム（wait-freedom）、ロック・フリーダム（lock-freedom）、またはオブストラクション・フリーダム（obstruction-freedom）などのノンブロッキング・プログレス保証を提供しています。
Lincheckは、オブストラクション・フリーダムの検証のみをサポートしています。しかし、ロック・フリーやウェイト・フリーのアルゴリズムはオブストラクション・フリーでもあるため、オブストラクション・フリーダムへのいかなる違反も、それらのより強力な保証への違反を意味します。
checkObstructionFreedomオプションを使用して、プログラムのオブストラクション・フリーダム保証を検証します。
@Test
fun modelCheckingTest() = ModelCheckingOptions()
.checkObstructionFreedom()
.check(this::class)
checkObstructionFreedomオプションは、モデル・チェック戦略でのみ利用可能です。
Lincheckは、他のすべてのスレッドが一時停止しているときにスレッドが進行できるかどうかをチェックすることで、オブストラクション・フリーダムを検証します。スレッドの実行がループでスタック（stuck in a loop）した場合、Lincheckはアクティブなロックを報告します。
特定の関数が意図的にブロッキングである場合は、@Operation(blocking = true)でマークすることで誤検知を防ぐことができます。
例: ConcurrentHashMap のオブストラクション・フリーダムのテスト
この例では、ConcurrentHashMap 構造の put() 関数をテストします。
ConcurrentHashMapTest.ktファイルを作成します。ConcurrentHashMap構造のテストクラスを作成し、put()関数を宣言します。kotlinclass ConcurrentHashMapTest { private val map = ConcurrentHashMap<Int, Int>() @Operation fun put(key: Int, value: Int) = map.put(key, value) }checkObstructionFreedom()オプションを有効にしたテスト関数を宣言します。kotlin@Test fun modelCheckingTest() = ModelCheckingOptions() .checkObstructionFreedom() .threads(2) .actorsPerThread(1) .check(this::class)threadsおよびactorsPerThreadオプションは、潜在的な実行シナリオの数を減らすために使用されます。これらのオプションはテストの合否結果を変えるものではありませんが、テスト時間を大幅に短縮します。テストを実行します。以下のレポートとともに失敗するはずです。
text= The algorithm should be non-blocking, but an active lock is detected = | --------------------- | | Thread 1 | Thread 2 | | --------------------- | | put(1, 0) | put(1, 1) | | --------------------- | The following interleaving leads to the error: | -------------------------------------------------------------------------------------------------------------- | | Thread 1 | Thread 2 | | -------------------------------------------------------------------------------------------------------------- | | put(1, 0): <hung> | | | map.put(1, 0) | | | putVal(1, 0, false) | | | spread(1): 1 | | | table ➜ null | | | loop(1 iterations) at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1016) | | | <iteration 1> | | | initTable() | | | loop(1 iterations) at ConcurrentHashMap.initTable(ConcurrentHashMap.java:2293) | | | table ➜ null | | | switch | | | | put(1, 1): <hung> | | -------------------------------------------------------------------------------------------------------------- |put()関数のアノテーションにblocking = trueオプションを追加します。kotlin@Operation(blocking = true) fun put(key: Int, value: Int) = map.put(key, value)テストを再実行します。正常にパスするはずです。
例: ConcurrentSkipListMap のオブストラクション・フリーダムのテスト
この例では、ノンブロッキングな ConcurrentSkipListMap 構造の put() 関数をテストします。
ConcurrentSkipListMapTest.ktファイルを作成します。ConcurrentSkipListMap構造のテストクラスを作成し、put()関数を宣言します。kotlinclass ConcurrentSkipListMapTest { private val map = ConcurrentSkipListMap<Int, Int>() @Operation fun put(key: Int, value: Int) = map.put(key, value) }checkObstructionFreedom()オプションを有効にしたテスト関数を宣言します。kotlin@Test fun modelCheckingTest() = ModelCheckingOptions() .checkObstructionFreedom() .check(this::class)テストを実行します。正常にパスするはずです。