lincheck-2.9

This is a very major release that introduces a model checking mode (#40)! In this mode, Lincheck studies all possible schedules with a bounded number of context switches by fully controlling the execution and putting context switches in different locations in threads. In order to make the test time predictable, Lincheck bounds the number of schedules to be studied and increases the number of context switches gradually. The main advantages of the model checking mode are better coverage and providing a trace that reproduces the found error.

lincheck-2.8

Features

1. Allow extra suspensions in the dual data structures formalism (#43, #48)
2. Support Serializable classes as operation parameters and results (#46)
3. Add a mechanism to provide the thread number as an operation parameter (#47)

Bug Fixes

1. Do not show old threads in deadlock/livelock thread dumps (#41)

Improvements

1. Improve the execution performance by Implementing a custom executor for ParallelThreadsRunner that keeps the threads active (#44)

lincheck-2.7

Features

1. Add invariants validation mechanism (#36)

Bug Fixes and Improvements

1. Fix LinkageError when using CancellableContinuation (#37)
2. Improve the quality of error messages and make the verification phase slightly faster (#35)

lincheck-2.6

Features

1. Linearizability support additionally to sequential consistency #33

lincheck-2.5

Improvements

1. Allow extra suspensions in executions
2. Fix starvation on internal spin-loop based synchronizations if the number of available cores is less than the number of scenario threads

lincheck-2.4

Improvements

1. The stress strategy now detects hanging, stops the test and prints the thread dump in this case (#25)
2. It becomes possible to write a part of the test in a superclass (#24)

Breaking Changes

1. We decided to remove quantitative relaxation, it requires too many resources to support it, and we do not use relaxed algorithms in Kotlin (#22)

lincheck-2.3

Features

1. Instead of using the testing data structure in a sequential way to specify the behavior of the operations, it is now possible to use a separate simple implementation as a specification. See sequentialSpecification parameter in both options and annotations.

Bug Fixes

1. There were some bugs fixed with suspend functions support

lincheck-2.2

Features

1. Lincheck tries to minimize scenarios on which the test fails; thus, it is now easier to investigate found bugs (#13)

Bug Fixes

1. Tests do not fail if there is a suspendable operation and the actorsAfter parameter is non-zero (#15)
2. Fixed incorrect exception result representation in logs (#14)
3. Fixed wrong alignment in init/post parts in logs (#10)

Improvements

1. Empty post and init scenarios parts are omitted in logs if they are empty (added under #10)

lincheck 2.1

Main Change

A suspend functions support has been introduced, so that it becomes possible to test data structures like channels or mutexes from the Kotlin Coroutines library; see the corresponding README section.

Improvements

1. Incorrect results representation has become more readable (#2)
2. The synchronization between threads in stress mode has been improved (#4)
3. An optional (enabled by default) check that equals/hashCode methods for verifiers are specified correctly has been introduced (#6)