Kotlin Help

Progress guarantees

Many concurrent algorithms provide non-blocking progress guarantees, such as wait-freedom, lock-freedom, or obstruction-freedom.

Lincheck only supports verification of obstruction-freedom. However, because lock-free and wait-free algorithms are also obstruction-free, any violation of obstruction-freedom also indicates a violation of those stronger guarantees.

Use the checkObstructionFreedom option to verify the obstruction-freedom guarantee of the program:

@Test fun modelCheckingTest() = ModelCheckingOptions() .checkObstructionFreedom() .check(this::class)

Lincheck verifies obstruction-freedom by checking whether a thread can make progress when all other threads are paused. If a thread's execution gets stuck in a loop, Lincheck reports an active lock.

If certain functions are intentionally blocking, you can mark them with @Operation(blocking = true) to prevent false positives.

Example: test ConcurrentHashMap for obstruction-freedom

In this example, you will test the put() function of a ConcurrentHashMap structure.

  1. Create a ConcurrentHashMapTest.kt file.

  2. Create a test class for the ConcurrentHashMap structure and declare the put() function:

    class ConcurrentHashMapTest { private val map = ConcurrentHashMap<Int, Int>() @Operation fun put(key: Int, value: Int) = map.put(key, value) }

  3. Declare a test function with the checkObstructionFreedom() option enabled:

    @Test fun modelCheckingTest() = ModelCheckingOptions() .checkObstructionFreedom() .threads(2) .actorsPerThread(1) .check(this::class)

    The threads and actorsPerThread options are used to reduce the number of potential execution scenarios. These options do not change the pass/fail state of the test, but they significantly reduce the testing time.

  4. Run the test. It should fail with the following report:

    = 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> | | -------------------------------------------------------------------------------------------------------------- |

  5. Add the blocking = true option to the put() function annotation:

    @Operation(blocking = true) fun put(key: Int, value: Int) = map.put(key, value)

  6. Rerun the test. It should pass successfully.

Example: test ConcurrentSkipListMap for obstruction-freedom

In this example, you will test the put() function of a non-blocking ConcurrentSkipListMap structure.

  1. Create a ConcurrentSkipListMapTest.kt file.

  2. Create a test class for the ConcurrentSkipListMap structure and declare the put() function:

    class ConcurrentSkipListMapTest { private val map = ConcurrentSkipListMap<Int, Int>() @Operation fun put(key: Int, value: Int) = map.put(key, value) }

  3. Declare a test function with the checkObstructionFreedom() option enabled:

    @Test fun modelCheckingTest() = ModelCheckingOptions() .checkObstructionFreedom() .check(this::class)

  4. Run the test. It should pass successfully.

See also

24 July 2026
Operation execution optionsResults verification and validation