Add the model checking mode in Lincheck tests

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

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 30)
+        .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 1)
+        .customize(isStressTest)
+
+    override fun extractState(): Any = error("Not implemented")
+}

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

@@ -11,11 +11,11 @@ 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(
     c = Channel(RENDEZVOUS),
@@ -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 ChannelLCStressTestBase(
+    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 LockFreeListLCStressTest : 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 AbstractLockFreeTaskQueueWithoutRemoveLCStressTest protected constructor(singleConsumer: Boolean) : AbstractLincheckTest() {
     @JvmField
     protected val q = LockFreeTaskQueue<Int>(singleConsumer = singleConsumer)
 
@@ -29,12 +28,10 @@ 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)

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 MutexLCStressTest : 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 SegmentListRemoveLCStressTest : 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 SegmentQueueLCStressTest : 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 SemaphoreLCStressTestBase(permits: Int) : AbstractLincheckTest() {
     private val semaphore = Semaphore(permits)
 
     @Operation
@@ -22,10 +21,8 @@ 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
 }