here's the 'biggest' test I've written:

class FireAtLeastOnceConsumerLincheckTest {
    private val observed = ConcurrentLinkedQueue<String>()
    private val observer = FireAtLeastOnceConsumer<String> { observed.add(it) }

    @Operation
    fun consume(item: String) = observer.consume(item)

    @Operation
    fun sendIfUnfired(item: String) = observer.consumeIfFirst(item)

    @Operation
    fun poll() = observed.poll()

    @Test
    fun modelTest() = ModelCheckingOptions()
        .sequentialSpecification(SequentialFireAtLeastOnceObserver::class.java)
        .check(this::class)

    @Test
    fun stressTest() = StressOptions()
        .sequentialSpecification(SequentialFireAtLeastOnceObserver::class.java)
        .check(this::class)
}

class SequentialFireAtLeastOnceObserver()  {
    private var fired = false
    private val queue = mutableListOf<String>()

    public fun sendIfUnfired(value: String) {
        if (!fired) {
            consume(value)
        }
    }
    public fun consume(data: String) {
        fired = true

        queue.add(data)
    }

    public fun poll() = queue.removeFirstOrNull()

    override fun equals(other: Any?): Boolean {
        if (this === other) return true
        if (javaClass != other?.javaClass) return false

        other as SequentialFireAtLeastOnceObserver

        if (fired != other.fired) return false
        return queue == other.queue
    }

    override fun hashCode(): Int {
        var result = fired.hashCode()
        result = 31 * result + queue.hashCode()
        return result
    }
}

This succeeds, meaning lincheck doesn't find the race.

If I use a

mutableListOf<String>()

as the

observed

field, then it fails because of concurrent updates to the ArrayList.

I think the problem is that the unsafe write doesn't happen in the

FireAtLeastOnceConsumer

, but in some other class. I guess that means Lincheck is unable to insert its bytecode checks in the right place. Is that reasonable? How might one solve this?

(I'm mostly interested in feedback on how to test this, not on whether it's a good approach to solving a real problem 🙂 )