lin-check is a tool for Java that checks linearizability on concurrent data structures.
Lin-check is a testing framework to check that concurrent data structure is linearizable. The approach is based on linearization definition and tries to find non-linearizable execution with specified operations due to a lot of executions. The execution is represented as a list of actors for every test thread, where the actor is the operation with already counted parameters.
The following example tests that ConcurrentHashMap is linearizable.
The artifacts are available in Bintray. For Maven, use
com.devexperts.lincheck:core:<version> artifact for your tests.
The base entity in lin-check is operation. It is defined via public method (should be annotated with @Operation annotation) and generators for every method parameter. Further operations are used to create actors and execute them concurrently.
To generate parameters for operation the
ParameterGenerator implementation is used. Each parameter should have the generator.
Lin-check has generators for all primitive types and String. Note that if an operation has primitive or String parameter then this parameter value is contained in generated byte-code. Thus way, boxing/unboxing does not happen.
Java 8 introduces the feature (JEP 188) to store parameter names to class files. If test class is compiled with storing parameter names to class files then they can be used as the name of the generator.
For example, the following code
is similar to the next one.
Unfortunately, this feature is disabled in javac compiler by default. Use
-parameters option to enable it. For example, in Maven you can use the following plugin configuration:
However, some IDEs (such as IntelliJ IDEA) do not understand build system configuration as well as possible and running test from these IDEs is not worked. To solve this issue you should add
-parameters option for javac compiler in your IDE configuration.
Exception as result
If an operation can throw an exception and this is a normal result (e.g. method remove in Queue implementation throws NoSuchElementException if the queue is empty) you can handle this exception via
@HandleExceptionAsResult annotation on the operation method.
The following example processes NoSuchElementException as a normal result:
@CTest annotation for test class to configure testing parameters. The
@CTest annotation has the following parameters:
- actorsPerThread - the range of actors for each thread (presented as array), should be in the following format:
- iterations - number of iterations to be processed;
- invocationsPerIteration - number of invocations in each iteration. Default value is
Note that one test class can have several
@CTest annotations and each configuration is used for testing.
For every execution lin-check produces about all actors for every thread. If the test is done successfully, no additional information is produced. However, if any invocation is not linearizable lin-check produces information about this execution results and all possible linearizable results.
Here is an example of non-linearizable queue testing:
If you need help, you have a question, or you need further details on how to use lin-check, you can refer to the following resources:
You can use the following e-mail to contact us directly: