Hi! I'm trying to figure out if Lincheck would be ...
# lincheck
c
Hi! I'm trying to figure out if Lincheck would be able to identify a bug we have. We have a data structure that has two kinds of events: events it consumes, and events it emits. To model it under Lincheck, it seems clear to me that events it emits should be modeled as functions with the
Operation
annotation. Reading the documentation, however, I don't understand how events emitted by the structure should be represented. To give a bit more precision: • incoming events are dated. It's possible that we do not receive them in the order in which they were initially created. • there are complex rules w.r.t which outgoing events are emitted based on which incoming events. We suspect our system breaks down in edge cases of: • events which are processed in the incorrect order from their creation date • events which are processed in parallel in a way that is incoherent with the rules. As a simplification, we can represent the structure as:
Copy code
data class Incoming(
    val id: UUID,
    val createdAt: Instant,
    val payload: String,
)

data class Outgoing(
    val id: UUID,
    val createdAt: Instant,
    val payload: String,
)

class SystemUnderTest(
    val emit: (Outgoing) -> Unit,
) {

    fun receive(event: Incoming) {
        // complex logic...
        emit(otherEvent1)
        emit(otherEvent2) // in some cases...
        // ...
    }

}
What would a Lincheck model test for this class look like? I assume something like:
Copy code
class SUTTest {
    private val emit: (Outgoing) -> Unit = // what here??
    private val sut = SystemUnderTest(emit)

    @Operation fun eventType1() { sut.receive(UUID.random(), Instant.random(), "1") }

    @Operation fun eventType2() { sut.receive(UUID.random(), Instant.random(), "2") }
}
But I can't figure out how to represent the different kinds of outgoing events we expect, such that Lincheck can find incoherent sequences.
p
I think this seems similar to the question I asked earlier (and got no response to). Basically, I have the impression that lincheck isn't able to insert its bytecode instructions into classes outside the system under test, so it can't find this type of problem. I didn't spend a lot more time on it, but it feels like if the system under test was wrapped with something where lincheck can insert its barriers, that might work. So not doing the shared state mutation in the test code, but having it in a 'production code wrapper', that can be instrumented. I'm not sure.
c
cc @ndkoval Sorry for the ping, you made the KotlinConf talk so I assume you'd know the answer