Testing single producer single consumer (SPSC) queue with Lin

[kayceesrk]

Is it possible to test SPSC, MPSC, SPMC queues in Lin? I can't seem to find an interface where I can limit the kinds of operations that can limit the number of domains or the nature of the operations. Thanks.

[jmid]

I don't think this is possible with the currently exposed Lin interface.
As you remark, one would need a refined interface where the generated operations differ between domains.
Domain-wise, Lin currently uses exactly 2 spawned domains.

STM is more customizable. For example, here's an STM test of MPSC queues from Saturn that limits consumer operations in one of the child domains: https://github.com/ocaml-multicore/saturn/blob/2a653b676afa45159968a5b46bfbd465dc5b1d2a/test/mpsc_queue/stm_mpsc_queue.ml#L109-L125

AFAICS Saturn runs other PBTs, e.g., single-domain SPSC tests, by writing out the tested QCheck property by hand.

[kayceesrk]

Thanks for the answer. I'm teaching a course on concurrent programming, and Lin seems like the best way to get some correctness guarantees without having to do much more. I will do STM also; it takes a bit more than what I'd like the students to write :-)