NVM testing

build.gradle.kts

@@ -65,6 +65,7 @@ kotlin {
             dependencies {
                 implementation("junit:junit:$junitVersion")
                 implementation("org.jctools:jctools-core:$jctoolsVersion")
+                implementation("org.apache.commons:commons-math3:3.5")
             }
         }
     }
@@ -89,6 +90,7 @@ tasks {
     }
     withType<Test> {
         maxParallelForks = 1
+        maxHeapSize = "4g"
         jvmArgs("--add-opens", "java.base/jdk.internal.misc=ALL-UNNAMED",
                 "--add-exports", "java.base/jdk.internal.util=ALL-UNNAMED")
     }

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

@@ -42,7 +42,9 @@ data class Actor @JvmOverloads constructor(
     val promptCancellation: Boolean = false,
     // we have to specify `isSuspendable` property explicitly for transformed classes since
     // `isSuspendable` implementation produces a circular dependency and, therefore, fails.
-    val isSuspendable: Boolean = method.isSuspendable()
+    val isSuspendable: Boolean = method.isSuspendable(),
+    // save the indices of ThreadId params to replace them later in copyWithThreadId
+    val threadIdArgsIndices: List<Int> = emptyList()
 ) {
     init {
         if (promptCancellation) require(cancelOnSuspension) {
@@ -57,6 +59,11 @@ data class Actor @JvmOverloads constructor(
         (if (cancelOnSuspension) "cancel" else "")
 
     val handlesExceptions = handledExceptions.isNotEmpty()
+
+    /** Returns the copy of this actor with all ThreadId params are set to [threadId]. */
+    fun copyWithThreadId(threadId: Int): Actor = copy(arguments = List(arguments.size) { i ->
+        if (i in threadIdArgsIndices) threadId else arguments[i]
+    })
 }
 
 fun Method.isSuspendable(): Boolean = kotlinFunction?.isSuspend ?: false

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

@@ -23,6 +23,9 @@ package org.jetbrains.kotlinx.lincheck
 
 import org.jetbrains.kotlinx.lincheck.CTestConfiguration.Companion.DEFAULT_TIMEOUT_MS
 import org.jetbrains.kotlinx.lincheck.execution.*
+import org.jetbrains.kotlinx.lincheck.nvm.NoRecoverModel
+import org.jetbrains.kotlinx.lincheck.nvm.RecoverabilityModel
+import org.jetbrains.kotlinx.lincheck.nvm.StrategyRecoveryOptions
 import org.jetbrains.kotlinx.lincheck.strategy.*
 import org.jetbrains.kotlinx.lincheck.strategy.managed.*
 import org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedCTestConfiguration.Companion.DEFAULT_ELIMINATE_LOCAL_OBJECTS
@@ -44,13 +47,16 @@ abstract class CTestConfiguration(
     val actorsBefore: Int,
     val actorsAfter: Int,
     val generatorClass: Class<out ExecutionGenerator>,
-    val verifierClass: Class<out Verifier>,
+    _verifierClass: Class<out Verifier>,
     val requireStateEquivalenceImplCheck: Boolean,
     val minimizeFailedScenario: Boolean,
     val sequentialSpecification: Class<*>,
     val timeoutMs: Long,
-    val customScenarios: List<ExecutionScenario>
+    val customScenarios: List<ExecutionScenario>,
+    val recoverabilityModel: RecoverabilityModel
 ) {
+    val verifierClass = if (recoverabilityModel is NoRecoverModel) _verifierClass else recoverabilityModel.verifierClass
+
     abstract fun createStrategy(testClass: Class<*>, scenario: ExecutionScenario, validationFunctions: List<Method>,
                                 stateRepresentationMethod: Method?, verifier: Verifier): Strategy
     companion object {
@@ -74,7 +80,7 @@ internal fun createFromTestClassAnnotations(testClass: Class<*>): List<CTestConf
                 ann.generator.java, ann.verifier.java, ann.invocationsPerIteration,
                 ann.requireStateEquivalenceImplCheck, ann.minimizeFailedScenario,
                 chooseSequentialSpecification(ann.sequentialSpecification.java, testClass),
-                DEFAULT_TIMEOUT_MS, emptyList()
+                DEFAULT_TIMEOUT_MS, emptyList(), ann.recover.createModel(StrategyRecoveryOptions.STRESS)
             )
         }
     val modelCheckingConfigurations: List<CTestConfiguration> = testClass.getAnnotationsByType(ModelCheckingCTest::class.java)
@@ -84,7 +90,8 @@ internal fun createFromTestClassAnnotations(testClass: Class<*>): List<CTestConf
                 ann.generator.java, ann.verifier.java, ann.checkObstructionFreedom, ann.hangingDetectionThreshold,
                 ann.invocationsPerIteration, ManagedCTestConfiguration.DEFAULT_GUARANTEES, ann.requireStateEquivalenceImplCheck,
                 ann.minimizeFailedScenario, chooseSequentialSpecification(ann.sequentialSpecification.java, testClass),
-                DEFAULT_TIMEOUT_MS, DEFAULT_ELIMINATE_LOCAL_OBJECTS, DEFAULT_VERBOSE_TRACE, emptyList()
+                DEFAULT_TIMEOUT_MS, DEFAULT_ELIMINATE_LOCAL_OBJECTS, DEFAULT_VERBOSE_TRACE, emptyList(),
+                ann.recover.createModel(StrategyRecoveryOptions.MANAGED)
             )
         }
     return stressConfigurations + modelCheckingConfigurations

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

@@ -24,6 +24,7 @@ package org.jetbrains.kotlinx.lincheck
 import org.jetbrains.kotlinx.lincheck.annotations.*
 import org.jetbrains.kotlinx.lincheck.execution.*
 import org.jetbrains.kotlinx.lincheck.strategy.*
+import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTestConfiguration
 import org.jetbrains.kotlinx.lincheck.verifier.*
 import kotlin.reflect.*
 
@@ -66,13 +67,15 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
         val exGen = createExecutionGenerator()
         val verifier = createVerifier(checkStateEquivalence = true)
         for (i in customScenarios.indices) {
+            iterationId.set(-(i + 1))
             val scenario = customScenarios[i]
             scenario.validate()
             reporter.logIteration(i + 1, customScenarios.size, scenario)
             val failure = scenario.run(this, verifier)
             if (failure != null) return failure
         }
         repeat(iterations) { i ->
+            iterationId.set(i)
             val scenario = exGen.nextExecution()
             scenario.validate()
             reporter.logIteration(i + 1 + customScenarios.size, iterations, scenario)
@@ -97,12 +100,12 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
         reporter.logScenarioMinimization(scenario)
         var minimizedFailure = this
         while (true) {
-            minimizedFailure = minimizedFailure.scenario.tryMinimize(testCfg) ?: break
+            minimizedFailure = minimizedFailure.scenario.tryMinimize(testCfg, minimizedFailure) ?: break
         }
         return minimizedFailure
     }
 
-    private fun ExecutionScenario.tryMinimize(testCfg: CTestConfiguration): LincheckFailure? {
+    private fun ExecutionScenario.tryMinimize(testCfg: CTestConfiguration, currentFailure: LincheckFailure): LincheckFailure? {
         // Reversed indices to avoid conflicts with in-loop removals
         for (i in parallelExecution.indices.reversed()) {
             for (j in parallelExecution[i].indices.reversed()) {
@@ -118,23 +121,55 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
             val failure = tryMinimize(threads + 1, j, testCfg)
             if (failure != null) return failure
         }
+        if (testCfg is StressCTestConfiguration
+            && testCfg.recoverabilityModel.crashes
+            && currentFailure is IncorrectResultsFailure)
+            return minimizeCrashes(testCfg, currentFailure)
         return null
     }
 
     private fun ExecutionScenario.tryMinimize(threadId: Int, position: Int, testCfg: CTestConfiguration): LincheckFailure? {
-        val newScenario = this.copy()
-        val actors = newScenario[threadId] as MutableList<Actor>
-        actors.removeAt(position)
-        if (actors.isEmpty() && threadId != 0 && threadId != newScenario.threads + 1) {
-            // Also remove the empty thread
-            newScenario.parallelExecution.removeAt(threadId - 1)
-        }
+        val newScenario = this.copyWithRemovedActor(threadId, position)
         return if (newScenario.isValid) {
-            val verifier = testCfg.createVerifier(checkStateEquivalence = false)
-            newScenario.run(testCfg, verifier)
+            newScenario.runTryMinimize(testCfg)
         } else null
     }
 
+    private fun ExecutionScenario.runTryMinimize(testCfg: CTestConfiguration): LincheckFailure? {
+        val verifier = testCfg.createVerifier(checkStateEquivalence = false)
+        return run(testCfg, verifier)
+    }
+
+    private fun IncorrectResultsFailure.crashesNumber() = results.crashes.sumBy { it.size }
+
+    /**
+     * Run the scenario at most [testCfg.iterations] times with maximum crashes allowed decreased to minimize the number of crashes.
+     */
+    private fun ExecutionScenario.minimizeCrashes(testCfg: CTestConfiguration, failure: IncorrectResultsFailure): LincheckFailure? {
+        var scenario = this
+        var crashes = failure.crashesNumber()
+        var result: LincheckFailure? = null
+        var iterations = testCfg.iterations
+        useProxyCrash.set(false)
+        while (iterations > 0) {
+            crashesMinimization.set(crashes - 1)
+            val newFailure = scenario.runTryMinimize(testCfg)
+            if (newFailure != null
+                && newFailure is IncorrectResultsFailure
+                && newFailure.crashesNumber() < crashes
+            ) {
+                result = newFailure
+                scenario = newFailure.scenario
+                crashes = newFailure.crashesNumber()
+                continue
+            }
+            iterations--
+        }
+        crashesMinimization.remove()
+        useProxyCrash.remove()
+        return result
+    }
+
     private fun ExecutionScenario.run(testCfg: CTestConfiguration, verifier: Verifier): LincheckFailure? =
         testCfg.createStrategy(
             testClass = testClass,
@@ -144,12 +179,6 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
             verifier = verifier
         ).run()
 
-    private fun ExecutionScenario.copy() = ExecutionScenario(
-        ArrayList(initExecution),
-        parallelExecution.map { ArrayList(it) },
-        ArrayList(postExecution)
-    )
-
     private val ExecutionScenario.isValid: Boolean
         get() = !isParallelPartEmpty &&
                 (!hasSuspendableActors() || (!hasSuspendableActorsInInitPart && !hasPostPartAndSuspendableActors))
@@ -209,6 +238,15 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
         fun check(testClass: Class<*>, options: Options<*, *>? = null) {
             LinChecker(testClass, options).check()
         }
+
+        /** A test-local setting of the maximum number of crashes allowed. */
+        internal val crashesMinimization = ThreadLocal.withInitial<Int?> { null }
+
+        /** A test-local setting whether to use crash proxy. Proxy is not used during the minimization only. */
+        internal val useProxyCrash = ThreadLocal.withInitial { true }
+
+        /** A test-local storage for the current iteration number. */
+        internal val iterationId = ThreadLocal.withInitial { 0 }
     }
 }
 
@@ -231,4 +269,4 @@ 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()

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

@@ -23,6 +23,7 @@ package org.jetbrains.kotlinx.lincheck
 
 import org.jetbrains.kotlinx.lincheck.annotations.Operation
 import org.jetbrains.kotlinx.lincheck.execution.*
+import org.jetbrains.kotlinx.lincheck.nvm.Recover
 import org.jetbrains.kotlinx.lincheck.verifier.*
 
 /**
@@ -42,6 +43,7 @@ abstract class Options<OPT : Options<OPT, CTEST>, CTEST : CTestConfiguration> {
     protected var sequentialSpecification: Class<*>? = null
     protected var timeoutMs: Long = CTestConfiguration.DEFAULT_TIMEOUT_MS
     protected var customScenarios: MutableList<ExecutionScenario> = mutableListOf()
+    protected var recover: Recover = Recover.NO_RECOVER
 
     /**
      * Number of different test scenarios to be executed
@@ -158,6 +160,17 @@ abstract class Options<OPT : Options<OPT, CTEST>, CTEST : CTestConfiguration> {
         customScenarios.add(scenario)
     }
 
+    /**
+     * Set the recovery model. [Recover.NO_RECOVER] is used by default.
+     * With any other recovery option enables non-volatile memory testing
+     * in the specified model.
+     *
+     * @see Recover
+     */
+    fun recover(recoverModel: Recover): OPT = applyAndCast {
+        recover = recoverModel
+    }
+
     /**
      * Examine the specified custom scenario additionally to the generated ones.
      */

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

@@ -24,6 +24,7 @@ package org.jetbrains.kotlinx.lincheck
 
 import org.jetbrains.kotlinx.lincheck.LoggingLevel.*
 import org.jetbrains.kotlinx.lincheck.execution.*
+import org.jetbrains.kotlinx.lincheck.nvm.CrashError
 import org.jetbrains.kotlinx.lincheck.runner.*
 import org.jetbrains.kotlinx.lincheck.strategy.*
 import org.jetbrains.kotlinx.lincheck.strategy.managed.*
@@ -186,17 +187,21 @@ private fun StringBuilder.appendDeadlockWithDumpFailure(failure: DeadlockWithDum
     for ((t, stackTrace) in failure.threadDump) {
         val threadNumber = if (t is FixedActiveThreadsExecutor.TestThread) t.iThread.toString() else "?"
         appendLine("Thread-$threadNumber:")
-        stackTrace.map {
-            StackTraceElement(it.className.removePrefix(TransformationClassLoader.REMAPPED_PACKAGE_CANONICAL_NAME), it.methodName, it.fileName, it.lineNumber)
-        }.map { it.toString() }.filter { line ->
-            "org.jetbrains.kotlinx.lincheck.strategy" !in line
-                && "org.jetbrains.kotlinx.lincheck.runner" !in line
-                && "org.jetbrains.kotlinx.lincheck.UtilsKt" !in line
-        }.forEach { appendLine("\t$it") }
+        appendStackTrace(stackTrace)
     }
     return this
 }
 
+private fun StringBuilder.appendStackTrace(stackTrace: Array<StackTraceElement>) {
+    stackTrace.map {
+        StackTraceElement(it.className.removePrefix(TransformationClassLoader.REMAPPED_PACKAGE_CANONICAL_NAME), it.methodName, it.fileName, it.lineNumber)
+    }.map { it.toString() }.filter { line ->
+        "org.jetbrains.kotlinx.lincheck.strategy" !in line
+                && "org.jetbrains.kotlinx.lincheck.runner" !in line
+                && "org.jetbrains.kotlinx.lincheck.UtilsKt" !in line
+    }.forEach { appendLine("\t$it") }
+}
+
 private fun StringBuilder.appendIncorrectResultsFailure(failure: IncorrectResultsFailure): StringBuilder {
     appendln("= Invalid execution results =")
     if (failure.scenario.initExecution.isNotEmpty()) {
@@ -224,6 +229,16 @@ private fun StringBuilder.appendIncorrectResultsFailure(failure: IncorrectResult
     if (failure.results.parallelResultsWithClock.flatten().any { !it.clockOnStart.empty })
         appendln("\n---\nvalues in \"[..]\" brackets indicate the number of completed operations \n" +
             "in each of the parallel threads seen at the beginning of the current operation\n---")
+    failure.results.crashes.forEachIndexed { threadId, threadCrashes ->
+        if (threadCrashes.isNotEmpty()) {
+            appendLine("\nCrashes in thread $threadId:")
+            threadCrashes.forEach { crash ->
+                val actor = if (crash.actorIndex == -1) "constructor" else "actor ${1 + crash.actorIndex}"
+                appendLine("Crashed inside $actor:")
+                appendCrash(crash)
+            }
+        }
+    }
     return this
 }
 
@@ -251,4 +266,8 @@ internal fun StringBuilder.appendStateEquivalenceViolationMessage(sequentialSpec
         "At the current moment, `${sequentialSpecification.simpleName}` does not specify it, or the equivalence relation implementation is incorrect.\n" +
         "To fix this, please implement `equals()` and `hashCode()` functions on `${sequentialSpecification.simpleName}`; the simplest way is to extend `VerifierState`\n" +
         "and override the `extractState()` function, which is called at once and the result of which is used for further `equals()` and `hashCode()` invocations.")
-}
+}
+
+private fun StringBuilder.appendCrash(crash: CrashError) {
+    appendStackTrace(crash.crashStackTrace)
+}

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

@@ -1,5 +1,6 @@
 package org.jetbrains.kotlinx.lincheck
 
+import org.jetbrains.kotlinx.lincheck.nvm.NVMStateHolder
 import java.io.Serializable
 import kotlin.coroutines.*
 
@@ -111,6 +112,7 @@ data class ExceptionResult private constructor(val tClazz: Class<out Throwable>,
         fun create(tClazz: Class<out Throwable>, wasSuspended: Boolean = false) = ExceptionResult(tClazz.normalize(), wasSuspended)
     }
 }
+
 // for byte-code generation
 @JvmSynthetic
 fun createExceptionResult(tClazz: Class<out Throwable>) = ExceptionResult.create(tClazz, false)
@@ -138,4 +140,22 @@ internal data class ResumedResult(val contWithSuspensionPointRes: Pair<Continuat
 
     lateinit var resumedActor: Actor
     lateinit var by: Actor
-}
+}
+
+
+class CrashResult : Result() {
+    lateinit var crashedActors: IntArray
+    override val wasSuspended get() = false
+    override fun toString() = "CRASH${crashedActors.joinToString(",", "(", ")") { s -> if (s == -1) "-" else s.toString() }}"
+
+    override fun hashCode() = crashedActors.contentHashCode()
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other !is CrashResult) return false
+        return crashedActors.contentEquals(other.crashedActors)
+    }
+}
+
+// for byte-code generation
+@JvmSynthetic
+fun createCrashResult() = CrashResult()