Trace collection in stress mode

build.gradle.kts

@@ -93,6 +93,7 @@ tasks {
     withType<Test> {
         maxParallelForks = 1
         jvmArgs(
+            "-Xmx1G",
             "--add-opens", "java.base/jdk.internal.misc=ALL-UNNAMED",
             "--add-exports", "java.base/jdk.internal.util=ALL-UNNAMED",
             "--add-exports", "java.base/sun.security.action=ALL-UNNAMED"

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

@@ -9,6 +9,7 @@
  */
 package org.jetbrains.kotlinx.lincheck
 
+import org.jetbrains.kotlinx.lincheck.CTestConfiguration.Companion.DEFAULT_REPRODUCE_WITH_MODEL_CHECKING
 import org.jetbrains.kotlinx.lincheck.CTestConfiguration.Companion.DEFAULT_TIMEOUT_MS
 import org.jetbrains.kotlinx.lincheck.execution.*
 import org.jetbrains.kotlinx.lincheck.strategy.*
@@ -33,13 +34,14 @@ abstract class CTestConfiguration(
     val generatorClass: Class<out ExecutionGenerator>,
     val verifierClass: Class<out Verifier>,
     val minimizeFailedScenario: Boolean,
+    val reproduceWithModelChecking: Boolean,
     val sequentialSpecification: Class<*>,
     val timeoutMs: Long,
     val customScenarios: List<ExecutionScenario>
 ) {
     abstract fun createStrategy(
         testClass: Class<*>, scenario: ExecutionScenario, validationFunction: Actor?,
-        stateRepresentationMethod: Method?, verifier: Verifier
+        stateRepresentationMethod: Method?
     ): Strategy
 
     companion object {
@@ -51,6 +53,7 @@ abstract class CTestConfiguration(
         val DEFAULT_EXECUTION_GENERATOR: Class<out ExecutionGenerator?> = RandomExecutionGenerator::class.java
         val DEFAULT_VERIFIER: Class<out Verifier> = LinearizabilityVerifier::class.java
         const val DEFAULT_MINIMIZE_ERROR = true
+        const val DEFAULT_REPRODUCE_WITH_MODEL_CHECKING = true
         const val DEFAULT_TIMEOUT_MS: Long = 10000
     }
 }
@@ -69,6 +72,7 @@ internal fun createFromTestClassAnnotations(testClass: Class<*>): List<CTestConf
                 verifierClass = ann.verifier.java,
                 invocationsPerIteration = ann.invocationsPerIteration,
                 minimizeFailedScenario = ann.minimizeFailedScenario,
+                reproduceWithModelChecking = ann.reproduceWithModelChecking,
                 sequentialSpecification = chooseSequentialSpecification(ann.sequentialSpecification.java, testClass),
                 timeoutMs = DEFAULT_TIMEOUT_MS,
                 customScenarios = emptyList()

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

@@ -13,12 +13,15 @@ import org.jetbrains.kotlinx.lincheck.annotations.*
 import org.jetbrains.kotlinx.lincheck.execution.*
 import org.jetbrains.kotlinx.lincheck.strategy.*
 import org.jetbrains.kotlinx.lincheck.verifier.*
+import org.jetbrains.kotlinx.lincheck.strategy.managed.*
+import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
+import org.jetbrains.kotlinx.lincheck.strategy.stress.*
 import kotlin.reflect.*
 
 /**
  * This class runs concurrent tests.
  */
-class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
+class LinChecker(private val testClass: Class<*>, options: Options<*, *>?) {
     private val testStructure = CTestStructure.getFromTestClass(testClass)
     private val testConfigurations: List<CTestConfiguration>
     private val reporter: Reporter
@@ -50,80 +53,111 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
         check(testConfigurations.isNotEmpty()) { "No Lincheck test configuration to run" }
         for (testCfg in testConfigurations) {
             val failure = testCfg.checkImpl()
-            if (failure != null) return failure
+            if (failure != null)
+                return failure
         }
         return null
     }
 
     private fun CTestConfiguration.checkImpl(): LincheckFailure? {
-        val exGen = createExecutionGenerator(testStructure.randomProvider)
-        for (i in customScenarios.indices) {
-            val verifier = createVerifier()
-            val scenario = customScenarios[i]
-            scenario.validate()
-            reporter.logIteration(i + 1, customScenarios.size, scenario)
-            val failure = scenario.run(this, verifier)
-            if (failure != null) return failure
-        }
         var verifier = createVerifier()
-        repeat(iterations) { i ->
+        val generator = createExecutionGenerator(testStructure.randomProvider)
+        val randomScenarios = generateSequence {
+            generator.nextExecution().also {
+                // reset the parameter generator ranges to start with the same initial bounds for each scenario.
+                testStructure.parameterGenerators.forEach { it.reset() }
+            }
+        }
+        val scenarios = customScenarios.asSequence() + randomScenarios.take(iterations)
+        val scenariosSize = customScenarios.size + iterations
+        scenarios.forEachIndexed { i, scenario ->
+            val isCustomScenario = (i < customScenarios.size)
+            var iteration = i
             // For performance reasons, verifier re-uses LTS from previous iterations.
-            // This behaviour is similar to a memory leak and can potentially cause OutOfMemoryError.
+            // This behavior is similar to a memory leak and can potentially cause OutOfMemoryError.
             // This is why we periodically create a new verifier to still have increased performance
             // from re-using LTS and limit the size of potential memory leak.
             // https://github.com/Kotlin/kotlinx-lincheck/issues/124
-            if ((i + 1) % VERIFIER_REFRESH_CYCLE == 0)
+            if (iteration + 1 % VERIFIER_REFRESH_CYCLE == 0)
                 verifier = createVerifier()
-            val scenario = exGen.nextExecution()
             scenario.validate()
-            reporter.logIteration(i + 1 + customScenarios.size, iterations, scenario)
-            val failure = scenario.run(this, verifier)
-            if (failure != null) {
-                val minimizedFailedIteration = if (!minimizeFailedScenario) failure else failure.minimize(this)
-                reporter.logFailedIteration(minimizedFailedIteration)
-                return minimizedFailedIteration
+            reporter.logIteration(iteration, scenariosSize, scenario)
+            var failure = scenario.run(iteration, this, verifier)
+                ?: return@forEachIndexed
+            if (minimizeFailedScenario && !isCustomScenario) {
+                reporter.logScenarioMinimization(scenario)
+                verifier = createVerifier()
+                failure = failure.minimize { minimizedScenario ->
+                    minimizedScenario.run(++iteration, this, verifier)
+                }
+            }
+            val isStressMode = (this is StressCTestConfiguration)
+            if (isStressMode && reproduceWithModelChecking) {
+                // stress mode does not support trace reporting, so we attempt to reproduce the failure
+                // with the model checking mode and collect the trace
+                check(failure.trace == null)
+                reporter.logFailureReproduction(failure)
+                verifier = createVerifier()
+                failure = failure.tryReproduceInModelCheckingMode(++iteration, this, verifier) ?: failure
             }
-            // Reset the parameter generator ranges to start with the same initial bounds on each scenario generation.
-            testStructure.parameterGenerators.forEach { it.reset() }
+            reporter.logFailedIteration(failure)
+            return failure
         }
         return null
     }
 
-    // Tries to minimize the specified failing scenario to make the error easier to understand.
-    // The algorithm is greedy: it tries to remove one actor from the scenario and checks
-    // whether a test with the modified one fails with error as well. If it fails,
-    // then the scenario has been successfully minimized, and the algorithm tries to minimize it again, recursively.
-    // Otherwise, if no actor can be removed so that the generated test fails, the minimization is completed.
-    // Thus, the algorithm works in the linear time of the total number of actors.
-    private fun LincheckFailure.minimize(testCfg: CTestConfiguration): LincheckFailure {
-        reporter.logScenarioMinimization(scenario)
-        var minimizedFailure = this
-        while (true) {
-            minimizedFailure = minimizedFailure.scenario.tryMinimize(testCfg) ?: break
+    private fun ExecutionScenario.run(
+        iteration: Int,
+        testCfg: CTestConfiguration,
+        verifier: Verifier,
+    ): LincheckFailure? {
+        val strategy = testCfg.createStrategy(
+            testClass = testClass,
+            scenario = this,
+            validationFunction = testStructure.validationFunction,
+            stateRepresentationMethod = testStructure.stateRepresentation,
+        )
+        return strategy.use {
+            it.runIteration(iteration, testCfg.invocationsPerIteration, verifier)
         }
-        return minimizedFailure
     }
 
-    private fun ExecutionScenario.tryMinimize(testCfg: CTestConfiguration): LincheckFailure? {
-        // Reversed indices to avoid conflicts with in-loop removals
-        for (i in threads.indices.reversed()) {
-            for (j in threads[i].indices.reversed()) {
-                tryMinimize(i, j)
-                    ?.run(testCfg, testCfg.createVerifier())
-                    ?.let { return it }
-            }
-        }
-        return null
-    }
-
-    private fun ExecutionScenario.run(testCfg: CTestConfiguration, verifier: Verifier): LincheckFailure? =
-        testCfg.createStrategy(
+    private fun LincheckFailure.tryReproduceInModelCheckingMode(
+        iteration: Int,
+        testCfg: CTestConfiguration,
+        verifier: Verifier
+    ): LincheckFailure? {
+        val modelCheckingConfiguration = ModelCheckingCTestConfiguration(
+            testClass = testCfg.testClass,
+            iterations = testCfg.iterations,
+            invocationsPerIteration = testCfg.invocationsPerIteration,
+            threads = testCfg.threads,
+            actorsPerThread = testCfg.actorsPerThread,
+            actorsBefore = testCfg.actorsBefore,
+            actorsAfter = testCfg.actorsAfter,
+            generatorClass = testCfg.generatorClass,
+            verifierClass = testCfg.verifierClass,
+            sequentialSpecification = testCfg.sequentialSpecification,
+            minimizeFailedScenario = false,
+            timeoutMs = testCfg.timeoutMs,
+            customScenarios = testCfg.customScenarios,
+            checkObstructionFreedom = ManagedCTestConfiguration.DEFAULT_CHECK_OBSTRUCTION_FREEDOM,
+            hangingDetectionThreshold = ManagedCTestConfiguration.DEFAULT_HANGING_DETECTION_THRESHOLD,
+            eliminateLocalObjects = ManagedCTestConfiguration.DEFAULT_ELIMINATE_LOCAL_OBJECTS,
+            guarantees = ManagedCTestConfiguration.DEFAULT_GUARANTEES,
+        )
+        val strategy = modelCheckingConfiguration.createStrategy(
             testClass = testClass,
-            scenario = this,
+            scenario = scenario,
             validationFunction = testStructure.validationFunction,
             stateRepresentationMethod = testStructure.stateRepresentation,
-            verifier = verifier
-        ).run()
+        )
+        val invocationsPerIteration = testCfg.invocationsPerIteration
+            .coerceAtMost(MODEL_CHECKING_FAILURE_REPRODUCTION_INVOCATIONS_COUNT)
+        return strategy.use {
+            it.runIteration(iteration, invocationsPerIteration, verifier)
+        }
+    }
 
     private fun CTestConfiguration.createVerifier() =
         verifierClass.getConstructor(Class::class.java).newInstance(sequentialSpecification)
@@ -135,6 +169,12 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
             RandomProvider::class.java
         ).newInstance(this, testStructure, randomProvider)
 
+    private val CTestConfiguration.invocationsPerIteration get() = when (this) {
+        is ModelCheckingCTestConfiguration -> this.invocationsPerIteration
+        is StressCTestConfiguration -> this.invocationsPerIteration
+        else -> error("unexpected")
+    }
+
     // This companion object is used for backwards compatibility.
     companion object {
         /**
@@ -153,6 +193,33 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
     }
 }
 
+// Tries to minimize the specified failing scenario to make the error easier to understand.
+// The algorithm is greedy: it tries to remove one actor from the scenario and checks
+// whether a test with the modified one fails with error as well. If it fails,
+// then the scenario has been successfully minimized, and the algorithm tries to minimize it again, recursively.
+// Otherwise, if no actor can be removed so that the generated test fails, the minimization is completed.
+// Thus, the algorithm works in the linear time of the total number of actors.
+private fun LincheckFailure.minimize(checkScenario: (ExecutionScenario) -> LincheckFailure?): LincheckFailure {
+    var minimizedFailure = this
+    while (true) {
+        minimizedFailure = minimizedFailure.scenario.tryMinimize(checkScenario)
+            ?: break
+    }
+    return minimizedFailure
+}
+
+private fun ExecutionScenario.tryMinimize(checkScenario: (ExecutionScenario) -> LincheckFailure?): LincheckFailure? {
+    // Reversed indices to avoid conflicts with in-loop removals
+    for (i in threads.indices.reversed()) {
+        for (j in threads[i].indices.reversed()) {
+            tryMinimize(i, j)
+                ?.run(checkScenario)
+                ?.let { return it }
+        }
+    }
+    return null
+}
+
 
 /**
  * This is a short-cut for the following code:
@@ -172,4 +239,6 @@ fun <O : Options<O, *>> O.check(testClass: Class<*>) = LinChecker.check(testClas
  */
 fun <O : Options<O, *>> O.check(testClass: KClass<*>) = this.check(testClass.java)
 
-internal fun <O : Options<O, *>> O.checkImpl(testClass: Class<*>) = LinChecker(testClass, this).checkImpl()
+internal fun <O : Options<O, *>> O.checkImpl(testClass: Class<*>) = LinChecker(testClass, this).checkImpl()
+
+private const val MODEL_CHECKING_FAILURE_REPRODUCTION_INVOCATIONS_COUNT = 5_000

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

@@ -26,6 +26,7 @@ abstract class Options<OPT : Options<OPT, CTEST>, CTEST : CTestConfiguration> {
     protected var executionGenerator = CTestConfiguration.DEFAULT_EXECUTION_GENERATOR
     protected var verifier = CTestConfiguration.DEFAULT_VERIFIER
     protected var minimizeFailedScenario = CTestConfiguration.DEFAULT_MINIMIZE_ERROR
+    protected var reproduceWithModelChecking = CTestConfiguration.DEFAULT_REPRODUCE_WITH_MODEL_CHECKING
     protected var sequentialSpecification: Class<*>? = null
     protected var timeoutMs: Long = CTestConfiguration.DEFAULT_TIMEOUT_MS
     protected var customScenarios: MutableList<ExecutionScenario> = mutableListOf()
@@ -119,6 +120,10 @@ abstract class Options<OPT : Options<OPT, CTEST>, CTEST : CTestConfiguration> {
         this.minimizeFailedScenario = minimizeFailedScenario
     }
 
+    fun reproduceWithModelChecking(reproduceWithModelChecking : Boolean): OPT = applyAndCast {
+        this.reproduceWithModelChecking = reproduceWithModelChecking
+    }
+
     abstract fun createTestConfigurations(testClass: Class<*>): CTEST
 
     /**

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

@@ -23,7 +23,7 @@ class Reporter(private val logLevel: LoggingLevel) {
     private val outErr: PrintStream = System.err
 
     fun logIteration(iteration: Int, maxIterations: Int, scenario: ExecutionScenario) = log(INFO) {
-        appendLine("\n= Iteration $iteration / $maxIterations =")
+        appendLine("\n= Iteration ${iteration + 1} / $maxIterations =")
         appendExecutionScenario(scenario)
     }
 
@@ -36,6 +36,10 @@ class Reporter(private val logLevel: LoggingLevel) {
         appendExecutionScenario(scenario)
     }
 
+    fun logFailureReproduction(failure: LincheckFailure) = log(INFO) {
+        appendLine("\nFailure detected, trying to reproduce it and collect the trace:")
+        appendFailure(failure)
+    }
 
     private inline fun log(logLevel: LoggingLevel, crossinline msg: StringBuilder.() -> Unit): Unit = synchronized(this) {
         if (this.logLevel > logLevel) return