Migration to the immutable Result type

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

@@ -36,45 +36,60 @@ import kotlin.coroutines.Continuation
  * the execution thread was suspended without any chance to be resumed,
  * meaning that all other execution threads completed their execution or were suspended too.
  */
-public sealed class Result {
-    var wasSuspended: Boolean = false
+sealed class Result {
+    abstract val wasSuspended: Boolean
+    protected val wasSuspendedPrefix: String get() = (if (wasSuspended) "S + " else "")
 }
 
 /**
  * Type of result used if the actor invocation returns any value.
  */
-data class ValueResult(val value: Any?) : Result() {
-    override fun toString() = if (wasSuspended) "($value, wasSuspended)" else "$value"
+data class ValueResult @JvmOverloads constructor(val value: Any?, override val wasSuspended: Boolean = false) : Result() {
+    override fun toString() = wasSuspendedPrefix + "$value"
 }
 
 /**
  * Type of result used if the actor invocation does not return value.
  */
 object VoidResult : Result() {
-    override fun toString() = if (wasSuspended) "(void, wasSuspended)" else "void"
+    override val wasSuspended get() = false
+    override fun toString() = wasSuspendedPrefix + VOID
 }
 
+object SuspendedVoidResult : Result() {
+    override val wasSuspended get() = true
+    override fun toString() = wasSuspendedPrefix + VOID
+}
+
+private const val VOID = "void"
+
 /**
  * Type of result used if the actor invocation fails with the specified in {@link Operation#handleExceptionsAsResult()} exception [tClazz].
  */
-data class ExceptionResult(val tClazz: Class<out Throwable>?) : Result() {
-    override fun toString() = if (wasSuspended) "(${tClazz?.simpleName}, wasSuspended)" else "${tClazz?.simpleName}"
+data class ExceptionResult @JvmOverloads constructor(val tClazz: Class<out Throwable>?, override val wasSuspended: Boolean = false) : Result() {
+    override fun toString() = wasSuspendedPrefix + "${tClazz?.simpleName}"
 }
 
 /**
  * Type of result used if the actor invocation suspended the thread and did not get the final result yet
  * though it can be resumed later
  */
 object NoResult : Result() {
-    override fun toString() = "suspended"
+    override val wasSuspended get() = false
+    override fun toString() = "-"
+}
+
+object Suspended : Result() {
+    override val wasSuspended get() = true
+    override fun toString() = "S"
 }
 
 /**
  * Type of result used for verification.
  * Resuming thread writes result of the suspension point and continuation to be executed in the resumed thread into [contWithSuspensionPointRes].
  */
 internal data class ResumedResult(val contWithSuspensionPointRes: Pair<Continuation<Any?>?, kotlin.Result<Any?>>) : Result() {
-    init { super.wasSuspended = true }
+    override val wasSuspended: Boolean get() = true
 
     lateinit var resumedActor: Actor
     lateinit var by: Actor

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Utils.kt

@@ -133,22 +133,22 @@ private fun getRelaxedMethod(instance: Any, actor: Actor): Method = methodsCache
  * Failure values of [kotlin.Result] instances are represented as [ExceptionResult].
  */
 internal fun createLinCheckResult(res: Any?, wasSuspended: Boolean = false) = when {
-    (res != null && res.javaClass.isAssignableFrom(Void.TYPE)) || res is kotlin.Unit -> VoidResult.also { it.wasSuspended = wasSuspended }
-    res != null && res is Throwable -> ExceptionResult(res.javaClass).also { it.wasSuspended = wasSuspended }
-    res === COROUTINE_SUSPENDED -> NoResult.also { it.wasSuspended = true }
-    res is kotlin.Result<Any?> -> res.toLinCheckResult().also { it.wasSuspended = wasSuspended }
-    else -> ValueResult(res).also { it.wasSuspended = wasSuspended }
+    (res != null && res.javaClass.isAssignableFrom(Void.TYPE)) || res is Unit -> if (wasSuspended) SuspendedVoidResult else VoidResult
+    res != null && res is Throwable -> ExceptionResult(res.javaClass, wasSuspended)
+    res === COROUTINE_SUSPENDED -> Suspended
+    res is kotlin.Result<Any?> -> res.toLinCheckResult(wasSuspended)
+    else -> ValueResult(res, wasSuspended)
 }
 
-private fun kotlin.Result<Any?>.toLinCheckResult() =
+private fun kotlin.Result<Any?>.toLinCheckResult(wasSuspended: Boolean) =
     if (isSuccess) {
         when (val value = getOrNull()) {
-            is Unit -> VoidResult
+            is Unit -> if (wasSuspended) SuspendedVoidResult else VoidResult
             // Throwable was returned as a successful result
-            is Throwable -> ValueResult(value::class.java)
-            else -> ValueResult(value)
+            is Throwable -> ValueResult(value::class.java, wasSuspended)
+            else -> ValueResult(value, wasSuspended)
         }
-    } else ExceptionResult(exceptionOrNull()?.let { it::class.java })
+    } else ExceptionResult(exceptionOrNull()?.let { it::class.java }, wasSuspended)
 
 
 fun <R> Throwable.catch(vararg exceptions: Class<*>, block: () -> R): R {

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

@@ -80,7 +80,7 @@ open class ParallelThreadsRunner(
             // otherwise it was already decremented before writing resWithCont
             resWithCont.get() ?: completedOrSuspendedThreads.decrementAndGet()
             // write method's final result
-            suspensionPointResults[threadId] = createLinCheckResult(result)
+            suspensionPointResults[threadId] = createLinCheckResult(result, wasSuspended = true)
         }
     }
 
@@ -123,20 +123,19 @@ open class ParallelThreadsRunner(
         val finalResult: Result
         val completion = completions[threadId][actorId]
         if (res === COROUTINE_SUSPENDED) {
-            suspensionPointResults[threadId].wasSuspended = true
             completedOrSuspendedThreads.incrementAndGet()
             // Thread was suspended -> if suspended method call has follow-up after this suspension point
             // then wait for result of this suspension point
             // and continuation written by resuming thread to be executed by this thread,
             // or final result written by the resuming thread
-            while (completion.resWithCont.get() === null && suspensionPointResults[threadId] is NoResult) {
+            while (completion.resWithCont.get() === null && suspensionPointResults[threadId] === NoResult) {
                 if (completedOrSuspendedThreads.get() == scenario.threads) {
                     // all threads were suspended or completed
                     suspensionPointResults[threadId] = NoResult
-                    return NoResult
+                    return Suspended
                 }
             }
-            if (suspensionPointResults[threadId] !is NoResult) {
+            if (suspensionPointResults[threadId] !== NoResult) {
                 // Result of the suspension point equals to the final method call result
                 // completion.resumeWith was called in the resuming thread, final result is written
                 finalResult = suspensionPointResults[threadId]
@@ -171,8 +170,9 @@ open class ParallelThreadsRunner(
         var postPartSuspended = false
         val postResults = scenario.postExecution.map { postActor ->
             // no actors are executed after suspension of a post part
-            if (postPartSuspended) NoResult
-            else {
+            if (postPartSuspended) {
+                NoResult
+            } else {
                 // post part may contain suspendable actors if there aren't any in the parallel part, invoke with dummy continuation
                 executeActor(testInstance, postActor, dummyCompletion).also { postPartSuspended = it.wasSuspended }
             }

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

@@ -72,6 +72,9 @@ public class TestThreadExecutionGenerator {
     private static final Type VOID_RESULT_TYPE = Type.getType(VoidResult.class);
     private static final String VOID_RESULT_CLASS_NAME = VoidResult.class.getCanonicalName().replace('.', '/');
 
+    private static final Type SUSPENDED_VOID_RESULT_TYPE = Type.getType(SuspendedVoidResult.class);
+    private static final String SUSPENDED_RESULT_CLASS_NAME = SuspendedVoidResult.class.getCanonicalName().replace('.', '/');
+
     private static final String INSTANCE = "INSTANCE";
 
     private static final Type VALUE_RESULT_TYPE = Type.getType(ValueResult.class);
@@ -82,6 +85,8 @@ public class TestThreadExecutionGenerator {
 
     private static final Type RESULT_ARRAY_TYPE = Type.getType(Result[].class);
 
+    private static final Method RESULT_WAS_SUSPENDED_GETTER_METHOD = new Method("getWasSuspended", Type.BOOLEAN_TYPE, new Type[]{});
+
     private static final Type PARALLEL_THREADS_RUNNER_TYPE = Type.getType(ParallelThreadsRunner.class);
     private static final Method PARALLEL_THREADS_RUNNER_PROCESS_INVOCATION_RESULT_METHOD = new Method("processInvocationResult", RESULT_TYPE, new Type[]{ OBJECT_TYPE, Type.INT_TYPE, Type.INT_TYPE });
     private static final Method RUNNER_IS_PARALLEL_EXECUTION_COMPLETED_METHOD = new Method("isParallelExecutionCompleted", Type.BOOLEAN_TYPE, new Type[]{});
@@ -226,12 +231,12 @@ private static void generateRun(ClassVisitor cv, Type testType, int iThread, Lis
                 mv.push(i);
                 mv.invokeVirtual(PARALLEL_THREADS_RUNNER_TYPE, PARALLEL_THREADS_RUNNER_PROCESS_INVOCATION_RESULT_METHOD);
                 if (actor.getMethod().getReturnType() == void.class) {
-                    createVoidResult(mv);
+                    createVoidResult(actor, mv);
                 }
             } else {
                 // Create result
                 if (actor.getMethod().getReturnType() == void.class) {
-                    createVoidResult(mv);
+                    createVoidResult(actor, mv);
                 } else {
                     mv.invokeConstructor(VALUE_RESULT_TYPE, VALUE_RESULT_TYPE_CONSTRUCTOR);
                 }
@@ -253,7 +258,7 @@ private static void generateRun(ClassVisitor cv, Type testType, int iThread, Lis
             // Increment number of current operation
             mv.iinc(iLocal, 1);
             mv.visitJumpInsn(GOTO, launchNextActor);
-            // write NoResult(wasSuspended = true) if all threads were suspended or completed
+            // write NoResult if all threads were suspended or completed
             mv.visitLabel(returnNoResult);
             mv.loadLocal(resLocal);
             mv.push(i);
@@ -277,9 +282,19 @@ private static void generateRun(ClassVisitor cv, Type testType, int iThread, Lis
         mv.visitEnd();
     }
 
-    private static void createVoidResult(GeneratorAdapter mv) {
-        mv.pop();
-        mv.visitFieldInsn(GETSTATIC, VOID_RESULT_CLASS_NAME, INSTANCE, VOID_RESULT_TYPE.getDescriptor());
+    private static void createVoidResult(Actor actor, GeneratorAdapter mv) {
+        if (actor.isSuspendable()) {
+            Label suspendedVoidResult = mv.newLabel();
+            mv.invokeVirtual(RESULT_TYPE, RESULT_WAS_SUSPENDED_GETTER_METHOD);
+            mv.push(true);
+            mv.ifCmp(Type.BOOLEAN_TYPE, GeneratorAdapter.EQ, suspendedVoidResult);
+            mv.visitFieldInsn(GETSTATIC, VOID_RESULT_CLASS_NAME, INSTANCE, VOID_RESULT_TYPE.getDescriptor());
+            mv.visitLabel(suspendedVoidResult);
+            mv.visitFieldInsn(GETSTATIC, SUSPENDED_RESULT_CLASS_NAME, INSTANCE, SUSPENDED_VOID_RESULT_TYPE.getDescriptor());
+        } else {
+            mv.pop();
+            mv.visitFieldInsn(GETSTATIC, VOID_RESULT_CLASS_NAME, INSTANCE, VOID_RESULT_TYPE.getDescriptor());
+        }
     }
 
     private static void storeExceptionResultFromThrowable(GeneratorAdapter mv, int resLocal, int iLocal) {

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/LTS.kt

@@ -132,17 +132,22 @@ class LTS(
                 resInfo
             }
             return if (isQuantitativelyRelaxed) resultWithTransitionInfo
-            else if (resultWithTransitionInfo!!.result == expectedResult ||
-                // Allow transition by a suspended request
-                // regardless whether the operation was suspended during test running or not,
-                // thus allowing elimination of interblocking operations in the implementation.
-                (isRequest && resultWithTransitionInfo.result is NoResult)
-            )
+            else if (transitionAllowed(isRequest, resultWithTransitionInfo!!, expectedResult))
                 resultWithTransitionInfo
             else
                 null
         }
 
+        private fun transitionAllowed(isRequest: Boolean, transitionInfo: TransitionInfo, expectedResult: Result) =
+            (transitionInfo.result == expectedResult) ||
+            // Allow transition with a suspended result
+            // regardless whether the operation was suspended during test running or not,
+            // thus allowing elimination of interblocking operations in the implementation.
+            (isRequest && transitionInfo.wasSuspended) ||
+            (transitionInfo.result is ValueResult && expectedResult is ValueResult && transitionInfo.result.value == expectedResult.value && !expectedResult.wasSuspended) ||
+            (transitionInfo.result is ExceptionResult && expectedResult is ExceptionResult && transitionInfo.result.tClazz == expectedResult.tClazz && !expectedResult.wasSuspended) ||
+            (expectedResult == VoidResult && transitionInfo.result == SuspendedVoidResult)
+
         /**
          * Counts or gets the existing relaxed transition from the current state
          * by the given [actor] and [expectedResult].
@@ -207,8 +212,8 @@ class LTS(
                 TransitionInfo(
                     nextState = stateInfo.state,
                     resumedTickets = stateInfo.resumedOperations.map { it.resumedActorTicket }.toSet(),
-                    wasSuspended = result is NoResult,
-                    ticket = if (rf != null && result is NoResult) rf[operation.ticket] else operation.ticket,
+                    wasSuspended = result === Suspended,
+                    ticket = if (rf != null && result === Suspended) rf[operation.ticket] else operation.ticket,
                     rf = rf,
                     result = result
                 )
@@ -236,7 +241,7 @@ class LTS(
                     RelaxedTransitionInfo(
                         nextState = stateInfo.state,
                         resumedTickets = stateInfo.resumedOperations.map { it.resumedActorTicket }.toSet(),
-                        wasSuspended = result is NoResult,
+                        wasSuspended = result === Suspended,
                         ticket = operation.ticket,
                         rf = rf,
                         result = result,
@@ -284,7 +289,7 @@ class LTS(
                 if (isQuantitativelyRelaxed) result else null
             )
         }
-        if (res is NoResult) {
+        if (res === Suspended) {
             // Operation suspended it's execution.
             suspendedOperations.add(this)
         } else {
@@ -574,16 +579,31 @@ abstract class VerifierContext<STATE>(
     /**
      * Current execution scenario.
      */
-    val scenario: ExecutionScenario,
+    protected val scenario: ExecutionScenario,
+    /**
+     * Expected execution results
+     */
+    protected val results: ExecutionResult,
     /**
      * LTS state of this context
      */
-    val state: STATE,
+    val state: State,
     /**
      * Number of executed actors in each thread. Note that initial and post parts
      * are represented as threads with ids `0` and `threads + 1` respectively.
      */
-    val executed: IntArray
+    protected val executed: IntArray = IntArray(scenario.threads + 2),
+    /**
+     * For every scenario thread stores whether it is suspended or not.
+     */
+    protected val suspended: BooleanArray = BooleanArray(scenario.threads + 2),
+    /**
+     * For every thread it stores a ticket assigned to the last executed actor by [LTS].
+     * A ticket is assigned from the range (0 .. threads) to an actor that suspends it's execution,
+     * after being resumed the actor is invoked with this ticket to complete it's execution.
+     * If an actor does not suspend, the assigned ticket equals `-1`.
+     */
+    protected val tickets: IntArray = IntArray(scenario.threads + 2) { -1 }
 ) {
     /**
      * Counts next possible states and the corresponding contexts if the specified thread is executed.
@@ -596,28 +616,34 @@ abstract class VerifierContext<STATE>(
     fun isCompleted(threadId: Int) = executed[threadId] == scenario[threadId].size
 
     /**
-     * Returns the number of threads from the range [[tidFrom]..[tidTo]] (inclusively) which are completed.
+     * Returns `true` if the initial part is completed.
      */
-    private fun completedThreads(tidFrom: Int, tidTo: Int) = (tidFrom..tidTo).count { t -> isCompleted(t) }
+    val initCompleted: Boolean get() = isCompleted(0)
 
     /**
-     * Returns the number of completed scenario threads.
+     * Returns `true` if all actors from the parallel scenario part are executed.
      */
-    val completedThreads: Int get() = completedThreads(0, scenario.threads + 1)
+    val parallelCompleted: Boolean get() = completedThreads(1, scenario.threads) == scenario.threads
 
     /**
-     * Returns `true` if the initial part is completed.
+     * Returns `true` if all threads completed their execution.
      */
-    val initCompleted: Boolean get() = isCompleted(0)
+    val completed: Boolean get() = completedThreads + suspendedThreads == scenario.threads + 2
 
     /**
-     * Returns `true` if all actors from the parallel scenario part are executed.
+     * The number of threads that expectedly suspended their execution.
      */
-    val parallelCompleted: Boolean get() = completedThreads(1, scenario.threads) == scenario.threads
+    private val suspendedThreads: Int
+        get() = (0..scenario.threads + 1).count { t -> suspended[t] && results[t][executed[t]] === Suspended }
 
     /**
-     * Returns `true` if all threads completed their execution.
+     * Returns the number of threads from the range [[tidFrom]..[tidTo]] (inclusively) which are completed.
+     */
+    private fun completedThreads(tidFrom: Int, tidTo: Int) = (tidFrom..tidTo).count { t -> isCompleted(t) }
+
+    /**
+     * Returns the number of completed scenario threads.
      */
-    abstract val completed: Boolean
+    private val completedThreads: Int get() = completedThreads(0, scenario.threads + 1)
 }
 

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/linearizability/LinearizabilityVerifier.kt

@@ -51,7 +51,8 @@ class LinearizabilityVerifier(
     )
 
     override fun createInitialContext(results: ExecutionResult): VerifierContext<LTS.State> =
-        QuantitativelyRelaxedLinearizabilityContext(scenario, lts.initialState, results, relaxationFactor, pathCostFunc)
+        QuantitativelyRelaxedLinearizabilityContext(scenario, results, lts.initialState,
+            PathCostFunction.NON_RELAXED.createIterativePathCostFunctionCounter(0))
 }