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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
/*
* Copyright 2016-2018 JetBrains s.r.o. Use of this source code is governed by the Apache 2.0 license.
*/
@file:Suppress("unused")
package kotlinx.coroutines.channels
import com.devexperts.dxlab.lincheck.*
import com.devexperts.dxlab.lincheck.annotations.*
import com.devexperts.dxlab.lincheck.paramgen.*
import com.devexperts.dxlab.lincheck.stress.*
import kotlinx.coroutines.*
import org.junit.*
import java.io.*
@Param(name = "value", gen = IntGen::class, conf = "1:3")
class ChannelIsClosedLinearizabilityTest : TestBase() {
private val lt = LinTesting()
private lateinit var channel: Channel<Int>
@Reset
fun resetChannel() {
channel = Channel()
}
@Operation(runOnce = true)
fun send1(@Param(name = "value") value: Int) = lt.run("send1") { channel.send(value) }
@Operation(runOnce = true)
fun send2(@Param(name = "value") value: Int) = lt.run("send2") { channel.send(value) }
@Operation(runOnce = true)
fun receive1() = lt.run("receive1") { channel.receive() }
@Operation(runOnce = true)
fun receive2() = lt.run("receive2") { channel.receive() }
@Operation(runOnce = true)
fun close1() = lt.run("close1") { channel.close(IOException("close1")) }
@Operation(runOnce = true)
fun isClosedForReceive() = lt.run("isClosedForReceive") { channel.isClosedForReceive }
@Operation(runOnce = true)
fun isClosedForSend() = lt.run("isClosedForSend") { channel.isClosedForSend }
@Test
fun testLinearizability() {
val options = StressOptions()
.iterations(100)
.invocationsPerIteration(1000 * stressTestMultiplier)
.addThread(1, 3)
.addThread(1, 3)
.addThread(1, 3)
.verifier(LinVerifier::class.java)
.injectExecution { actors, methods ->
actors[0].add(actorMethod(methods, "receive1"))
actors[0].add(actorMethod(methods, "receive2"))
actors[0].add(actorMethod(methods, "close1"))
actors[1].add(actorMethod(methods, "send2"))
actors[1].add(actorMethod(methods, "send1"))
actors[2].add(actorMethod(methods, "isClosedForSend"))
}
LinChecker.check(ChannelIsClosedLinearizabilityTest::class.java, options)
}
}
|
