Lincheck: Testing concurrency on the JVM
summary
Lincheck verifies concurrent JVM data structures by generating scenarios and running stress or controlled bytecode hooks model checking that switch threads at each shared-memory access. It finds real bugs: a non-atomic bounded queue lets three successful offers against capacity two, a counter loses an increment, and a bug in java.util.concurrent.ConcurrentLinkedDeque was reproduced. Verification checks linearizability and progress (lock-freedom), works with Kotlin and Java, and emits deterministic traces for debugging.
AI-written summary · about
chapters (14)
- 0:00Introduction and motivation
- 1:05AI-generated concurrent queue
- 3:54Limitations of stress testing
- 4:59Ideal concurrent test design
- 6:04First failure with LeanCheck
- 7:10Linearizability explained
- 11:07Analyzing the failure trace
- 13:16How LeanCheck works internally
- 16:48Model checking basics
- 21:04Progress guarantees testing
- 22:32Testing Java standard library
- 25:23LeanCheck in production
- 26:29Summary and call to action
- 27:10Q&A session
related talks
31mLincheck: Testing Concurrent Algorithms on JVM
01h 11mWorkshop. Lincheck: Testing concurrency on the JVM (Part 2)
01h 10mWorkshop. Lincheck: Testing concurrency on the JVM (Part 1)
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
02h 01mWorkshop: Java Concurrency Stress (JCStress). Part 2
36mTesting Stateful and Concurrent Systems Using test.check
32mChecking Concurrency Coding Rules
01h 20mWorkshop: Java Concurrency Stress (JCStress). Part 1