AllowExtraSuspension parameter deprecated, SUSPENDED prefix removed f…

…rom the output (#339) --------- Co-authored-by: Aleksandr.Potapov <[email protected]>
JetBrains · Jul 17, 2024 · 1a6f1c1 · 1a6f1c1
1 parent 26f2bb6
commit 1a6f1c1
Show file tree

Hide file tree

Showing 19 changed files with 256 additions and 148 deletions.
diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Actor.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Actor.kt
@@ -24,7 +24,6 @@ data class Actor @JvmOverloads constructor(
     val method: Method,
     val arguments: List<Any?>,
     val cancelOnSuspension: Boolean = false,
-    val allowExtraSuspension: Boolean = false,
     val blocking: Boolean = false,
     val causesBlocking: Boolean = false,
     val promptCancellation: Boolean = false,

diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestStructure.java b/src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestStructure.java
@@ -126,7 +126,7 @@ private static void readTestStructureFromClass(
                     gens.add(parameterGenerator);
                 }
                 ActorGenerator actorGenerator = new ActorGenerator(m, gens, opAnn.runOnce(),
-                    opAnn.cancellableOnSuspension(), opAnn.allowExtraSuspension(), opAnn.blocking(), opAnn.causesBlocking(),
+                    opAnn.cancellableOnSuspension(), opAnn.blocking(), opAnn.causesBlocking(),
                     opAnn.promptCancellation());
                 actorGenerators.add(actorGenerator);
                 // Get list of groups and add this operation to specified ones

diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Result.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Result.kt
@@ -24,36 +24,26 @@ import kotlin.coroutines.*
  * the execution thread was suspended without any chance to be resumed,
  * meaning that all other execution threads completed their execution or were suspended too.
  */
-sealed class Result {
-    abstract val wasSuspended: Boolean
-    protected val wasSuspendedPrefix: String get() = (if (wasSuspended) "SUSPENDED + " else "")
-}
+sealed interface Result
 
 /**
  * Type of result used if the actor invocation returns any value.
  */
-data class ValueResult @JvmOverloads constructor(val value: Any?, override val wasSuspended: Boolean = false) : Result() {
-    override fun toString() = wasSuspendedPrefix + "$value"
+data class ValueResult @JvmOverloads constructor(val value: Any?) : Result {
+    override fun toString() = "$value"
 }
 
 /**
  * Type of result used if the actor invocation does not return value.
  */
-object VoidResult : Result() {
-    override val wasSuspended get() = false
-    override fun toString() = wasSuspendedPrefix + VOID
-}
-
-object SuspendedVoidResult : Result() {
-    override val wasSuspended get() = true
-    override fun toString() = wasSuspendedPrefix + VOID
+object VoidResult : Result {
+    override fun toString() = VOID
 }
 
 private const val VOID = "void"
 
-object Cancelled : Result() {
-    override val wasSuspended get() = true
-    override fun toString() = wasSuspendedPrefix + "CANCELLED"
+object Cancelled : Result {
+    override fun toString() = "CANCELLED"
 }
 
 /**
@@ -63,64 +53,53 @@ class ExceptionResult private constructor(
     /**
      * Exception is stored to print it's stackTrace in case of incorrect results
      */
-    val throwable: Throwable,
-    override val wasSuspended: Boolean,
-    /**
-     * Normalized version of the exception class
-     */
-    tClazz: Class<out Throwable>,
-) : Result() {
+    val throwable: Throwable
+) : Result {
+
+    internal val tClassCanonicalName: String get() = throwable::class.java.canonicalName
 
-    val tClassCanonicalName: String = tClazz.canonicalName
-    override fun toString() = wasSuspendedPrefix + throwable::class.java.simpleName
+    override fun toString(): String = throwable::class.java.simpleName
     override fun equals(other: Any?): Boolean {
         if (this === other) return true
         if (other !is ExceptionResult) return false
 
         if (tClassCanonicalName != other.tClassCanonicalName) return false
-        return wasSuspended == other.wasSuspended
+        return true
     }
 
     override fun hashCode(): Int {
-        var result = tClassCanonicalName.hashCode()
-        result = 31 * result + wasSuspended.hashCode()
-        return result
+        return tClassCanonicalName.hashCode()
     }
 
 
     companion object {
         @Suppress("UNCHECKED_CAST")
         @JvmOverloads
-        fun create(throwable: Throwable, wasSuspended: Boolean = false) =
-            ExceptionResult(throwable, wasSuspended, throwable::class.java)
+        fun create(throwable: Throwable) = ExceptionResult(throwable)
     }
 }
 
 // for byte-code generation
 @JvmSynthetic
-fun createExceptionResult(throwable: Throwable) = ExceptionResult.create(throwable, false)
+fun createExceptionResult(throwable: Throwable) = ExceptionResult.create(throwable)
 
 /**
  * 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 val wasSuspended get() = false
+object NoResult : Result {
     override fun toString() = "-"
 }
 
-object Suspended : Result() {
-    override val wasSuspended get() = true
-    override fun toString() = "S"
+object Suspended : Result {
+    override fun toString() = "Suspended"
 }
 
 /**
  * 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() {
-    override val wasSuspended: Boolean get() = true
-
+internal data class ResumedResult(val contWithSuspensionPointRes: Pair<Continuation<Any?>?, kotlin.Result<Any?>>) : Result {
     lateinit var resumedActor: Actor
     lateinit var by: Actor
 }
diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt
@@ -113,23 +113,21 @@ private val Any?.isPrimitiveWrapper get() = when (this) {
  * Success values of [kotlin.Result] instances are represented as either [VoidResult] or [ValueResult].
  * 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 Unit -> if (wasSuspended) SuspendedVoidResult else VoidResult
-    res != null && res is Throwable -> ExceptionResult.create(res, wasSuspended)
+internal fun createLincheckResult(res: Any?) = when {
+    (res != null && res.javaClass.isAssignableFrom(Void.TYPE)) || res is Unit -> VoidResult
+    res != null && res is Throwable -> ExceptionResult.create(res)
     res === COROUTINE_SUSPENDED -> Suspended
-    res is kotlin.Result<Any?> -> res.toLinCheckResult(wasSuspended)
-    else -> ValueResult(res, wasSuspended)
+    res is kotlin.Result<Any?> -> res.toLinCheckResult()
+    else -> ValueResult(res)
 }
 
-private fun kotlin.Result<Any?>.toLinCheckResult(wasSuspended: Boolean) =
+private fun kotlin.Result<Any?>.toLinCheckResult() =
     if (isSuccess) {
         when (val value = getOrNull()) {
-            is Unit -> if (wasSuspended) SuspendedVoidResult else VoidResult
-            // Throwable was returned as a successful result
-            is Throwable -> ValueResult(value::class.java, wasSuspended)
-            else -> ValueResult(value, wasSuspended)
+            is Unit -> VoidResult
+            else -> ValueResult(value)
         }
-    } else ExceptionResult.create(exceptionOrNull()!!, wasSuspended)
+    } else ExceptionResult.create(exceptionOrNull()!!)
 
 inline fun <R> Throwable.catch(vararg exceptions: Class<*>, block: () -> R): R {
     if (exceptions.any { this::class.java.isAssignableFrom(it) }) {

diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/annotations/Operation.java b/src/jvm/main/org/jetbrains/kotlinx/lincheck/annotations/Operation.java
@@ -67,8 +67,11 @@
      * is set to `true`) even if it should not according to the sequential
      * specification. The one may consider this as a relaxation of the
      * dual data structures formalism.
+     *
+     * @deprecated extra suspensions are now allowed for all operations
      */
-    boolean allowExtraSuspension() default false;
+    @Deprecated(forRemoval = true)
+    boolean allowExtraSuspension() default true;
 
     /**
      * Specifies whether this operation is blocking.

diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ActorGenerator.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ActorGenerator.kt
@@ -24,7 +24,6 @@ class ActorGenerator(
     private val parameterGenerators: List<ParameterGenerator<*>>,
     val useOnce: Boolean,
     cancellableOnSuspension: Boolean,
-    private val allowExtraSuspension: Boolean,
     private val blocking: Boolean,
     private val causesBlocking: Boolean,
     promptCancellation: Boolean
@@ -42,7 +41,6 @@ class ActorGenerator(
             method = method,
             arguments = parameters,
             cancelOnSuspension = cancelOnSuspension,
-            allowExtraSuspension = allowExtraSuspension,
             blocking = blocking,
             causesBlocking = causesBlocking,
             promptCancellation = promptCancellation

diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt
@@ -117,7 +117,7 @@ internal open class ParallelThreadsRunner(
                     }
                 }
                 // write function's final result
-                suspensionPointResults[iThread][actorId] = createLincheckResult(result, wasSuspended = true)
+                suspensionPointResults[iThread][actorId] = createLincheckResult(result)
             }
         }
 

diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/TestThreadExecutionGenerator.java b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/TestThreadExecutionGenerator.java
@@ -53,9 +53,6 @@ public class TestThreadExecutionGenerator {
     private static final Type VOID_RESULT_TYPE = getType(VoidResult.class);
     private static final String VOID_RESULT_CLASS_NAME = VoidResult.class.getCanonicalName().replace('.', '/');
 
-    private static final Type SUSPENDED_VOID_RESULT_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 = getType(ValueResult.class);
@@ -304,7 +301,7 @@ private static void createVoidResult(Actor actor, GeneratorAdapter mv) {
             mv.ifCmp(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());
+            mv.visitFieldInsn(GETSTATIC, VOID_RESULT_CLASS_NAME, INSTANCE, VOID_RESULT_TYPE.getDescriptor());
         } else {
             mv.pop();
             mv.visitFieldInsn(GETSTATIC, VOID_RESULT_CLASS_NAME, INSTANCE, VOID_RESULT_TYPE.getDescriptor());

diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TraceReporter.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TraceReporter.kt
@@ -288,7 +288,7 @@ private class ExecutionResultsProvider(result: ExecutionResult?, failure: Linche
                 .toMap()
         }
         if (failure is ValidationFailure) {
-            results[0 to firstThreadActorCount(failure)] = ExceptionResult.create(failure.exception, false)
+            results[0 to firstThreadActorCount(failure)] = ExceptionResult.create(failure.exception)
         }
         threadNumberToActorResultMap = results
     }

diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/verifier/LTS.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/verifier/LTS.kt
@@ -91,9 +91,9 @@ class LTS(private val sequentialSpecification: Class<*>) {
             // Check whether the current actor allows an extra suspension and the the expected result is `Cancelled` while the
             // constructed transition does not suspend -- we can simply consider that this cancelled invocation does not take
             // any effect and remove it from the history.
-            if (actor.allowExtraSuspension && expectedResult == Cancelled && transitionInfo.result != Suspended)
+            if (expectedResult == Cancelled && transitionInfo.result != Suspended)
                 return atomicallySuspendedAndCancelledTransition
-            return if (expectedResult.isLegalByRequest(transitionInfo, actor.allowExtraSuspension)) transitionInfo else null
+            return if (expectedResult.isLegalByRequest(transitionInfo)) transitionInfo else null
         }
 
         private fun nextByFollowUp(actor: Actor, ticket: Int, expectedResult: Result): TransitionInfo? {
@@ -108,7 +108,7 @@ class LTS(private val sequentialSpecification: Class<*>) {
             check(transitionInfo.result != Suspended) {
                 "Execution of the follow-up part of this operation ${actor.method} suspended - this behaviour is not supported"
             }
-            return if (expectedResult.isLegalByFollowUp(transitionInfo, actor.allowExtraSuspension)) transitionInfo else null
+            return if (expectedResult.isLegalByFollowUp(transitionInfo)) transitionInfo else null
         }
 
         fun nextByCancellation(actor: Actor, ticket: Int): TransitionInfo = transitionsByCancellations.computeIfAbsent(ticket) {
@@ -121,20 +121,13 @@ class LTS(private val sequentialSpecification: Class<*>) {
             }
         }
 
-        private fun Result.isLegalByRequest(transitionInfo: TransitionInfo, allowExtraSuspension: Boolean) =
-            isLegalByFollowUp(transitionInfo, allowExtraSuspension) ||
-            this.wasSuspended && (transitionInfo.result == Suspended || allowExtraSuspension) ||
-            !this.wasSuspended && transitionInfo.result == Suspended
+        private fun Result.isLegalByRequest(transitionInfo: TransitionInfo) =
+            isLegalByFollowUp(transitionInfo) || transitionInfo.result == Suspended
 
-        private fun Result.isLegalByFollowUp(transitionInfo: TransitionInfo, allowExtraSuspension: Boolean) =
+        private fun Result.isLegalByFollowUp(transitionInfo: TransitionInfo) =
             this == transitionInfo.result ||
-            this is ValueResult && transitionInfo.result is ValueResult && this.value == transitionInfo.result.value &&
-                (!wasSuspended && transitionInfo.result.wasSuspended || wasSuspended && allowExtraSuspension) ||
-            this is ExceptionResult && transitionInfo.result is ExceptionResult && this.tClassCanonicalName == transitionInfo.result.tClassCanonicalName &&
-                (!wasSuspended && transitionInfo.result.wasSuspended || wasSuspended && allowExtraSuspension) ||
-            this == VoidResult && transitionInfo.result == SuspendedVoidResult ||
-            this == SuspendedVoidResult && transitionInfo.result == VoidResult && allowExtraSuspension
-
+            this is ValueResult && transitionInfo.result is ValueResult && this.value == transitionInfo.result.value  ||
+            this is ExceptionResult && transitionInfo.result is ExceptionResult && this.tClassCanonicalName == transitionInfo.result.tClassCanonicalName
 
         private inline fun <T> copyAndApply(
             action: (
@@ -205,7 +198,7 @@ class LTS(private val sequentialSpecification: Class<*>) {
                         resumedOperations[ticket]!!.contWithSuspensionPointRes.second
                     })
                 resumedOperations.remove(ticket)
-                createLincheckResult(finalRes, wasSuspended = true)
+                createLincheckResult(finalRes)
             }
             CANCELLATION -> {
                 continuationsMap[Operation(this.actor, this.ticket, REQUEST)]!!.cancelByLincheck(promptCancellation = actor.promptCancellation)

diff --git a/...jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/ParallelThreadsRunnerExceptionTest.kt b/...jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/ParallelThreadsRunnerExceptionTest.kt
@@ -91,7 +91,7 @@ class ParallelThreadsRunnerExceptionTest {
             parallel {
                 thread {
                     operation(
-                        actor(susWithoutException), ExceptionResult.create(SuspendResumeScenarios.TestException(), wasSuspended = true)
+                        actor(susWithoutException), ExceptionResult.create(SuspendResumeScenarios.TestException())
                     )
                 }
                 thread {
@@ -115,7 +115,7 @@ class ParallelThreadsRunnerExceptionTest {
             parallel {
                 thread {
                     operation(
-                        actor(susResumeThrow), ExceptionResult.create(SuspendResumeScenarios.TestException(), wasSuspended = true)
+                        actor(susResumeThrow), ExceptionResult.create(SuspendResumeScenarios.TestException())
                     )
                 }
                 thread {

diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/ResumingFollowUpTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/ResumingFollowUpTest.kt
@@ -57,7 +57,7 @@ class ResumingFollowUpTest {
         verify(ResumingFollowUpTest::class.java, LinearizabilityVerifier::class.java, {
             parallel {
                 thread {
-                    operation(actor(f), ValueResult("OK", wasSuspended = true))
+                    operation(actor(f), ValueResult("OK"))
                 }
                 thread {
                     operation(actor(b, 1), ValueResult(true))

diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/AllowExtraSuspensionTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/AllowExtraSuspensionTest.kt
@@ -36,7 +36,7 @@ class AllowExtraSuspensionCorrectTest : AbstractLincheckTest() {
     }
 }
 
-class AllowExtraSuspensionIncorrectTest : AbstractLincheckTest(IncorrectResultsFailure::class) {
+class AllowExtraSuspensionIncorrectTest : AbstractLincheckTest() {
     private val mutex = Mutex()
     private var counter = AtomicInteger()
 

diff --git a/.../test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/BufferedChannelTest.kt b/.../test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/BufferedChannelTest.kt
@@ -21,10 +21,10 @@ import org.jetbrains.kotlinx.lincheck_test.*
 class BufferedChannelTest : AbstractLincheckTest() {
     private val c = Channel<Int>(2)
 
-    @Operation(cancellableOnSuspension = false, allowExtraSuspension = true)
+    @Operation(cancellableOnSuspension = false)
     suspend fun send(@Param(name = "value") value: Int) = c.send(value)
 
-    @Operation(cancellableOnSuspension = false, allowExtraSuspension = true)
+    @Operation(cancellableOnSuspension = false)
     suspend fun receive() = c.receive()
 
     @Operation