refactor the strategy API to expose the single invocation run method

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

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

@@ -39,7 +39,7 @@ abstract class CTestConfiguration(
 ) {
     abstract fun createStrategy(
         testClass: Class<*>, scenario: ExecutionScenario, validationFunction: Actor?,
-        stateRepresentationMethod: Method?, verifier: Verifier
+        stateRepresentationMethod: Method?
     ): Strategy
 
     companion object {

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

@@ -13,12 +13,14 @@ 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.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 +52,65 @@ 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)
             // 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)
                 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
-            }
-            // Reset the parameter generator ranges to start with the same initial bounds on each scenario generation.
-            testStructure.parameterGenerators.forEach { it.reset() }
-        }
-        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
-        }
-        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 }
+            reporter.logIteration(i + 1, scenariosSize, scenario)
+            var failure = scenario.run(i, this, verifier)
+            if (failure == null)
+                return@forEachIndexed
+            if (minimizeFailedScenario && !isCustomScenario) {
+                var j = i + 1
+                reporter.logScenarioMinimization(scenario)
+                failure = failure.minimize { minimizedScenario ->
+                    minimizedScenario.run(j++, this, createVerifier())
+                }
             }
+            reporter.logFailedIteration(failure)
+            return failure
         }
         return null
     }
 
-    private fun ExecutionScenario.run(testCfg: CTestConfiguration, verifier: Verifier): LincheckFailure? =
-        testCfg.createStrategy(
+    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,
-            verifier = verifier
-        ).run()
+        )
+        return strategy.use {
+            it.runIteration(iteration, testCfg.invocationsPerIteration, verifier)
+        }
+    }
 
     private fun CTestConfiguration.createVerifier() =
         verifierClass.getConstructor(Class::class.java).newInstance(sequentialSpecification)
@@ -135,6 +122,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 +146,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:

src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt

@@ -9,9 +9,12 @@
  */
 package org.jetbrains.kotlinx.lincheck.strategy
 
+import org.jetbrains.kotlinx.lincheck.runner.*
 import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario
-import org.jetbrains.kotlinx.lincheck.runner.ExecutionPart
+import org.jetbrains.kotlinx.lincheck.strategy.managed.Trace
+import org.jetbrains.kotlinx.lincheck.verifier.Verifier
 import org.objectweb.asm.ClassVisitor
+import java.io.Closeable
 
 /**
  * Implementation of this class describes how to run the generated execution.
@@ -22,18 +25,130 @@ import org.objectweb.asm.ClassVisitor
  */
 abstract class Strategy protected constructor(
     val scenario: ExecutionScenario
-) {
+) : Closeable {
+    /**
+     * Determines if the strategy requires bytecode transformation.
+     *
+     * @return `true` if a transformation is needed, `false` otherwise.
+     */
     open fun needsTransformation() = false
+
+    /**
+     * Creates a bytecode transformer required by the strategy..
+     *
+     * @param cv the [ClassVisitor] to create a transformer for.
+     * @return a [ClassVisitor] representing the transformer.
+     */
     open fun createTransformer(cv: ClassVisitor): ClassVisitor {
         throw UnsupportedOperationException("$javaClass strategy does not transform classes")
     }
 
-    abstract fun run(): LincheckFailure?
+    /**
+     * Sets the internal state of strategy to run the next invocation.
+     *
+     * @return true if there is next invocation to run, false if all invocations have been studied.
+     */
+    open fun nextInvocation(): Boolean = true
 
+    /**
+     * Initializes the invocation.
+     * Should be called before each call to [runInvocation].
+     */
+    open fun initializeInvocation() {}
+
+    /**
+     * Runs the current invocation and returns its result.
+     *
+     * Should be called after [initializeInvocation] and only if previous call to [nextInvocation] returned `true`:
+     *
+     * ```kotlin
+     *  with(strategy) {
+     *      if (nextInvocation()) {
+     *          initializeInvocation()
+     *          runInvocation()
+     *      }
+     *  }
+     * ```
+     *
+     * For deterministic strategies, consecutive calls to [runInvocation]
+     * (without intervening [nextInvocation] calls)
+     * should run the same invocation, leading to the same results.
+     *
+     * @return the result of the invocation run.
+     */
+    abstract fun runInvocation(): InvocationResult
+
+    /**
+     * Tries to construct the trace leading to the given invocation result.
+     *
+     * @param result The invocation result.
+     * @return The collected trace, or null if it was not possible to collect the trace.
+     */
+    open fun tryCollectTrace(result: InvocationResult): Trace? = null
+
+    /**
+     * This method is called before the execution of a specific scenario part.
+     *
+     * @param part The execution part that is about to be executed.
+     */
     open fun beforePart(part: ExecutionPart) {}
 
     /**
-     * Is invoked before each actor execution.
+     * This method is called before each actor execution.
+     *
+     * @param iThread the thread index on which the actor is starting
      */
     open fun onActorStart(iThread: Int) {}
+
+    /**
+     * Closes the strategy and releases any resources associated with it.
+     */
+    override fun close() {}
+}
+
+/**
+ * Runs one Lincheck's test iteration with the given strategy and verifier.
+ *
+ * @param iteration the id of the iteration.
+ * @param invocationsBound number of invocations to run.
+ * @param verifier the verifier to be used.
+ *
+ * @return the failure, if detected, null otherwise.
+ */
+fun Strategy.runIteration(iteration: Int, invocationsBound: Int, verifier: Verifier): LincheckFailure? {
+    var spinning = false
+    for (invocation in 0 until invocationsBound) {
+        if (!(spinning || nextInvocation()))
+            return null
+        spinning = false
+        initializeInvocation()
+        val failure = run {
+            val result = runInvocation()
+            spinning = (result is SpinCycleFoundAndReplayRequired)
+            if (!spinning)
+                verify(result, verifier)
+            else null
+        }
+        if (failure != null)
+            return failure
+    }
+    return null
 }
+
+/**
+ * Verifies the results of the given invocation.
+ * Attempts to collect the trace in case of incorrect results.
+ *
+ * @param result invocation result to verify.
+ * @param verifier the verifier to be used.
+ *
+ * @return failure, if invocation results are incorrect, null otherwise.
+ */
+fun Strategy.verify(result: InvocationResult, verifier: Verifier): LincheckFailure? = when (result) {
+    is CompletedInvocationResult ->
+        if (!verifier.verifyResults(scenario, result.results)) {
+            IncorrectResultsFailure(scenario, result.results, tryCollectTrace(result))
+        } else null
+    else ->
+        result.toLincheckFailure(scenario, tryCollectTrace(result))
+}