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

Author: ndkoval

gradle.properties

@@ -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.9
 dokka_version=0.9.16-rdev-2-mpp-hacks
 byte_buddy_version=1.10.9
 reactor_version=3.2.5.RELEASE

kotlinx-coroutines-core/build.gradle

@@ -180,6 +180,7 @@ jvmTest {
     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
@@ -205,12 +206,26 @@ 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 }
+    minHeapSize = '1g'
+    maxHeapSize = '10g' // we may need more space for building an interleaving tree in the model checking mode
+    include '**/*LincheckTest.*'
+    enableAssertions = true
+    testLogging.showStandardStreams = true
+    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
+    systemProperty 'kotlinx.coroutines.semaphore.segmentSize', '2'
+    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
@@ -220,7 +235,7 @@ task jdk16Test(type: Test, dependsOn: [compileTestKotlinJvm, checkJdk16]) {
 jdk16Test.onlyIf { project.properties['stressTest'] != null }
 
 // Always run those tests
-task moreTest(dependsOn: [jvmStressTest, jdk16Test])
+task moreTest(dependsOn: [jvmStressTest, jvmLincheckTest, jdk16Test])
 build.dependsOn moreTest
 
 task testsJar(type: Jar, dependsOn: jvmTestClasses) {

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

@@ -0,0 +1,37 @@
+/*
+ * 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
+
+    @Test
+    fun modelCheckingTest() = ModelCheckingOptions()
+        .iterations(if (isStressTest) 100 else 20)
+        .invocationsPerIteration(if (isStressTest) 10_000 else 1_000)
+        .commonConfiguration()
+        .check(this::class)
+
+    @Test
+    fun stressTest() = StressOptions()
+        .iterations(if (isStressTest) 100 else 20)
+        .invocationsPerIteration(if (isStressTest) 10_000 else 1_000)
+        .commonConfiguration()
+        .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/LCStressOptionsDefault.kt

@@ -11,37 +11,37 @@ 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,7 +51,10 @@ 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<*>) {
+abstract class ChannelLincheckTestBase(
+    private val c: Channel<Int>,
+    private val sequentialSpecification: Class<*>
+) : AbstractLincheckTest() {
     @Operation
     suspend fun send(@Param(name = "value") value: Int): Any = try {
         c.send(value)
@@ -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/linearizability/ChannelsLCStressTest.kt

@@ -10,11 +10,9 @@ 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.*
 
 @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,9 +41,6 @@ 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) }

kotlinx-coroutines-core/jvm/test/linearizability/LockFreeListLCStressTest.kt

@@ -7,15 +7,14 @@ package kotlinx.coroutines.linearizability
 
 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.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 protected constructor(singleConsumer: Boolean) : AbstractLincheckTest() {
     @JvmField
     protected val q = LockFreeTaskQueue<Int>(singleConsumer = singleConsumer)
 
@@ -29,16 +28,14 @@ internal abstract class AbstractLockFreeTaskQueueWithoutRemoveLCStressTest prote
     @Operation(group = "consumer")
     fun removeFirstOrNull() = q.removeFirstOrNull()
 
-    override fun extractState() = q.map { it } to q.isClosed()
+    override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O =
+        verifier(QuiescentConsistencyVerifier::class.java)
 
-    @Test
-    fun testWithRemoveForQuiescentConsistency() = LCStressOptionsDefault()
-        .verifier(QuiescentConsistencyVerifier::class.java)
-        .check(this::class)
+    override fun extractState() = q.map { it } to q.isClosed()
 }
 
 @OpGroupConfig(name = "consumer", nonParallel = false)
-internal class MCLockFreeTaskQueueWithRemoveLCStressTest : AbstractLockFreeTaskQueueWithoutRemoveLCStressTest(singleConsumer = false)
+internal class MCLockFreeTaskQueueWithRemoveLincheckTest : AbstractLockFreeTaskQueueWithoutRemoveLincheckTest(singleConsumer = false)
 
 @OpGroupConfig(name = "consumer", nonParallel = true)
-internal class SCLockFreeTaskQueueWithRemoveLCStressTest : AbstractLockFreeTaskQueueWithoutRemoveLCStressTest(singleConsumer = true)
+internal class SCLockFreeTaskQueueWithRemoveLincheckTest : AbstractLockFreeTaskQueueWithoutRemoveLincheckTest(singleConsumer = true)

kotlinx-coroutines-core/jvm/test/linearizability/LockFreeTaskQueueLCStressTest.kt

@@ -6,11 +6,10 @@ package kotlinx.coroutines.linearizability
 
 import kotlinx.coroutines.*
 import kotlinx.coroutines.sync.*
+import org.jetbrains.kotlinx.lincheck.*
 import org.jetbrains.kotlinx.lincheck.annotations.Operation
-import org.jetbrains.kotlinx.lincheck.verifier.*
-import org.junit.*
 
-class MutexLCStressTest : VerifierState() {
+class MutexLincheckTest : AbstractLincheckTest() {
     private val mutex = Mutex()
 
     @Operation
@@ -22,10 +21,8 @@ class MutexLCStressTest : VerifierState() {
     @Operation(handleExceptionsAsResult = [IllegalStateException::class])
     fun unlock() = mutex.unlock()
 
-    @Test
-    fun test() = LCStressOptionsDefault()
-        .actorsBefore(0)
-        .check(this::class)
+    override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O =
+        actorsBefore(0)
 
     override fun extractState() = mutex.isLocked
 }

kotlinx-coroutines-core/jvm/test/linearizability/MutexLCStressTest.kt

@@ -8,14 +8,11 @@ package kotlinx.coroutines.linearizability
 
 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.junit.*
 
-
-class SegmentListRemoveLCStressTest : VerifierState() {
+class SegmentListRemoveLincheckTest : AbstractLincheckTest() {
     private val q = SegmentBasedQueue<Int>()
     private val segments: Array<OneElementSegment<Int>>
 
@@ -29,17 +26,14 @@ class SegmentListRemoveLCStressTest : VerifierState() {
         segments[index].removeSegment()
     }
 
+    override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O = this
+        .actorsBefore(0).actorsAfter(0)
+
     override fun extractState() = segments.map { it.logicallyRemoved }
 
     @Validate
     fun checkAllRemoved() {
         q.checkHeadPrevIsCleaned()
         q.checkAllSegmentsAreNotLogicallyRemoved()
     }
-
-    @Test
-    fun test() = LCStressOptionsDefault()
-        .actorsBefore(0)
-        .actorsAfter(0)
-        .check(this::class)
 }

kotlinx-coroutines-core/jvm/test/linearizability/SegmentListRemoveLCStressTest.kt

@@ -10,11 +10,9 @@ import kotlinx.coroutines.internal.SegmentBasedQueue
 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.*
 
 @Param(name = "value", gen = IntGen::class, conf = "1:5")
-class SegmentQueueLCStressTest : VerifierState() {
+class SegmentQueueLincheckTest : AbstractLincheckTest() {
     private val q = SegmentBasedQueue<Int>()
 
     @Operation
@@ -39,7 +37,4 @@ class SegmentQueueLCStressTest : VerifierState() {
         val closed = q.enqueue(0) === null
         return elements to closed
     }
-
-    @Test
-    fun test() = LCStressOptionsDefault().check(this::class)
 }

kotlinx-coroutines-core/jvm/test/linearizability/SegmentQueueLCStressTest.kt

@@ -6,11 +6,10 @@ package kotlinx.coroutines.linearizability
 
 import kotlinx.coroutines.*
 import kotlinx.coroutines.sync.*
+import org.jetbrains.kotlinx.lincheck.*
 import org.jetbrains.kotlinx.lincheck.annotations.Operation
-import org.jetbrains.kotlinx.lincheck.verifier.*
-import org.junit.*
 
-abstract class SemaphoreLCStressTestBase(permits: Int) : VerifierState() {
+abstract class SemaphoreLincheckTestBase(permits: Int) : AbstractLincheckTest() {
     private val semaphore = Semaphore(permits)
 
     @Operation
@@ -22,13 +21,11 @@ abstract class SemaphoreLCStressTestBase(permits: Int) : VerifierState() {
     @Operation(handleExceptionsAsResult = [IllegalStateException::class])
     fun release() = semaphore.release()
 
-    @Test
-    fun test() = LCStressOptionsDefault()
-        .actorsBefore(0)
-        .check(this::class)
+    override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O =
+        actorsBefore(0)
 
     override fun extractState() = semaphore.availablePermits
 }
 
-class Semaphore1LCStressTest : SemaphoreLCStressTestBase(1)
-class Semaphore2LCStressTest : SemaphoreLCStressTestBase(2)
+class Semaphore1LincheckTest : SemaphoreLincheckTestBase(1)
+class Semaphore2LincheckTest : SemaphoreLincheckTestBase(2)