Implement durable model run

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

@@ -1,5 +1,6 @@
 package org.jetbrains.kotlinx.lincheck
 
+import org.jetbrains.kotlinx.lincheck.nvm.CrashError
 import java.io.Serializable
 import kotlin.coroutines.*
 
@@ -138,4 +139,12 @@ internal data class ResumedResult(val contWithSuspensionPointRes: Pair<Continuat
 
     lateinit var resumedActor: Actor
     lateinit var by: Actor
-}
+}
+
+data class CrashResult(val e: CrashError) : Result() {
+    override val wasSuspended get() = false
+}
+
+// for byte-code generation
+@JvmSynthetic
+fun creteCrashResult(e: CrashError) = CrashResult(e)

src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/RecoverabilityModel.kt

@@ -20,21 +20,19 @@
 
 package org.jetbrains.kotlinx.lincheck.nvm
 
-import org.jetbrains.kotlinx.lincheck.runner.ParallelThreadsRunner
-import org.jetbrains.kotlinx.lincheck.runner.RecoverableParallelThreadsRunner
-import org.jetbrains.kotlinx.lincheck.runner.Runner
-import org.jetbrains.kotlinx.lincheck.runner.UseClocks
+import org.jetbrains.kotlinx.lincheck.runner.*
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTestConfiguration
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressStrategy
 import org.objectweb.asm.ClassVisitor
 import java.lang.reflect.Method
 
 enum class Recover {
-    NO_RECOVER, NRL;
+    NO_RECOVER, NRL, DURABLE;
 
     fun createModel() = when (this) {
         NO_RECOVER -> NoRecoverModel()
         NRL -> NRLModel()
+        DURABLE -> DurableModel()
     }
 }
 
@@ -49,6 +47,8 @@ interface RecoverabilityModel {
         stateRepresentationFunction: Method?,
         testCfg: StressCTestConfiguration
     ): Runner
+
+    fun createActorCrashHandlerGenerator(): ActorCrashHandlerGenerator
 }
 
 class NoRecoverModel : RecoverabilityModel {
@@ -62,8 +62,10 @@ class NoRecoverModel : RecoverabilityModel {
         testCfg: StressCTestConfiguration
     ): Runner = ParallelThreadsRunner(
         strategy, testClass, validationFunctions, stateRepresentationFunction,
-        testCfg.timeoutMs, UseClocks.RANDOM
+        testCfg.timeoutMs, UseClocks.RANDOM, this
     )
+
+    override fun createActorCrashHandlerGenerator() = ActorCrashHandlerGenerator()
 }
 
 class NRLModel(override val crashes: Boolean = true) : RecoverabilityModel {
@@ -85,4 +87,27 @@ class NRLModel(override val crashes: Boolean = true) : RecoverabilityModel {
         strategy, testClass, validationFunctions, stateRepresentationFunction,
         testCfg.timeoutMs, UseClocks.RANDOM, this
     )
+
+    override fun createActorCrashHandlerGenerator() = ActorCrashHandlerGenerator()
+}
+
+class DurableModel(override val crashes: Boolean = true) : RecoverabilityModel {
+    override fun createTransformer(cv: ClassVisitor, clazz: Class<*>) = if (crashes) {
+        CrashTransformer(cv, clazz)
+    } else {
+        cv
+    }
+
+    override fun createRunner(
+        strategy: StressStrategy,
+        testClass: Class<*>,
+        validationFunctions: List<Method>,
+        stateRepresentationFunction: Method?,
+        testCfg: StressCTestConfiguration
+    ): Runner = RecoverableParallelThreadsRunner(
+        strategy, testClass, validationFunctions, stateRepresentationFunction,
+        testCfg.timeoutMs, UseClocks.RANDOM, this
+    )
+
+    override fun createActorCrashHandlerGenerator() = DurableActorCrashHandlerGenerator()
 }

src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ActorCrashHandlerGenerator.kt

@@ -0,0 +1,73 @@
+/*
+ * Lincheck
+ *
+ * Copyright (C) 2019 - 2021 JetBrains s.r.o.
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU Lesser General Public License as
+ * published by the Free Software Foundation, either version 3 of the
+ * License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Lesser Public License for more details.
+ *
+ * You should have received a copy of the GNU General Lesser Public
+ * License along with this program.  If not, see
+ * <http://www.gnu.org/licenses/lgpl-3.0.html>
+ */
+
+package org.jetbrains.kotlinx.lincheck.runner
+
+import org.jetbrains.kotlinx.lincheck.CrashResult
+import org.jetbrains.kotlinx.lincheck.nvm.CrashError
+import org.objectweb.asm.Label
+import org.objectweb.asm.Type
+import org.objectweb.asm.commons.GeneratorAdapter
+import org.objectweb.asm.commons.Method
+
+private val CRASH_ERROR_TYPE = Type.getType(CrashError::class.java)
+private val CRASH_RESULT_TYPE = Type.getType(CrashResult::class.java)
+private val RESULT_KT_CREATE_CRASH_RESULT_METHOD =
+    Method("creteCrashResult", CRASH_RESULT_TYPE, arrayOf(CRASH_ERROR_TYPE))
+
+
+open class ActorCrashHandlerGenerator {
+    open fun addCrashTryBlock(start: Label, end: Label, mv: GeneratorAdapter) {}
+    open fun addCrashCatchBlock(mv: GeneratorAdapter, resLocal: Int, iLocal: Int, skip: Label) {}
+}
+
+class DurableActorCrashHandlerGenerator : ActorCrashHandlerGenerator() {
+    private lateinit var handlerLabel: Label
+
+    override fun addCrashTryBlock(start: Label, end: Label, mv: GeneratorAdapter) {
+        super.addCrashTryBlock(start, end, mv)
+        handlerLabel = mv.newLabel()
+        mv.visitTryCatchBlock(start, end, handlerLabel, CRASH_ERROR_TYPE.internalName)
+    }
+
+    override fun addCrashCatchBlock(mv: GeneratorAdapter, resLocal: Int, iLocal: Int, skip: Label) {
+        super.addCrashCatchBlock(mv, resLocal, iLocal, skip)
+        mv.visitLabel(handlerLabel)
+        storeExceptionResultFromCrash(mv, resLocal, iLocal, skip)
+    }
+
+    private fun storeExceptionResultFromCrash(mv: GeneratorAdapter, resLocal: Int, iLocal: Int, skip: Label) {
+        mv.checkCast(CRASH_ERROR_TYPE)
+        val eLocal = mv.newLocal(CRASH_ERROR_TYPE)
+        mv.storeLocal(eLocal)
+
+        mv.loadLocal(resLocal)
+        mv.loadLocal(iLocal)
+
+        // Load exception result
+        mv.loadLocal(eLocal)
+        // Create crash result instance
+        mv.invokeStatic(TestThreadExecutionGenerator.RESULT_KT_TYPE, RESULT_KT_CREATE_CRASH_RESULT_METHOD)
+        mv.checkCast(TestThreadExecutionGenerator.RESULT_TYPE)
+        mv.arrayStore(TestThreadExecutionGenerator.RESULT_TYPE)
+
+        mv.goTo(skip)
+    }
+}

src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt

@@ -24,6 +24,8 @@ package org.jetbrains.kotlinx.lincheck.runner
 import org.jetbrains.kotlinx.lincheck.*
 import org.jetbrains.kotlinx.lincheck.execution.*
 import org.jetbrains.kotlinx.lincheck.nvm.CrashError
+import org.jetbrains.kotlinx.lincheck.nvm.NoRecoverModel
+import org.jetbrains.kotlinx.lincheck.nvm.RecoverabilityModel
 import org.jetbrains.kotlinx.lincheck.runner.FixedActiveThreadsExecutor.TestThread
 import org.jetbrains.kotlinx.lincheck.runner.UseClocks.*
 import org.jetbrains.kotlinx.lincheck.strategy.*
@@ -49,7 +51,8 @@ internal open class ParallelThreadsRunner(
     validationFunctions: List<Method>,
     stateRepresentationFunction: Method?,
     private val timeoutMs: Long, // for deadlock or livelock detection
-    private val useClocks: UseClocks // specifies whether `HBClock`-s should always be used or with some probability
+    private val useClocks: UseClocks, // specifies whether `HBClock`-s should always be used or with some probability
+    protected val recoverModel: RecoverabilityModel = NoRecoverModel()
 ) : Runner(strategy, testClass, validationFunctions, stateRepresentationFunction) {
     private val runnerHash = this.hashCode() // helps to distinguish this runner threads from others
     private val executor = FixedActiveThreadsExecutor(scenario.threads, runnerHash) // shoukd be closed in `close()`
@@ -81,7 +84,7 @@ internal open class ParallelThreadsRunner(
     override fun initialize() {
         super.initialize()
         testThreadExecutions = Array(scenario.threads) { t ->
-            TestThreadExecutionGenerator.create(this, t, scenario.parallelExecution[t], completions[t], scenario.hasSuspendableActors())
+            TestThreadExecutionGenerator.create(this, t, scenario.parallelExecution[t], completions[t], scenario.hasSuspendableActors(), recoverModel.createActorCrashHandlerGenerator())
         }
         testThreadExecutions.forEach { it.allThreadExecutions = testThreadExecutions }
     }

src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/RecoverableParallelThreadsRunner.kt

@@ -82,8 +82,8 @@ internal class RecoverableParallelThreadsRunner(
     stateRepresentationFunction: Method?,
     timeoutMs: Long,
     useClocks: UseClocks,
-    private val recoverModel: RecoverabilityModel
-) : ParallelThreadsRunner(strategy, testClass, validationFunctions, stateRepresentationFunction, timeoutMs, useClocks) {
+    recoverModel: RecoverabilityModel
+) : ParallelThreadsRunner(strategy, testClass, validationFunctions, stateRepresentationFunction, timeoutMs, useClocks, recoverModel) {
     override fun needsTransformation() = true
     override fun createTransformer(cv: ClassVisitor) =
         recoverModel.createTransformer(super.createTransformer(cv), _testClass)
@@ -104,7 +104,6 @@ internal class RecoverableParallelThreadsRunner(
             scenario.initExecution.size + scenario.parallelExecution.sumBy { it.size } + scenario.postExecution.size
         Crash.reset()
         RecoverableStateContainer.state = ExecutionState.INIT
-        RecoverableStateContainer.crashesEnabled = true
         Crash.register(0)
     }
 
@@ -113,18 +112,19 @@ internal class RecoverableParallelThreadsRunner(
         super.beforeParallel(threads)
         RecoverableStateContainer.threads = threads
         RecoverableStateContainer.state = ExecutionState.PARALLEL
+        RecoverableStateContainer.crashesEnabled = true
     }
 
     override fun beforePost() {
         super.beforePost()
+        RecoverableStateContainer.crashesEnabled = false
         RecoverableStateContainer.state = ExecutionState.POST
         Crash.register(scenario.threads + 1)
     }
 
     override fun afterPost() {
         super.afterPost()
         Crash.exit(scenario.threads + 1)
-        RecoverableStateContainer.crashesEnabled = false
         RecoverableStateContainer.state = ExecutionState.INIT
     }
 

src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/TestThreadExecutionGenerator.java

@@ -61,7 +61,7 @@ public class TestThreadExecutionGenerator {
     private static final Method TEST_THREAD_EXECUTION_INC_CLOCK = new Method("incClock", VOID_TYPE, NO_ARGS);
     private static final Method TEST_THREAD_EXECUTION_READ_CLOCKS = new Method("readClocks", VOID_TYPE, new Type[]{INT_TYPE});
 
-    private static final Type RESULT_TYPE = getType(Result.class);
+    static final Type RESULT_TYPE = getType(Result.class);
 
     private static final Type NO_RESULT_TYPE = getType(NoResult.class);
     private static final String NO_RESULT_CLASS_NAME = NoResult.class.getCanonicalName().replace('.', '/');
@@ -78,7 +78,7 @@ public class TestThreadExecutionGenerator {
     private static final Method VALUE_RESULT_TYPE_CONSTRUCTOR = new Method("<init>", VOID_TYPE, new Type[] {OBJECT_TYPE});
 
     private static final Type EXCEPTION_RESULT_TYPE = getType(ExceptionResult.class);
-    private static final Type RESULT_KT_TYPE = getType(ResultKt.class);
+    static final Type RESULT_KT_TYPE = getType(ResultKt.class);
     private static final Method RESULT_KT_CREATE_EXCEPTION_RESULT_METHOD = new Method("createExceptionResult", EXCEPTION_RESULT_TYPE, new Type[] {CLASS_TYPE});
 
     private static final Type RESULT_ARRAY_TYPE = getType(Result[].class);
@@ -105,12 +105,23 @@ public class TestThreadExecutionGenerator {
     public static TestThreadExecution create(Runner runner, int iThread, List<Actor> actors,
                                              List<ParallelThreadsRunner.Completion> completions,
                                              boolean scenarioContainsSuspendableActors
+    ) {
+        return create(runner, iThread, actors, completions, scenarioContainsSuspendableActors, new ActorCrashHandlerGenerator());
+    }
+
+    /**
+     * Creates a {@link TestThreadExecution} instance with specified {@link TestThreadExecution#run()} implementation.
+     */
+    public static TestThreadExecution create(Runner runner, int iThread, List<Actor> actors,
+                                             List<ParallelThreadsRunner.Completion> completions,
+                                             boolean scenarioContainsSuspendableActors,
+                                             ActorCrashHandlerGenerator actorCrashHandlerGenerator
     ) {
         String className = TestThreadExecution.class.getCanonicalName() + generatedClassNumber++;
         String internalClassName = className.replace('.', '/');
         List<Object> objArgs = new ArrayList<>();
         Class<? extends TestThreadExecution> clz = runner.getClassLoader().defineClass(className,
-                generateClass(internalClassName, getType(runner.getTestClass()), iThread, actors, objArgs, completions, scenarioContainsSuspendableActors));
+                generateClass(internalClassName, getType(runner.getTestClass()), iThread, actors, objArgs, completions, scenarioContainsSuspendableActors, actorCrashHandlerGenerator));
         try {
             TestThreadExecution execution = clz.newInstance();
             execution.runner = runner;
@@ -123,13 +134,14 @@ public static TestThreadExecution create(Runner runner, int iThread, List<Actor>
 
     private static byte[] generateClass(String internalClassName, Type testClassType, int iThread, List<Actor> actors,
                                         List<Object> objArgs, List<ParallelThreadsRunner.Completion> completions,
-                                        boolean scenarioContainsSuspendableActors)
+                                        boolean scenarioContainsSuspendableActors,
+                                        ActorCrashHandlerGenerator actorCrashHandlerGenerator)
     {
         ClassWriter cw = new ClassWriter(ClassWriter.COMPUTE_FRAMES);
         CheckClassAdapter cca = new CheckClassAdapter(cw, false);
         cca.visit(52, ACC_PUBLIC + ACC_SUPER, internalClassName, null, TEST_THREAD_EXECUTION_TYPE.getInternalName(), null);
         generateConstructor(cca);
-        generateRun(cca, testClassType, iThread, actors, objArgs, completions, scenarioContainsSuspendableActors);
+        generateRun(cca, testClassType, iThread, actors, objArgs, completions, scenarioContainsSuspendableActors, actorCrashHandlerGenerator);
         cca.visitEnd();
         return cw.toByteArray();
     }
@@ -146,7 +158,8 @@ private static void generateConstructor(ClassVisitor cv) {
 
     private static void generateRun(ClassVisitor cv, Type testType, int iThread, List<Actor> actors,
                                     List<Object> objArgs, List<Completion> completions,
-                                    boolean scenarioContainsSuspendableActors)
+                                    boolean scenarioContainsSuspendableActors,
+                                    ActorCrashHandlerGenerator actorCrashHandlerGenerator)
     {
         int access = ACC_PUBLIC;
         Method m = new Method("run", VOID_TYPE, NO_ARGS);
@@ -193,6 +206,9 @@ private static void generateRun(ClassVisitor cv, Type testType, int iThread, Lis
                 for (Class<? extends Throwable> ec : actor.getHandledExceptions())
                     mv.visitTryCatchBlock(actorCatchBlockStart, actorCatchBlockEnd, handledExceptionHandler, getType(ec).getInternalName());
             }
+
+            actorCrashHandlerGenerator.addCrashTryBlock(actorCatchBlockStart, actorCatchBlockEnd, mv);
+
             // Catch those exceptions that has not been caught yet
             Label unexpectedExceptionHandler = mv.newLabel();
             mv.visitTryCatchBlock(actorCatchBlockStart, actorCatchBlockEnd, unexpectedExceptionHandler, THROWABLE_TYPE.getInternalName());
@@ -264,6 +280,8 @@ private static void generateRun(ClassVisitor cv, Type testType, int iThread, Lis
             // End of try-catch block for all other exceptions
             mv.goTo(skipHandlers);
 
+            actorCrashHandlerGenerator.addCrashCatchBlock(mv, resLocal, iLocal, skipHandlers);
+
             // Unexpected exception handler
             mv.visitLabel(unexpectedExceptionHandler);
             // Call onFailure method

src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/DurableMSQueueTest.kt → src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/durable/DurableMSQueueTest.kt

@@ -1,32 +1,33 @@
-/*-
- * #%L
+/*
  * Lincheck
- * %%
- * Copyright (C) 2019 - 2020 JetBrains s.r.o.
- * %%
+ *
+ * Copyright (C) 2019 - 2021 JetBrains s.r.o.
+ *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU Lesser General Public License as
  * published by the Free Software Foundation, either version 3 of the
  * License, or (at your option) any later version.
- * 
+ *
  * This program is distributed in the hope that it will be useful,
  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  * GNU General Lesser Public License for more details.
- * 
+ *
  * You should have received a copy of the GNU General Lesser Public
  * License along with this program.  If not, see
- * <http://www.gnu.org/licenses/lgpl-3.0.html>.
- * #L%
+ * <http://www.gnu.org/licenses/lgpl-3.0.html>
  */
 package org.jetbrains.kotlinx.lincheck.test.verifier.nlr
 
-import org.jetbrains.kotlinx.lincheck.Options
+import org.jetbrains.kotlinx.lincheck.LinChecker
+import org.jetbrains.kotlinx.lincheck.LincheckAssertionError
 import org.jetbrains.kotlinx.lincheck.annotations.Operation
 import org.jetbrains.kotlinx.lincheck.annotations.Param
+import org.jetbrains.kotlinx.lincheck.nvm.Recover
 import org.jetbrains.kotlinx.lincheck.paramgen.ThreadIdGen
-import org.jetbrains.kotlinx.lincheck.test.AbstractLincheckTest
+import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest
 import org.jetbrains.kotlinx.lincheck.test.verifier.linearizability.SequentialQueue
+import org.junit.Test
 import java.util.concurrent.atomic.AtomicInteger
 import java.util.concurrent.atomic.AtomicReference
 
@@ -35,7 +36,12 @@ private const val THREADS_NUMBER = 3
 /**
  * @see  <a href="http://www.cs.technion.ac.il/~erez/Papers/nvm-queue-full.pdf">A Persistent Lock-Free Queue for Non-Volatile Memory</a>
  */
-class DurableMSQueueTest : AbstractLincheckTest() {
+@StressCTest(
+    sequentialSpecification = SequentialQueue::class,
+    threads = THREADS_NUMBER,
+    recover = Recover.DURABLE
+)
+class DurableMSQueueTest {
     private val q = DurableMSQueue<Int>(2 + THREADS_NUMBER)
 
     @Operation
@@ -44,10 +50,9 @@ class DurableMSQueueTest : AbstractLincheckTest() {
     @Operation
     fun pop(@Param(gen = ThreadIdGen::class) threadId: Int) = q.pop(threadId)
 
-    override fun <O : Options<O, *>> O.customize() {
-        sequentialSpecification(SequentialQueue::class.java)
-        threads(THREADS_NUMBER)
-    }
+    // verification is incomplete
+    @Test(expected = LincheckAssertionError::class)
+    fun test() = LinChecker.check(this::class.java)
 }