You appear to be one of the authors, so forgive me asking a technical question.
In the technical paper, Section 5.4 you mention that kotlin has non-determinism in the scheduler. Where does this non-determinism come from?
It seems unclear to me why Kotlin would inject randomness here, and I suspect that you may actually have identified a false positive in the Lincheck DSL.
The "randomness" comes from Kotlin coroutines and user-space scheduling. For example, Kotlin runs multiple user-space threads on the same physical thread. Fray only reschedules physical threads. So when testing applications use coroutine/virtual threads, Fray cannot generate certain thread interleavings. Also, It cannot deterministically replay because the thread execution is no longer controlled by Fray.
In our paper, we found that Fray suffers from false negatives because of this missing feature. Lincheck supports Kotlin coroutines so it finds one more bug than Fray in LC-Bench.
We didn't make any claims about false positives in Lincheck.
In the technical paper, Section 5.4 you mention that kotlin has non-determinism in the scheduler. Where does this non-determinism come from?
It seems unclear to me why Kotlin would inject randomness here, and I suspect that you may actually have identified a false positive in the Lincheck DSL.