lincheck

In this version, we added a lincheck guide!

Bug Fixes:

• Fixed LinCheck failing when state representation is not deterministic (#108)
• Fixed non-determinism in the model checker caused by resetting TestThread.cont (#109)
• Equal objects must have different representation numbers (#110)
• Do not transform Kover coverage framework classes

Bug fixes:

1. Do not call Thread.stop() when no hang has been detected (#102)

Improvements:

1. Support thread-local randoms in Striped64 (#97)
2. Fix the missed state equivalence message (#98)
3. Provide default value in ManagedOptions.verboseTrace(..) (#99)
4. Add a nicer Options.addCustomScenario function (#100)
5. Support standard singleton collections representation in model checking traces (#101)

Features

1. Custom scenarios DSL (#8)

Improvements

1. Do not require state equivalence implementation by default (#95)

Bug Fixes

1. OutOfMemoryError when minimizing scenario has been fixed (#93)
2. Fix NoSuchFieldException when a field is inherited from an interface (#84)
3. Handle null-s as results properly (#83)
4. Fix a big in wait/notify processing in model checking (#82)

Improvements

1. Thread.yield should be ignored in model checking (#70)
2. Add a parameter generator for Boolean
3. Handle the exceptions related to invalid access from unnamed modules in model checking and provide the fix in the exception message

Features

1. Add an option for verbose trace for managed strategies (#65)

Improvements

1. Migrate from Maven to Gradle (#54)
2. Improve scenario generation diversity (#62)
3. Remove CheckClassAdapter for faster transformation (#63)

Bug Fixes

1. Add switch points into cancellation handlers for the model checking strategy (#66)
2. Prompt cancellation should be emulated by canceling the parent job (#67)
3. Fixed IllegalAccessError when accessing package-private methods in ThreadLocalRandom after the code transformation for model checking (#64)

Features

1. Allow some of the operations to be blocking while testing for obstruction-freedom (#55, #58)
2. Support prompt cancellation (#57, #59)

Bug Fixes

1. The last event was not logged sometimes on obstruction freedom violation

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.

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)

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)

Features

1. Linearizability support additionally to sequential consistency #33

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

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)

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

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)

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)