parameter generator 100% correlated with operation generator

[btwilk]

Version: 2.15 I was introducing defects into my code on the expectation that lincheck would detect them and ran into a false negative. Here is a minimal example.

@Param(name = "key", gen = IntGen::class, conf = "0:1")
class RandomLinTest {

    private val array = IntArray(size = 2)

    @Operation
    fun get(@Param(name = "key") key: Int) = array[key]

    @Operation
    fun inc(@Param(name = "key") key: Int) {
        array[key] += 1
    }

    @Test
    fun test() = ModelCheckingOptions().logLevel(LoggingLevel.INFO).check(this::class)
}

Although these operations are clearly not linearizable, lincheck doesn't detect it. Inspecting one of the generated test cases reveals why:

= Iteration 1 / 100 =
Execution scenario (init part):
[inc(1), inc(1), get(0), inc(1), inc(1)]
Execution scenario (parallel part):
| get(0) | inc(1) |
| get(0) | inc(1) |
| inc(1) | get(0) |
| get(0) | get(0) |
| inc(1) | inc(1) |
Execution scenario (post part):
[inc(1), inc(1), get(0), inc(1), get(0)]

Every get() is for key 0 and every inc() is for key 1. This is because operation generation and int generation use separate Random instances with the same seed.

[alefedor]

Hi @btwilk ! Thank you for this nice bug example. You are totally right, in this case, the binary Randoms for operation type generation and for parameter generation correlate due to the same seed

[ndkoval]

Let's make the seeds different.