JetBrains/lincheck

false positive live locks when upgrading to v2.21

btwilk opened this issue · 3 comments

btwilk commented

Version: 2.21

When trying to upgrade to Lincheck v2.21, I've encountered what I believe to be false positive livelocks. It looks like there is a fixed limit on the complexity of single-threaded execution between context switches. If so, it seems critical to allow customization of this limit. I can work around by optimizing code and minimizing threads/operations/data in the test cases, but it would be preferable to just relax the livelock threshold.

Hi @btwilk, can you provide the failing code and the output, please?

btwilk commented

Unfortunately I can't... If I find time I'll try to make a minimal example. But fyi, I use several low-level data structures like Semaphore and ConcurrentLinkedDeque/LinkedBlockingDeque. I was able to workaround the livelocks by replacing these with simple implementations that just use coarse-grained monitor synchronization. In contrast, the original impls either use park()/unpark() or CAS.

@ndkoval
I work with @btwilk. We could write a simple example that fails the live-lock detection since we cannot share our code.
Although this example seems unrealistic and artificial, a similar behavior actually happened and led to a false-alarm for the live-lock detector.
We'd like to have APIs to adjust thresholds related to the live-lock detection. We know there is already an api ManagedOptions.hangingDetectionThreshold(). We also want to have ManagedOptions.livelockEventsThreshold().
Also, it would be great if we can turn off the live-lock detection in cases we don't need it.

Here's a simple example of generating false-positive live-lock:

import org.jetbrains.kotlinx.lincheck.check
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions
import org.junit.jupiter.api.Test
import java.util.Deque
import java.util.Optional
import java.util.concurrent.ConcurrentLinkedDeque

class ExampleTest {

    @Operation
    fun simple() {
        val value = ByteArray(size = 5) { 0xFF.toByte() }
        val data: Deque<Optional<ByteArray>> = ConcurrentLinkedDeque()
        for (i in 1..2000) {
            data.addLast(Optional.ofNullable(value))
            data.lastOrNull()
        }
    }

    @Test
    fun test() {
        val options = ModelCheckingOptions()
            .threads(1)
            .actorsPerThread(1)
            .actorsBefore(0)
            .actorsAfter(0)
            .iterations(1)
            .invocationsPerIteration(1)
            .check(this::class)
    }
}