Roman Elizarov | a7db8ec | 2017-12-21 22:45:12 +0300 | [diff] [blame] | 1 | /* |
Roman Elizarov | 1f74a2d | 2018-06-29 19:19:45 +0300 | [diff] [blame^] | 2 | * Copyright 2016-2018 JetBrains s.r.o. Use of this source code is governed by the Apache 2.0 license. |
Roman Elizarov | a7db8ec | 2017-12-21 22:45:12 +0300 | [diff] [blame] | 3 | */ |
| 4 | |
Roman Elizarov | c43a9be | 2017-11-09 15:38:45 +0300 | [diff] [blame] | 5 | package kotlinx.coroutines.experimental.channels |
| 6 | |
| 7 | import com.devexperts.dxlab.lincheck.LinChecker |
| 8 | import com.devexperts.dxlab.lincheck.annotations.Operation |
| 9 | import com.devexperts.dxlab.lincheck.annotations.Param |
| 10 | import com.devexperts.dxlab.lincheck.annotations.Reset |
| 11 | import com.devexperts.dxlab.lincheck.paramgen.IntGen |
Roman Elizarov | 6129c94 | 2018-01-10 17:34:40 +0300 | [diff] [blame] | 12 | import com.devexperts.dxlab.lincheck.stress.* |
| 13 | import kotlinx.coroutines.experimental.* |
Roman Elizarov | c43a9be | 2017-11-09 15:38:45 +0300 | [diff] [blame] | 14 | import org.junit.Test |
| 15 | |
Roman Elizarov | c43a9be | 2017-11-09 15:38:45 +0300 | [diff] [blame] | 16 | @Param(name = "value", gen = IntGen::class, conf = "1:3") |
Roman Elizarov | 6129c94 | 2018-01-10 17:34:40 +0300 | [diff] [blame] | 17 | class ChannelLinearizabilityTest : TestBase() { |
Roman Elizarov | c43a9be | 2017-11-09 15:38:45 +0300 | [diff] [blame] | 18 | private val lt = LinTesting() |
| 19 | private lateinit var channel: Channel<Int> |
| 20 | |
| 21 | @Reset |
| 22 | fun reset() { |
| 23 | channel = Channel<Int>() |
| 24 | } |
| 25 | |
| 26 | @Operation(runOnce = true) |
| 27 | fun send1(@Param(name = "value") value: Int) = lt.run("send1") { channel.send(value) } |
| 28 | |
| 29 | @Operation(runOnce = true) |
| 30 | fun send2(@Param(name = "value") value: Int) = lt.run("send2") { channel.send(value) } |
| 31 | |
| 32 | @Operation(runOnce = true) |
| 33 | fun send3(@Param(name = "value") value: Int) = lt.run("send3") { channel.send(value) } |
| 34 | |
| 35 | @Operation(runOnce = true) |
| 36 | fun receive1() = lt.run("receive1") { channel.receive() } |
| 37 | |
| 38 | @Operation(runOnce = true) |
| 39 | fun receive2() = lt.run("receive2") { channel.receive() } |
| 40 | |
| 41 | @Operation(runOnce = true) |
| 42 | fun receive3() = lt.run("receive3") { channel.receive() } |
| 43 | |
| 44 | // @Operation(runOnce = true) |
| 45 | // fun close1() = lt.run("close1") { channel.close(IOException("close1")) } |
| 46 | // |
| 47 | // @Operation(runOnce = true) |
| 48 | // fun close2() = lt.run("close2") { channel.close(IOException("close2")) } |
| 49 | |
| 50 | @Test |
| 51 | fun testLinearizability() { |
Roman Elizarov | 6129c94 | 2018-01-10 17:34:40 +0300 | [diff] [blame] | 52 | val options = StressOptions() |
| 53 | .iterations(100) |
| 54 | .invocationsPerIteration(1000 * stressTestMultiplier) |
| 55 | .addThread(1, 3) |
| 56 | .addThread(1, 3) |
| 57 | .addThread(1, 3) |
| 58 | .verifier(LinVerifier::class.java) |
| 59 | LinChecker.check(ChannelLinearizabilityTest::class.java, options) |
Roman Elizarov | c43a9be | 2017-11-09 15:38:45 +0300 | [diff] [blame] | 60 | } |
| 61 | } |