New API for general-purpose model checking

[eupp]

One of the features of Lincheck framework is the concurrent code model checker.

Currently the model checker functionality in Lincheck is toughly coupled with the Lincheck's data structures testing API. This approach has its benefits: it provides a convenient end-to-end testing experience for users who want to test their concurrent data structures. However, for some use cases it is less convenient: sometimes users just want to run a piece of concurrent code in a model checking mode, exploring different possible interleavings.

Some examples of code that cannot be easily tested currently with Lincheck are thread pool implementations, parallel executors, coroutine schedulers, etc.

We aim to provide a simpler API to run model checker on an arbitrary code snippet (subject to a few constraints).

Overview of the API

Here is how the current data structures model checking API looks like:

class Counter {
    @Volatile
    private var value = 0

    fun inc(): Int = ++value
    fun get() = value
}

class BasicCounterTest {
    // Initial state

    private val c = Counter() 

    // Operations on the Counter

    @Operation
    fun inc() = c.inc()

    @Operation
    fun get() = c.get()

    // Test set-up

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

Here is how a concrete test for the counter with the general-purpose model checking API would look like:

class BasicCounterTest {

    @Test
    fun modelCheckingTest() = runWithModelChecker(invocations = 100) {
        val c = Counter()
        val t1 = thread {
            c.inc()
        }
        val t2 = thread {
            c.inc()
        }
        t1.join()
        t2.join()
        check(c.get() == 2)
    }
}

The concrete API is under discussion, but the general idea should stay the same.

[eupp]

There is a soft dependency on #387 : until we implement it, it would be possible to test only single threaded code (useless). But we still can start prototyping and developing this feature independently, and then merge with the custom threads support.