Draft 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:

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

[eupp]

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

[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.

[eupp]

The task to add support for thread pools turned out to be more challenging than anticipated, and it required non-trivial changes. I transferred it into separate PR so we can review and discuss that code separately: #447

[eupp]

I've tried to add tests with coroutines, using custom thread pool as a dispacther, using ExecutorService.asCoroutineDispatcher(): https://kotlinlang.org/api/kotlinx.coroutines/kotlinx-coroutines-core/kotlinx.coroutines/as-coroutine-dispatcher.html.

But it seems I run into bug #404 with this test, so I am going to try debug and fix it first.

[ndkoval]

Why do we need to implement this logic again? Can't we just call options.checkImpl instead?

[eupp]

Unfortunately, just using options.checkImpl currently does not work.
The problem is that we need to manually trigger the instrumentation of the passed lambda class:

ensureObjectIsTransformed(block)

Otherwise, it is not triggered automatically, with the current implementation of ensureObjectIsTransformed and ensureClassHierarchyIsTransformed. This is because instead of the lambda itself, we pass the GeneralPurposeModelCheckingWrapper object to make the whole thing work with the scenario-based Lincheck API. So only this class is transformed. Because this class does not store block lambda in any of its fields, but instead is passed as actor argument, its instrumentation is not triggered automatically.

I propose we implement the required refactoring in a separate PR, because it would touch a lot of places in the code (LinChecker.kt, runners, managed strategy, LincheckJavaAgent, etc).

In a meantime, I changed the code to use Strategy.runIteration. It is not as good, but still simplifies the code and avoids unnecessary duplication.

[ndkoval]

Would storing the lambda in GeneralPurposeModelCheckingWrapper solve the issue and simplify the logic?

[ndkoval]

Oh, I see why not -- GeneralPurposeModelCheckingWrapper must have an empty constructor.

[ndkoval]

Please add a test on Java, with and without invocations, to check the API.

[eupp]

Unfortunately, using this API from Java is currently unsupported due to technical limitations: #445

[ndkoval]

Yes, so let's ignore the test. However, we need to see what the code looks like in Java.

[ndkoval]

Note: as we are not working on the API now, we can postpone this question.

[ndkoval]

Do we need this line, or should we start the output with the exception?

[eupp]

I would leave it.

1. It is a title of the whole report, explaining what happened. Starting with the exception might be confusing, as if the code itself thrown an exception.

2. Currently there are two possible lines:

= Concurrent test failed =

= Concurrent test has hung =