blob: 2b471d7f26d8a3dc026536c07d227491a5944881 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
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.lincheck
import kotlinx.coroutines.*
import kotlinx.coroutines.sync.*
import org.jetbrains.kotlinx.lincheck.*
import org.jetbrains.kotlinx.lincheck.annotations.Operation
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
abstract class SemaphoreLincheckTestBase(permits: Int) : AbstractLincheckTest() {
private val semaphore = Semaphore(permits)
@Operation
fun tryAcquire() = semaphore.tryAcquire()
@Operation(promptCancellation = true, allowExtraSuspension = true)
suspend fun acquire() = semaphore.acquire()
@Operation(handleExceptionsAsResult = [IllegalStateException::class])
fun release() = semaphore.release()
override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O =
actorsBefore(0)
override fun extractState() = semaphore.availablePermits
override fun ModelCheckingOptions.customize(isStressTest: Boolean) =
checkObstructionFreedom()
}
class Semaphore1LincheckTest : SemaphoreLincheckTestBase(1)
class Semaphore2LincheckTest : SemaphoreLincheckTestBase(2)
|
