Closed kevinly01 closed 1 year ago
It looks like it is hanging during the linearizability checking phase, which makes sense because it executes operations sequentially to generate valid linearizations. It would be useful if lincheck were able to detect and report this kind of deadlock in linearizability verification.
We need to provide a separate sequential spec that doesn't have these dependencies between operations. E.g., fixing the minimal example:
import org.jetbrains.kotlinx.lincheck.LoggingLevel
import org.jetbrains.kotlinx.lincheck.annotations.Operation
import org.jetbrains.kotlinx.lincheck.check
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions
import org.junit.Test
import java.util.concurrent.Semaphore
class Test {
private val semaphore = Semaphore(0)
init {
println("init")
}
@Operation(nonParallelGroup = "acquire")
fun acquire(): Int {
println("acquire")
semaphore.acquire()
return 1
}
@Operation(nonParallelGroup = "release")
fun release(): Int {
println("release")
semaphore.release()
return 2
}
@Test
fun test() = ModelCheckingOptions()
.sequentialSpecification(SequentialSpec::class.java)
.threads(2)
.actorsPerThread(1)
.actorsBefore(0)
.actorsAfter(0)
.logLevel(LoggingLevel.INFO)
.check(this::class)
class SequentialSpec {
fun acquire(): Int {
return 1
}
fun release(): Int {
return 2
}
}
}
Hi, @kevinly01, thanks for the issue. Lincheck does not support blocking operations for threads at the moment. We are going to fix it under #167. Thus, I'm closing the issue as a duplicate.
Hi I have a use case where I have operations that depend on each other in order to proceed. I've tested the below code using Lincheck 2.23 and 2.18. While running my tests I noticed that despite me specifying the number of actors for the test run, there are some invocations during a iteration where operations are completely skipped. This results in the test eventually hanging due to a dependency on the other operation.
I've replicated a simple scenario below. As you can see during one of the invocations releasing lock is never called. And during the next iteration it hangs and gets stuck on Acquiring the lock. Is there a way to enforce LinCheck calling all actors during a invocation?