Skip to content

Commit

Permalink
Bump Lincheck version to 2.17 (Kotlin#3720)
Browse files Browse the repository at this point in the history
Signed-off-by: Nikita Koval <[email protected]>
  • Loading branch information
ndkoval committed Apr 19, 2023
1 parent 4bc89e2 commit c1cb323
Show file tree
Hide file tree
Showing 8 changed files with 5 additions and 23 deletions.
2 changes: 1 addition & 1 deletion gradle.properties
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ junit5_version=5.7.0
atomicfu_version=0.20.2
knit_version=0.4.0
html_version=0.7.2
lincheck_version=2.16
lincheck_version=2.17
dokka_version=1.8.10
byte_buddy_version=1.10.9
reactor_version=3.4.1
Expand Down
4 changes: 1 addition & 3 deletions kotlinx-coroutines-core/jvm/test/AbstractLincheckTest.kt
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ import org.jetbrains.kotlinx.lincheck.strategy.stress.*
import org.jetbrains.kotlinx.lincheck.verifier.*
import org.junit.*

abstract class AbstractLincheckTest : VerifierState() {
abstract class AbstractLincheckTest {
open fun <O: Options<O, *>> O.customize(isStressTest: Boolean): O = this
open fun ModelCheckingOptions.customize(isStressTest: Boolean): ModelCheckingOptions = this
open fun StressOptions.customize(isStressTest: Boolean): StressOptions = this
Expand Down Expand Up @@ -41,6 +41,4 @@ abstract class AbstractLincheckTest : VerifierState() {
.actorsPerThread(if (isStressTest) 3 else 2)
.actorsAfter(if (isStressTest) 3 else 0)
.customize(isStressTest)

override fun extractState(): Any = error("Not implemented")
}
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,6 @@ abstract class OnDemandAllocatingPoolLincheckTest(maxCapacity: Int) : AbstractLi

@Operation
fun close(): String = pool.close().sorted().toString()

override fun extractState(): Any = pool.stateRepresentation()
}

abstract class OnDemandAllocatingSequentialPool(private val maxCapacity: Int) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.annotations.Operation
import org.jetbrains.kotlinx.lincheck.paramgen.*
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
import org.jetbrains.kotlinx.lincheck.verifier.*

class RendezvousChannelLincheckTest : ChannelLincheckTestBaseWithOnSend(
c = Channel(RENDEZVOUS),
Expand Down Expand Up @@ -176,7 +175,7 @@ private class NumberedCancellationException(number: Int) : CancellationException
}


abstract class SequentialIntChannelBase(private val capacity: Int) : VerifierState() {
abstract class SequentialIntChannelBase(private val capacity: Int) {
private val senders = ArrayList<Pair<CancellableContinuation<Any>, Int>>()
private val receivers = ArrayList<CancellableContinuation<Any>>()
private val buffer = ArrayList<Int>()
Expand Down Expand Up @@ -266,8 +265,6 @@ abstract class SequentialIntChannelBase(private val capacity: Int) : VerifierSta
if (closedMessage !== null) return false
return buffer.isEmpty() && senders.isEmpty()
}

override fun extractState() = buffer to closedMessage
}

private fun <T> CancellableContinuation<T>.resume(res: T): Boolean {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,6 @@ internal abstract class AbstractLockFreeTaskQueueWithoutRemoveLincheckTest(
override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O =
verifier(QuiescentConsistencyVerifier::class.java)

override fun extractState() = q.map { it } to q.isClosed()

override fun ModelCheckingOptions.customize(isStressTest: Boolean) =
checkObstructionFreedom()
}
Expand All @@ -42,9 +40,8 @@ internal class MCLockFreeTaskQueueWithRemoveLincheckTest : AbstractLockFreeTaskQ
fun removeFirstOrNull() = q.removeFirstOrNull()
}

@OpGroupConfig(name = "consumer", nonParallel = true)
internal class SCLockFreeTaskQueueWithRemoveLincheckTest : AbstractLockFreeTaskQueueWithoutRemoveLincheckTest(singleConsumer = true) {
@QuiescentConsistent
@Operation(group = "consumer")
@Operation(nonParallelGroup = "consumer")
fun removeFirstOrNull() = q.removeFirstOrNull()
}
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,5 @@ class MutexLincheckTest : AbstractLincheckTest() {
override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O =
actorsBefore(0)

// state[i] == true <=> mutex.holdsLock(i) with the only exception for 0 that specifies `null`.
override fun extractState() = (1..2).map { mutex.holdsLock(it) } + mutex.isLocked

private val Int.asOwnerOrNull get() = if (this == 0) null else this
}
Original file line number Diff line number Diff line change
Expand Up @@ -11,17 +11,14 @@ import org.jetbrains.kotlinx.lincheck.paramgen.*

@Param(name = "index", gen = IntGen::class, conf = "0:4")
@Param(name = "value", gen = IntGen::class, conf = "1:5")
@OpGroupConfig(name = "sync", nonParallel = true)
class ResizableAtomicArrayLincheckTest : AbstractLincheckTest() {
private val a = ResizableAtomicArray<Int>(2)

@Operation
fun get(@Param(name = "index") index: Int): Int? = a[index]

@Operation(group = "sync")
@Operation(nonParallelGroup = "writer")
fun set(@Param(name = "index") index: Int, @Param(name = "value") value: Int) {
a.setSynchronized(index, value)
}

override fun extractState() = (0..4).map { a[it] }
}
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,6 @@ abstract class SemaphoreLincheckTestBase(permits: Int) : AbstractLincheckTest()
override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O =
actorsBefore(0)

override fun extractState() = semaphore.availablePermits

override fun ModelCheckingOptions.customize(isStressTest: Boolean) =
checkObstructionFreedom()
}
Expand Down

0 comments on commit c1cb323

Please sign in to comment.