Draft API for the general-purpose model checker #411

dmitrii-artuhov · 2024-10-07T14:04:01Z

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 · 2024-10-07T16:03:50Z

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

src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt

src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt

src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt

...rg/jetbrains/kotlinx/lincheck_test/representation/AtomicReferencesNamesRunWithLambdaTests.kt

...11/org/jetbrains/kotlinx/lincheck_test/representation/BaseRunWithLambdaRepresentationTest.kt

src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt

...jdk11/org/jetbrains/kotlinx/lincheck_test/representation/RunWithLambdaRepresentationTests.kt

dmitrii-artuhov · 2025-01-16T17:13:28Z

@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 · 2025-01-16T20:47:42Z

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 · 2025-01-22T00:00:06Z

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 · 2025-01-22T14:30:39Z

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.

src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt

ndkoval · 2025-01-23T19:38:06Z

src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt

+        val strategy = testCfg.createStrategy(GeneralPurposeMCWrapper::class.java, scenario, null, null)
+        val verifier = testCfg.createVerifier()
+
+        for (i in 1..invocations) {


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

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.

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

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

ndkoval · 2025-01-23T19:40:29Z

src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt

+ */
+fun <R> runConcurrentTest(
+    invocations: Int = DEFAULT_INVOCATIONS_COUNT,
+    block: () -> R


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

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

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

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

src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt

.../test/org/jetbrains/kotlinx/lincheck_test/representation/RunWithLambdaRepresentationTests.kt

...m/test/org/jetbrains/kotlinx/lincheck_test/representation/CustomThreadsRepresentationTest.kt

src/jvm/test/resources/expected_logs/array_rw_run_with_lambda.txt

src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt

… under mc

…yWithModelChecking' call

Signed-off-by: Evgeniy Moiseenko <[email protected]>

src/jvm/test/resources/expected_logs/run_concurrent_test/array_rw.txt

src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt

Signed-off-by: Evgeniy Moiseenko <[email protected]>

…cks) GOD FORGIVE ME FOR THIS CODE Signed-off-by: Evgeniy Moiseenko <[email protected]>

Signed-off-by: Evgeniy Moiseenko <[email protected]>

ndkoval · 2025-01-27T22:40:10Z

src/jvm/test/resources/expected_logs/run_concurrent_test/kotlin_thread.txt

@@ -0,0 +1,42 @@
+= Concurrent test failed =


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

I would leave it.

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.

Currently there are two possible lines:

= Concurrent test failed =

= Concurrent test has hung =

Signed-off-by: Evgeniy Moiseenko <[email protected]>

dmitrii-artuhov requested a review from eupp October 7, 2024 14:04

dmitrii-artuhov self-assigned this Oct 7, 2024

dmitrii-artuhov marked this pull request as draft October 7, 2024 14:04

dmitrii-artuhov changed the title ~~[Draft] Lincheck new API function~~ Lincheck new API function Oct 17, 2024

ndkoval changed the title ~~Lincheck new API function~~ API for the general-purpose model checker Nov 25, 2024

eupp requested changes Nov 25, 2024

View reviewed changes

dmitrii-artuhov force-pushed the run-with-lincheck-api branch from 9e0d1fa to 426aa8a Compare December 17, 2024 12:23

eupp requested changes Jan 8, 2025

View reviewed changes

dmitrii-artuhov marked this pull request as ready for review January 14, 2025 12:46

dmitrii-artuhov requested a review from eupp January 14, 2025 13:01

eupp requested changes Jan 15, 2025

View reviewed changes

src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt Outdated Show resolved Hide resolved

...jdk11/org/jetbrains/kotlinx/lincheck_test/representation/RunWithLambdaRepresentationTests.kt Outdated Show resolved Hide resolved

dmitrii-artuhov force-pushed the run-with-lincheck-api branch from 91168ea to 0c0e25c Compare January 16, 2025 16:49

dmitrii-artuhov requested a review from eupp January 16, 2025 16:51

eupp force-pushed the run-with-lincheck-api branch from 3c3d5d8 to 951e45a Compare January 21, 2025 23:56

eupp requested a review from ndkoval January 22, 2025 16:48

eupp approved these changes Jan 22, 2025

View reviewed changes

ndkoval requested changes Jan 23, 2025

View reviewed changes

eupp mentioned this pull request Jan 24, 2025

Prevent IllegalArgumentException #421

Merged

dmitrii-artuhov added 7 commits January 25, 2025 00:43

Add 'verifyWithModelChecker' function for running user arbitrary code…

30a6f60

… under mc

Remove 'createVerifier' extension function

82f41bd

Add PR fixes

1418c46

Add tests

010359e

Rebase to develop

72cb0ad

Move representation tests to jdk11

5df6b3f

Add some PR fixes

55dfb74

dmitrii-artuhov and others added 18 commits January 25, 2025 00:43

Distinguish failed check's between lincheck internal error and 'verif…

f8b55e1

…yWithModelChecking' call

Fix naming

984b72d

Add PR fixes

3169a38

Remove old expected logs

bcbec7b

Refactor tests

ece59f3

fix runConcurrentTest kdoc

480e716

Signed-off-by: Evgeniy Moiseenko <[email protected]>

increase the default number of invocations for runConcurrentTest

cd51538

Signed-off-by: Evgeniy Moiseenko <[email protected]>

make runConcurrentTest throw LincheckAssertionError

3f48ef2

Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor

a8ae164

Signed-off-by: Evgeniy Moiseenko <[email protected]>

repair AtomicReferencesNamesRunWithLambdaTest trace

ad6b6b4

Signed-off-by: Evgeniy Moiseenko <[email protected]>

rename auxiliary verifier to NoExceptionVerifier, re-word kdoc

acf78f1

Signed-off-by: Evgeniy Moiseenko <[email protected]>

optimize imports

839ee30

Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor changes

c37d89f

Signed-off-by: Evgeniy Moiseenko <[email protected]>

renamed *RunConcurrentRepresentationTest tests

3773bcc

Signed-off-by: Evgeniy Moiseenko <[email protected]>

implement a hack to not show internal wrapper run method in the trace

6bab457

Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor

9325fe5

Signed-off-by: Evgeniy Moiseenko <[email protected]>

add opt-in annotation for the experimental API

67a4efe

Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor

ba7d010

Signed-off-by: Evgeniy Moiseenko <[email protected]>

eupp force-pushed the run-with-lincheck-api branch from 5ef8842 to ba7d010 Compare January 24, 2025 23:44

eupp requested a review from ndkoval January 25, 2025 01:19

ndkoval requested changes Jan 27, 2025

View reviewed changes

eupp added 3 commits January 27, 2025 21:46

minor

3658f71

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fixed indentation for gpmc trace printing (through some horrendous ha…

ea16ee4

…cks) GOD FORGIVE ME FOR THIS CODE Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix report header for gpmc

47befec

Signed-off-by: Evgeniy Moiseenko <[email protected]>

ndkoval reviewed Jan 27, 2025

View reviewed changes

quickfix

9dd64a2

Signed-off-by: Evgeniy Moiseenko <[email protected]>

ndkoval approved these changes Jan 28, 2025

View reviewed changes

ndkoval merged commit d5ff599 into develop Jan 28, 2025
18 checks passed

ndkoval deleted the run-with-lincheck-api branch January 28, 2025 09:48

ndkoval changed the title ~~API for the general-purpose model checker~~ Draft API for the general-purpose model checker Jan 28, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Draft API for the general-purpose model checker #411

Draft API for the general-purpose model checker #411

dmitrii-artuhov commented Oct 7, 2024 •

edited by eupp

Loading

eupp commented Oct 7, 2024

dmitrii-artuhov commented Jan 16, 2025 •

edited

Loading

eupp commented Jan 16, 2025

eupp commented Jan 22, 2025

eupp commented Jan 22, 2025 •

edited

Loading

ndkoval Jan 23, 2025

eupp Jan 24, 2025 •

edited

Loading

ndkoval Jan 27, 2025

ndkoval Jan 27, 2025

ndkoval Jan 23, 2025

eupp Jan 24, 2025 •

edited

Loading

ndkoval Jan 27, 2025

ndkoval Jan 27, 2025

ndkoval Jan 27, 2025

eupp Jan 27, 2025

Draft API for the general-purpose model checker #411

Draft API for the general-purpose model checker #411

Conversation

dmitrii-artuhov commented Oct 7, 2024 • edited by eupp Loading

Description:

Additional improvements to the PR:

eupp commented Oct 7, 2024

dmitrii-artuhov commented Jan 16, 2025 • edited Loading

eupp commented Jan 16, 2025

eupp commented Jan 22, 2025

eupp commented Jan 22, 2025 • edited Loading

Choose a reason for hiding this comment

eupp Jan 24, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eupp Jan 24, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dmitrii-artuhov commented Oct 7, 2024 •

edited by eupp

Loading

dmitrii-artuhov commented Jan 16, 2025 •

edited

Loading

eupp commented Jan 22, 2025 •

edited

Loading

eupp Jan 24, 2025 •

edited

Loading

eupp Jan 24, 2025 •

edited

Loading