Add linearizability tests for Mutex and Semaphore

Fixes #1737

Author: ndkoval

gradle.properties

@@ -12,7 +12,7 @@ junit_version=4.12
 atomicfu_version=0.14.2
 knit_version=0.1.3
 html_version=0.6.8
-lincheck_version=2.5.3
+lincheck_version=2.6
 dokka_version=0.9.16-rdev-2-mpp-hacks
 byte_buddy_version=1.9.3
 reactor_vesion=3.2.5.RELEASE

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

@@ -0,0 +1,31 @@
+/*
+ * Copyright 2016-2020 JetBrains s.r.o. Use of this source code is governed by the Apache 2.0 license.
+ */
+@file:Suppress("unused")
+package kotlinx.coroutines.linearizability
+
+import kotlinx.coroutines.*
+import kotlinx.coroutines.sync.*
+import org.jetbrains.kotlinx.lincheck.annotations.Operation
+import org.jetbrains.kotlinx.lincheck.verifier.*
+import org.junit.*
+
+class MutexLCStressTest : VerifierState() {
+    private val mutex = Mutex()
+
+    @Operation
+    fun tryLock() = mutex.tryLock()
+
+    @Operation(cancellableOnSuspension = true)
+    suspend fun lock() = mutex.lock()
+
+    @Operation(handleExceptionsAsResult = [IllegalStateException::class])
+    fun unlock() = mutex.unlock()
+
+    @Test
+    fun test() = LCStressOptionsDefault()
+        .actorsBefore(0)
+        .check(this::class)
+
+    override fun extractState() = mutex.isLocked
+}

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

@@ -0,0 +1,35 @@
+/*
+ * Copyright 2016-2020 JetBrains s.r.o. Use of this source code is governed by the Apache 2.0 license.
+ */
+@file:Suppress("unused")
+package kotlinx.coroutines.linearizability
+
+import kotlinx.coroutines.*
+import kotlinx.coroutines.sync.*
+import org.jetbrains.kotlinx.lincheck.annotations.Operation
+import org.jetbrains.kotlinx.lincheck.verifier.*
+import org.junit.*
+
+abstract class SemaphoreLCStressTestBase(permits: Int) : VerifierState() {
+    private val semaphore = Semaphore(permits)
+
+//    @Operation
+    fun tryAcquire() = semaphore.tryAcquire()
+
+    @Operation(cancellableOnSuspension = true)
+    suspend fun acquire() = semaphore.acquire()
+
+    @Operation(handleExceptionsAsResult = [IllegalStateException::class])
+    fun release() = semaphore.release()
+
+    @Test
+    fun test() = LCStressOptionsDefault()
+        .actorsBefore(0)
+        .check(this::class)
+
+    override fun extractState() = semaphore.availablePermits
+}
+
+class Semaphore1LCStressTest : SemaphoreLCStressTestBase(1)
+class Semaphore2LCStressTest : SemaphoreLCStressTestBase(2)
+class Semaphore4LCStressTest : SemaphoreLCStressTestBase(4)