Add the model checking mode in Lincheck tests (#2326)

* Add the model checking mode to Lincheck tests and use a newer and faster version of it

Co-authored-by: Roman Elizarov <[email protected]>

Author: ndkoval

.gitignore

@@ -4,6 +4,7 @@
 !/.idea/copyright
 !/.idea/codeStyleSettings.xml
 !/.idea/codeStyles
+!/.idea/dictionaries
 *.iml
 .gradle
 .gradletasknamecache

.idea/dictionaries/shared.xml

@@ -12,7 +12,7 @@ junit_version=4.12
 atomicfu_version=0.14.4
 knit_version=0.2.2
 html_version=0.6.8
-lincheck_version=2.7.1
+lincheck_version=2.10
 dokka_version=0.9.16-rdev-2-mpp-hacks
 byte_buddy_version=1.10.9
 reactor_version=3.2.5.RELEASE

gradle.properties

@@ -184,13 +184,22 @@ jvmTest {
     minHeapSize = '1g'
     maxHeapSize = '1g'
     enableAssertions = true
-    systemProperty 'java.security.manager', 'kotlinx.coroutines.TestSecurityManager'
+    if (!Idea.active) {
+        // We should not set this security manager when `jvmTest`
+        // is invoked by IntelliJ IDEA since we need to pass
+        // system properties for Lincheck and stress tests.
+        // TODO Remove once IDEA is smart enough to select between `jvmTest`/`jvmStressTest`/`jvmLincheckTest` #KTIJ-599
+        systemProperty 'java.security.manager', 'kotlinx.coroutines.TestSecurityManager'
+    }
     // 'stress' is required to be able to run all subpackage tests like ":jvmTests --tests "*channels*" -Pstress=true"
     if (!Idea.active && rootProject.properties['stress'] == null) {
+        exclude '**/*LincheckTest.*'
         exclude '**/*StressTest.*'
     }
-    systemProperty 'kotlinx.coroutines.scheduler.keep.alive.sec', '100000' // any unpark problem hangs test
-
+    if (Idea.active) {
+        // Configure the IDEA runner for Lincheck
+        configureJvmForLincheck(jvmTest)
+    }
     // TODO: JVM IR generates different stacktrace so temporary disable stacktrace tests
     if (rootProject.ext.jvm_ir_enabled) {
         filter {
@@ -219,23 +228,41 @@ task jvmStressTest(type: Test, dependsOn: compileTestKotlinJvm) {
     systemProperty 'kotlinx.coroutines.semaphore.maxSpinCycles', '10'
 }
 
+task jvmLincheckTest(type: Test, dependsOn: compileTestKotlinJvm) {
+    classpath = files { jvmTest.classpath }
+    testClassesDirs = files { jvmTest.testClassesDirs }
+    include '**/*LincheckTest.*'
+    enableAssertions = true
+    testLogging.showStandardStreams = true
+    configureJvmForLincheck(jvmLincheckTest)
+}
+
+static void configureJvmForLincheck(task) {
+    task.minHeapSize = '1g'
+    task.maxHeapSize = '6g' // we may need more space for building an interleaving tree in the model checking mode
+    task.jvmArgs = ['--add-opens', 'java.base/jdk.internal.misc=ALL-UNNAMED',   // required for transformation
+                     '--add-exports', 'java.base/jdk.internal.util=ALL-UNNAMED'] // in the model checking mode
+    task.systemProperty 'kotlinx.coroutines.semaphore.segmentSize', '2'
+    task.systemProperty 'kotlinx.coroutines.semaphore.maxSpinCycles', '1' // better for the model checking mode
+}
+
 task jdk16Test(type: Test, dependsOn: [compileTestKotlinJvm, checkJdk16]) {
     classpath = files { jvmTest.classpath }
     testClassesDirs = files { jvmTest.testClassesDirs }
     executable = "$System.env.JDK_16/bin/java"
     exclude '**/*LFStressTest.*' // lock-freedom tests use LockFreedomTestEnvironment which needs JDK8
-    exclude '**/*LCStressTest.*' // lin-check tests use LinChecker which needs JDK8
+    exclude '**/*LincheckTest.*' // Lincheck tests use LinChecker which needs JDK8
     exclude '**/exceptions/**'   // exceptions tests check suppressed exception which needs JDK8
     exclude '**/ExceptionsGuideTest.*'
     exclude '**/RunInterruptibleStressTest.*' // fails on JDK 1.6 due to JDK bug
 }
 
-// Run these tests only during nightly stress test
+// Run jdk16Test test only during nightly stress test
 jdk16Test.onlyIf { project.properties['stressTest'] != null }
 
-// Always run those tests
-task moreTest(dependsOn: [jvmStressTest, jdk16Test])
-build.dependsOn moreTest
+// Always check additional test sets
+task moreTest(dependsOn: [jvmStressTest, jvmLincheckTest, jdk16Test])
+check.dependsOn moreTest
 
 task testsJar(type: Jar, dependsOn: jvmTestClasses) {
     classifier = 'tests'

kotlinx-coroutines-core/build.gradle

@@ -85,6 +85,13 @@ internal open class CancellableContinuationImpl<in T>(
 
     public override val isCancelled: Boolean get() = state is CancelledContinuation
 
+    // We cannot invoke `state.toString()` since it may cause a circular dependency
+    private val stateDebugRepresentation get() = when(state) {
+        is NotCompleted -> "Active"
+        is CancelledContinuation -> "Cancelled"
+        else -> "Completed"
+    }
+
     public override fun initCancellability() {
         setupCancellation()
     }
@@ -503,7 +510,7 @@ internal open class CancellableContinuationImpl<in T>(
 
     // For nicer debugging
     public override fun toString(): String =
-        "${nameString()}(${delegate.toDebugString()}){$state}@$hexAddress"
+        "${nameString()}(${delegate.toDebugString()}){$stateDebugRepresentation}@$hexAddress"
 
     protected open fun nameString(): String =
         "CancellableContinuation"

kotlinx-coroutines-core/common/src/CancellableContinuationImpl.kt

@@ -10,7 +10,7 @@ package kotlinx.coroutines.internal
  * @suppress **This is unstable API and it is subject to change.**
  */
 internal class Symbol(val symbol: String) {
-    override fun toString(): String = symbol
+    override fun toString(): String = "<$symbol>"
 
     @Suppress("UNCHECKED_CAST", "NOTHING_TO_INLINE")
     inline fun <T> unbox(value: Any?): T = if (value === this) null as T else value as T

kotlinx-coroutines-core/common/src/internal/Symbol.kt

@@ -0,0 +1,41 @@
+/*
+ * Copyright 2016-2020 JetBrains s.r.o. Use of this source code is governed by the Apache 2.0 license.
+ */
+package kotlinx.coroutines
+
+import org.jetbrains.kotlinx.lincheck.*
+import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
+import org.jetbrains.kotlinx.lincheck.strategy.stress.*
+import org.jetbrains.kotlinx.lincheck.verifier.*
+import org.junit.*
+
+abstract class AbstractLincheckTest : VerifierState() {
+    open fun <O: Options<O, *>> O.customize(isStressTest: Boolean): O = this
+    open fun ModelCheckingOptions.customize(isStressTest: Boolean): ModelCheckingOptions = this
+    open fun StressOptions.customize(isStressTest: Boolean): StressOptions = this
+
+    @Test
+    fun modelCheckingTest() = ModelCheckingOptions()
+        .iterations(if (isStressTest) 100 else 20)
+        .invocationsPerIteration(if (isStressTest) 10_000 else 1_000)
+        .commonConfiguration()
+        .customize(isStressTest)
+        .check(this::class)
+
+    @Test
+    fun stressTest() = StressOptions()
+        .iterations(if (isStressTest) 100 else 20)
+        .invocationsPerIteration(if (isStressTest) 10_000 else 1_000)
+        .commonConfiguration()
+        .customize(isStressTest)
+        .check(this::class)
+
+    private fun <O : Options<O, *>> O.commonConfiguration(): O = this
+        .actorsBefore(if (isStressTest) 3 else 1)
+        .threads(3)
+        .actorsPerThread(if (isStressTest) 4 else 2)
+        .actorsAfter(if (isStressTest) 3 else 0)
+        .customize(isStressTest)
+
+    override fun extractState(): Any = error("Not implemented")
+}

kotlinx-coroutines-core/jvm/test/AbstractLincheckTest.kt

@@ -3,45 +3,45 @@
  */
 @file:Suppress("unused")
 
-package kotlinx.coroutines.linearizability
+package kotlinx.coroutines.lincheck
 
 import kotlinx.coroutines.*
 import kotlinx.coroutines.channels.*
 import kotlinx.coroutines.channels.Channel.Factory.CONFLATED
 import kotlinx.coroutines.channels.Channel.Factory.RENDEZVOUS
 import kotlinx.coroutines.channels.Channel.Factory.UNLIMITED
 import kotlinx.coroutines.selects.*
+import org.jetbrains.kotlinx.lincheck.*
 import org.jetbrains.kotlinx.lincheck.annotations.*
 import org.jetbrains.kotlinx.lincheck.annotations.Operation
 import org.jetbrains.kotlinx.lincheck.paramgen.*
 import org.jetbrains.kotlinx.lincheck.verifier.*
-import org.junit.*
 
-class RendezvousChannelLCStressTest : ChannelLCStressTestBase(
+class RendezvousChannelLincheckTest : ChannelLincheckTestBase(
     c = Channel(RENDEZVOUS),
     sequentialSpecification = SequentialRendezvousChannel::class.java
 )
 class SequentialRendezvousChannel : SequentialIntChannelBase(RENDEZVOUS)
 
-class Array1ChannelLCStressTest : ChannelLCStressTestBase(
+class Array1ChannelLincheckTest : ChannelLincheckTestBase(
     c = Channel(1),
     sequentialSpecification = SequentialArray1RendezvousChannel::class.java
 )
 class SequentialArray1RendezvousChannel : SequentialIntChannelBase(1)
 
-class Array2ChannelLCStressTest : ChannelLCStressTestBase(
+class Array2ChannelLincheckTest : ChannelLincheckTestBase(
     c = Channel(2),
     sequentialSpecification = SequentialArray2RendezvousChannel::class.java
 )
 class SequentialArray2RendezvousChannel : SequentialIntChannelBase(2)
 
-class UnlimitedChannelLCStressTest : ChannelLCStressTestBase(
+class UnlimitedChannelLincheckTest : ChannelLincheckTestBase(
     c = Channel(UNLIMITED),
     sequentialSpecification = SequentialUnlimitedChannel::class.java
 )
 class SequentialUnlimitedChannel : SequentialIntChannelBase(UNLIMITED)
 
-class ConflatedChannelLCStressTest : ChannelLCStressTestBase(
+class ConflatedChannelLincheckTest : ChannelLincheckTestBase(
     c = Channel(CONFLATED),
     sequentialSpecification = SequentialConflatedChannel::class.java
 )
@@ -51,8 +51,11 @@ class SequentialConflatedChannel : SequentialIntChannelBase(CONFLATED)
     Param(name = "value", gen = IntGen::class, conf = "1:5"),
     Param(name = "closeToken", gen = IntGen::class, conf = "1:3")
 )
-abstract class ChannelLCStressTestBase(private val c: Channel<Int>, private val sequentialSpecification: Class<*>) {
-    @Operation
+abstract class ChannelLincheckTestBase(
+    private val c: Channel<Int>,
+    private val sequentialSpecification: Class<*>
+) : AbstractLincheckTest() {
+    @Operation(promptCancellation = true)
     suspend fun send(@Param(name = "value") value: Int): Any = try {
         c.send(value)
     } catch (e: NumberedCancellationException) {
@@ -74,7 +77,7 @@ abstract class ChannelLCStressTestBase(private val c: Channel<Int>, private val
         e.testResult
     }
 
-    @Operation
+    @Operation(promptCancellation = true)
     suspend fun receive(): Any = try {
         c.receive()
     } catch (e: NumberedCancellationException) {
@@ -96,7 +99,7 @@ abstract class ChannelLCStressTestBase(private val c: Channel<Int>, private val
         e.testResult
     }
 
-    @Operation
+    @Operation(causesBlocking = true)
     fun close(@Param(name = "closeToken") token: Int): Boolean = c.close(NumberedCancellationException(token))
 
     // TODO: this operation should be (and can be!) linearizable, but is not
@@ -113,11 +116,8 @@ abstract class ChannelLCStressTestBase(private val c: Channel<Int>, private val
     // @Operation
     fun isEmpty() = c.isEmpty
 
-    @Test
-    fun test() = LCStressOptionsDefault()
-        .actorsBefore(0)
-        .sequentialSpecification(sequentialSpecification)
-        .check(this::class)
+    override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O =
+        actorsBefore(0).sequentialSpecification(sequentialSpecification)
 }
 
 private class NumberedCancellationException(number: Int) : CancellationException() {

kotlinx-coroutines-core/jvm/test/LCStressOptionsDefault.kt

@@ -3,18 +3,17 @@
  */
 @file:Suppress("unused")
 
-package kotlinx.coroutines.linearizability
+package kotlinx.coroutines.lincheck
 
 import kotlinx.coroutines.*
 import kotlinx.coroutines.internal.*
 import org.jetbrains.kotlinx.lincheck.annotations.*
 import org.jetbrains.kotlinx.lincheck.annotations.Operation
 import org.jetbrains.kotlinx.lincheck.paramgen.*
-import org.jetbrains.kotlinx.lincheck.verifier.*
-import kotlin.test.*
+import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
 
 @Param(name = "value", gen = IntGen::class, conf = "1:5")
-class LockFreeListLCStressTest : VerifierState() {
+class LockFreeListLincheckTest : AbstractLincheckTest() {
     class Node(val value: Int): LockFreeLinkedListNode()
 
     private val q: LockFreeLinkedListHead = LockFreeLinkedListHead()
@@ -43,12 +42,12 @@ class LockFreeListLCStressTest : VerifierState() {
 
     private fun Any.isSame(value: Int) = this is Node && this.value == value
 
-    @Test
-    fun testAddRemoveLinearizability() = LCStressOptionsDefault().check(this::class)
-
     override fun extractState(): Any {
         val elements = ArrayList<Int>()
         q.forEach<Node> { elements.add(it.value) }
         return elements
     }
+
+    override fun ModelCheckingOptions.customize(isStressTest: Boolean) =
+        checkObstructionFreedom()
 }

kotlinx-coroutines-core/jvm/test/linearizability/ChannelsLCStressTest.kt renamed to kotlinx-coroutines-core/jvm/test/lincheck/ChannelsLincheckTest.kt

@@ -3,19 +3,21 @@
  */
 @file:Suppress("unused")
 
-package kotlinx.coroutines.linearizability
+package kotlinx.coroutines.lincheck
 
 import kotlinx.coroutines.*
 import kotlinx.coroutines.internal.*
+import org.jetbrains.kotlinx.lincheck.*
 import org.jetbrains.kotlinx.lincheck.annotations.*
 import org.jetbrains.kotlinx.lincheck.annotations.Operation
 import org.jetbrains.kotlinx.lincheck.paramgen.*
-import org.jetbrains.kotlinx.lincheck.verifier.*
+import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
 import org.jetbrains.kotlinx.lincheck.verifier.quiescent.*
-import kotlin.test.*
 
 @Param(name = "value", gen = IntGen::class, conf = "1:3")
-internal abstract class AbstractLockFreeTaskQueueWithoutRemoveLCStressTest protected constructor(singleConsumer: Boolean) : VerifierState() {
+internal abstract class AbstractLockFreeTaskQueueWithoutRemoveLincheckTest(
+    val singleConsumer: Boolean
+) : AbstractLincheckTest() {
     @JvmField
     protected val q = LockFreeTaskQueue<Int>(singleConsumer = singleConsumer)
 
@@ -25,20 +27,24 @@ internal abstract class AbstractLockFreeTaskQueueWithoutRemoveLCStressTest prote
     @Operation
     fun addLast(@Param(name = "value") value: Int) = q.addLast(value)
 
-    @QuiescentConsistent
-    @Operation(group = "consumer")
-    fun removeFirstOrNull() = q.removeFirstOrNull()
+    override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O =
+        verifier(QuiescentConsistencyVerifier::class.java)
 
     override fun extractState() = q.map { it } to q.isClosed()
 
-    @Test
-    fun testWithRemoveForQuiescentConsistency() = LCStressOptionsDefault()
-        .verifier(QuiescentConsistencyVerifier::class.java)
-        .check(this::class)
+    override fun ModelCheckingOptions.customize(isStressTest: Boolean) =
+        checkObstructionFreedom()
 }
 
-@OpGroupConfig(name = "consumer", nonParallel = false)
-internal class MCLockFreeTaskQueueWithRemoveLCStressTest : AbstractLockFreeTaskQueueWithoutRemoveLCStressTest(singleConsumer = false)
+internal class MCLockFreeTaskQueueWithRemoveLincheckTest : AbstractLockFreeTaskQueueWithoutRemoveLincheckTest(singleConsumer = false) {
+    @QuiescentConsistent
+    @Operation(blocking = true)
+    fun removeFirstOrNull() = q.removeFirstOrNull()
+}
 
 @OpGroupConfig(name = "consumer", nonParallel = true)
-internal class SCLockFreeTaskQueueWithRemoveLCStressTest : AbstractLockFreeTaskQueueWithoutRemoveLCStressTest(singleConsumer = true)
+internal class SCLockFreeTaskQueueWithRemoveLincheckTest : AbstractLockFreeTaskQueueWithoutRemoveLincheckTest(singleConsumer = true) {
+    @QuiescentConsistent
+    @Operation(group = "consumer")
+    fun removeFirstOrNull() = q.removeFirstOrNull()
+}