Progress guarantees

Many concurrent algorithms provide non-blocking progress guarantees, such as lock-freedom and wait-freedom. As they are usually non-trivial, it's easy to add a bug that blocks the algorithm. Lincheck can help you find liveness bugs using the model checking strategy.

To check the progress guarantee of the algorithm, enable the checkObstructionFreedom option in ModelCheckingOptions():

ModelCheckingOptions().checkObstructionFreedom()

For example, consider ConcurrentHashMap<K, V> from the Java standard library. Here is the Lincheck test to detect that put(key: K, value: V) is a blocking operation:

class ConcurrentHashMapTest {
    private val map = ConcurrentHashMap<Int, Int>()

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

    @Test
    fun modelCheckingTest() = ModelCheckingOptions()
        .actorsBefore(1) // To init the HashMap
        .actorsPerThread(1)
        .actorsAfter(0)
        .minimizeFailedScenario(false)
        .checkObstructionFreedom()
        .check(this::class)
}

Run the modelCheckingTest(). You should get the following result:

= Obstruction-freedom is required but a lock has been found =
Execution scenario (init part):
[put(2, 6)]
Execution scenario (parallel part):
| put(-6, -8) | put(1, 4) |

= The following interleaving leads to the error =
Parallel part trace:
|                                                                                          | put(1, 4)                                                                                |
|                                                                                          |   put(1,4) at ConcurrentHashMapTest.put(ConcurrentMapTest.kt:34)                         |
|                                                                                          |     putVal(1,4,false) at ConcurrentHashMap.put(ConcurrentHashMap.java:1006)              |
|                                                                                          |       table.READ: Node[]@1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1014)      |
|                                                                                          |       tabAt(Node[]@1,0): Node@1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1018) |
|                                                                                          |       MONITORENTER at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1031)              |
|                                                                                          |       tabAt(Node[]@1,0): Node@1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1032) |
|                                                                                          |       next.READ: null at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1046)           |
|                                                                                          |       switch                                                                             |
| put(-6, -8)                                                                              |                                                                                          |
|   put(-6,-8) at ConcurrentHashMapTest.put(ConcurrentMapTest.kt:34)                       |                                                                                          |
|     putVal(-6,-8,false) at ConcurrentHashMap.put(ConcurrentHashMap.java:1006)            |                                                                                          |
|       table.READ: Node[]@1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1014)      |                                                                                          |
|       tabAt(Node[]@1,0): Node@1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1018) |                                                                                          |
|       MONITORENTER at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1031)              |                                                                                          |
|                                                                                          |       MONITOREXIT at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1065)               |

Now let's write a test for the non-blocking ConcurrentSkipListMap<K, V>, expecting the test to pass successfully:

class ConcurrentSkipListMapTest {
    private val map = ConcurrentSkipListMap<Int, Int>()

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

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

At the moment, Lincheck supports only the obstruction-freedom progress guarantees. However, most real-life liveness bugs add unexpected blocking code, so the obstruction-freedom check will also help with lock-free and wait-free algorithms.

Next step

Learn how to specify the sequential specification of the testing algorithm explicitly, improving the Lincheck tests robustness.