API for the general-purpose model checker

[dmitrii-artuhov]

Description:

PR adds function for running lincheck model checker algorithm on arbitrary code via lambda body.
Usage example:

class JunitTest {
  val invocations = 100
  @Test
  fun test() = runConcurrentTest(invocations) {
    var counter = 0
    val t1 = thread { counter++ }
    val t2 = thread { counter++ }
    t1.join(); t2.join()
    check(counter == 2) // will detect an error an throw an exception
  }
}

Additional improvements to the PR:

• tests on java - bug arised ⚰️ Impossible to instrument the body of runConcurrentTest when it is used from java #445
• make a different default invocations count (more than lincheck does for data-structures testing)
• make runConcurrentTest throw AssertionError instead of returning it
• tests with thread pool (created inside a lambda body)
• tests with simple coroutines usage

[eupp]

@dmitrii-artuhov thanks for the PR.
Could you please repair the CI before we start reviewing this.

[eupp]

As discussed with @ndkoval .

For now, lets rename this function into runConcurrentTest, and make it top-level function (no Lincheck object needed). This is not a final name, we will discuss API of this function (including its name) in more detail before public release of this feature.

[eupp]

There are also tests in CustomThreadsRepresentationTest.kt file that I have added when I was working on supporting custom threads. Could you please move them in this file, rewrite them to use verifyWithModelChecker function and check that they would still work?

[dmitrii-artuhov]

@eupp I added the testClassInstance parameter to the runConcurrentTest function, because right now I utilize a specifal wrapper class which calls the lambda and only this wrapper is recreated between iterations, not the user class which might contain fields that are modified. Since on trace collection there are in total 2 iterations, then I need to restore the fields of the actual user test class. Required functionality was added to the SnapshotTracker class, so that it restores the user test class instance between iterations.

[eupp]

I added the testClassInstance parameter to the runConcurrentTest function

Let's please revert this change. The API should be as simple as it could be, that is the point why we adding it. It should only take the lambda to run and that's it.

I utilize a specifal wrapper class which calls the lambda and only this wrapper is recreated between iterations, not the user class which might contain fields that are modified.

To make the test work with only the lambda, please remove any state of the test class by either:

• making the respective fields static, or
• promoting the fields to regular variables inside lambda.

Use one method or another, depending on which makes more sense for a particular test.

This way we will eliminate any "external" state outside lambda (except static state, but it will be handled by the snapshot tracker).

In general, there is indeed a problem here --- the problem is that the lambda that we pass to the model checker should not capture any state, in order to be deterministically reproducible.
I will add this problem to the design document, and we will discuss it and possible solutions separately.

One of possible solutions is similar to what you propose --- to force the user to explicitly mention all captured objects as method parameters. But we need to discuss this solution and how to express it in the API in more detail before implementing it.