Data structure constraints
Some data structures may require a part of operations not to be executed concurrently, such as single-producer single-consumer queues. Lincheck provides out-of-the-box support for such contracts, generating concurrent scenarios according to the restrictions.
Consider the single-consumer queue from the JCTools library. Let's write a test to check correctness of its poll()
, peek()
, and offer(x)
operations.
In your build.gradle(.kts)
file, add the JCTools dependency:
To meet the single-consumer restriction, ensure that all poll()
and peek()
consuming operations are called from a single thread. For that, we can set the nonParallelGroup
parameter of the corresponding @Operation
annotations to the same value, e.g. "consumers"
.
Here is the resulting test:
Here is an example of the scenario generated for this test:
Note that all consuming poll()
and peek()
invocations are performed from a single thread, thus satisfying the "single-consumer" restriction.
Next step
Learn how to check your algorithm for progress guarantees with the model checking strategy.