Skip to content

Increase Lincheck version to 3.0 #4467

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Increase Lincheck version to 3.0 #4467

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions buildSrc/src/main/kotlin/CommunityProjectsBuild.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,6 +146,7 @@ fun isSnapshotTrainEnabled(project: Project): Boolean {
val firstPartyDependencies = listOf(
"kotlin",
"atomicfu",
"lincheck"
)

fun shouldUseLocalMaven(project: Project): Boolean {
Expand Down
2 changes: 1 addition & 1 deletion gradle.properties
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ benchmarks_jmh_version=1.37
junit_version=4.12
junit5_version=5.7.0
knit_version=0.5.0
lincheck_version=2.18.1
lincheck_version=3.0
dokka_version=2.0.0
org.jetbrains.dokka.experimental.gradle.pluginMode=V2Enabled
org.jetbrains.dokka.experimental.gradle.pluginMode.nowarn=true
Expand Down
3 changes: 2 additions & 1 deletion kotlinx-coroutines-core/build.gradle.kts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ kotlin {
}
jvmTest {
dependencies {
api("org.jetbrains.kotlinx:lincheck:${version("lincheck")}")
api("org.jetbrains.lincheck:lincheck:${version("lincheck")}")
api("org.jetbrains.kotlinx:kotlinx-knit-test:${version("knit")}")
implementation(project(":android-unit-tests"))
implementation("org.openjdk.jol:jol-core:0.16")
Expand Down Expand Up @@ -252,6 +252,7 @@ kover {

// lincheck has NPE error on `ManagedStrategyStateHolder` class
excludedClasses.addAll("org.jetbrains.kotlinx.lincheck.*")
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Historical note: https://repo.maven.apache.org/maven2/org/jetbrains/lincheck/lincheck/3.0/lincheck-3.0.jar does contain classes in both org.jetbrains.lincheck and org.jetbrains.kotlinx.lincheck packages, so keeping these exclusions is intentional.

excludedClasses.addAll("org.jetbrains.lincheck.*")
}
sources {
excludedSourceSets.addAll("benchmark")
Expand Down
4 changes: 1 addition & 3 deletions kotlinx-coroutines-core/jvm/test/AbstractLincheckTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,7 @@
package kotlinx.coroutines

import kotlinx.coroutines.testing.*
import org.jetbrains.kotlinx.lincheck.*
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
import org.jetbrains.kotlinx.lincheck.strategy.stress.*
import org.jetbrains.lincheck.datastructures.*
import org.junit.*

abstract class AbstractLincheckTest {
Expand Down
3 changes: 1 addition & 2 deletions kotlinx-coroutines-core/jvm/test/internal/OnDemandAllocatingPoolLincheckTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,7 @@ package kotlinx.coroutines.internal

import kotlinx.atomicfu.*
import kotlinx.coroutines.*
import org.jetbrains.kotlinx.lincheck.*
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.lincheck.datastructures.*

/**
* Test that:
Expand Down
24 changes: 8 additions & 16 deletions kotlinx-coroutines-core/jvm/test/lincheck/ChannelsLincheckTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,18 +2,13 @@

package kotlinx.coroutines.lincheck

import kotlinx.coroutines.testing.*
import kotlinx.coroutines.*
import kotlinx.coroutines.channels.*
import kotlinx.coroutines.channels.Channel.Factory.CONFLATED
import kotlinx.coroutines.channels.Channel.Factory.RENDEZVOUS
import kotlinx.coroutines.channels.Channel.Factory.UNLIMITED
import kotlinx.coroutines.selects.*
import org.jetbrains.kotlinx.lincheck.*
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.lincheck.datastructures.*

class RendezvousChannelLincheckTest : ChannelLincheckTestBaseWithOnSend(
c = Channel(RENDEZVOUS),
Expand Down Expand Up @@ -80,7 +75,7 @@ abstract class ChannelLincheckTestBaseWithOnSend(
sequentialSpecification: Class<*>,
obstructionFree: Boolean = true
) : ChannelLincheckTestBase(c, sequentialSpecification, obstructionFree) {
@Operation(allowExtraSuspension = true, blocking = true)
@Operation(blocking = true)
suspend fun sendViaSelect(@Param(name = "value") value: Int): Any = try {
select<Unit> { c.onSend(value) {} }
} catch (e: NumberedCancellationException) {
Expand All @@ -98,7 +93,7 @@ abstract class ChannelLincheckTestBase(
private val obstructionFree: Boolean = true
) : AbstractLincheckTest() {

@Operation(allowExtraSuspension = true, blocking = true)
@Operation(blocking = true)
suspend fun send(@Param(name = "value") value: Int): Any = try {
c.send(value)
} catch (e: NumberedCancellationException) {
Expand All @@ -114,14 +109,14 @@ abstract class ChannelLincheckTestBase(
else false
}

@Operation(allowExtraSuspension = true, blocking = true)
@Operation(blocking = true)
suspend fun receive(): Any = try {
c.receive()
} catch (e: NumberedCancellationException) {
e.testResult
}

@Operation(allowExtraSuspension = true, blocking = true)
@Operation(blocking = true)
suspend fun receiveCatching(): Any = c.receiveCatching()
.onSuccess { return it }
.onClosed { e -> return (e as NumberedCancellationException).testResult }
Expand All @@ -132,17 +127,17 @@ abstract class ChannelLincheckTestBase(
.onSuccess { return it }
.onFailure { return if (it is NumberedCancellationException) it.testResult else null }

@Operation(allowExtraSuspension = true, blocking = true)
@Operation(blocking = true)
suspend fun receiveViaSelect(): Any = try {
select<Int> { c.onReceive { it } }
} catch (e: NumberedCancellationException) {
e.testResult
}

@Operation(causesBlocking = true, blocking = true)
@Operation(blocking = true)
fun close(@Param(name = "closeToken") token: Int): Boolean = c.close(NumberedCancellationException(token))

@Operation(causesBlocking = true, blocking = true)
@Operation(blocking = true)
fun cancel(@Param(name = "closeToken") token: Int) = c.cancel(NumberedCancellationException(token))

// @Operation TODO non-linearizable in BufferedChannel
Expand All @@ -154,9 +149,6 @@ abstract class ChannelLincheckTestBase(
// @Operation TODO non-linearizable in BufferedChannel
open fun isEmpty() = c.isEmpty

@StateRepresentation
fun state() = (c as? BufferedChannel<*>)?.toStringDebug() ?: c.toString()
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

With this change, should we also remove toStringDebug() itself? If not, then at least the comment to that function should be updated.


@Validate
fun validate() {
(c as? BufferedChannel<*>)?.checkSegmentStructureInvariants()
Expand Down
9 changes: 3 additions & 6 deletions kotlinx-coroutines-core/jvm/test/lincheck/LockFreeTaskQueueLincheckTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,9 @@ package kotlinx.coroutines.lincheck

import kotlinx.coroutines.*
import kotlinx.coroutines.internal.*
import org.jetbrains.kotlinx.lincheck.*
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.quiescent.*
import org.jetbrains.lincheck.datastructures.*
import org.jetbrains.lincheck.datastructures.verifier.QuiescentConsistencyVerifier
import org.jetbrains.lincheck.datastructures.verifier.QuiescentConsistent

@Param(name = "value", gen = IntGen::class, conf = "1:3")
internal abstract class AbstractLockFreeTaskQueueWithoutRemoveLincheckTest(
Expand Down
11 changes: 4 additions & 7 deletions kotlinx-coroutines-core/jvm/test/lincheck/MutexLincheckTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,16 +4,13 @@ package kotlinx.coroutines.lincheck
import kotlinx.coroutines.*
import kotlinx.coroutines.selects.*
import kotlinx.coroutines.sync.*
import org.jetbrains.kotlinx.lincheck.*
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.annotations.Operation
import org.jetbrains.kotlinx.lincheck.paramgen.*
import org.jetbrains.lincheck.datastructures.*

@Param(name = "owner", gen = IntGen::class, conf = "0:2")
class MutexLincheckTest : AbstractLincheckTest() {
private val mutex = Mutex()

@Operation(handleExceptionsAsResult = [IllegalStateException::class])
@Operation
fun tryLock(@Param(name = "owner") owner: Int) = mutex.tryLock(owner.asOwnerOrNull)

// TODO: `lock()` with non-null owner is non-linearizable
Expand All @@ -22,10 +19,10 @@ class MutexLincheckTest : AbstractLincheckTest() {

// TODO: `onLock` with non-null owner is non-linearizable
// onLock may suspend in case of clause re-registration.
@Operation(allowExtraSuspension = true, promptCancellation = true)
@Operation(promptCancellation = true)
suspend fun onLock() = select<Unit> { mutex.onLock(null) {} }

@Operation(handleExceptionsAsResult = [IllegalStateException::class])
@Operation
fun unlock(@Param(name = "owner") owner: Int) = mutex.unlock(owner.asOwnerOrNull)

@Operation
Expand Down
3 changes: 1 addition & 2 deletions kotlinx-coroutines-core/jvm/test/lincheck/ResizableAtomicArrayLincheckTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,7 @@ package kotlinx.coroutines.lincheck

import kotlinx.coroutines.*
import kotlinx.coroutines.internal.*
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.paramgen.*
import org.jetbrains.lincheck.datastructures.*

@Param(name = "index", gen = IntGen::class, conf = "0:4")
@Param(name = "value", gen = IntGen::class, conf = "1:5")
Expand Down
9 changes: 3 additions & 6 deletions kotlinx-coroutines-core/jvm/test/lincheck/SemaphoreLincheckTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,23 +1,20 @@
@file:Suppress("unused")
package kotlinx.coroutines.lincheck

import kotlinx.coroutines.testing.*
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.*
import org.jetbrains.lincheck.datastructures.*

abstract class SemaphoreLincheckTestBase(permits: Int) : AbstractLincheckTest() {
private val semaphore = SemaphoreAndMutexImpl(permits = permits, acquiredPermits = 0)

@Operation
fun tryAcquire() = semaphore.tryAcquire()

@Operation(promptCancellation = true, allowExtraSuspension = true)
@Operation(promptCancellation = true)
suspend fun acquire() = semaphore.acquire()

@Operation(handleExceptionsAsResult = [IllegalStateException::class])
@Operation
fun release() = semaphore.release()

override fun <O : Options<O, *>> O.customize(isStressTest: Boolean): O =
Expand Down