Lincheck: Testing Concurrent Algorithms on JVM
summary
Lincheck is a JVM/Kotlin testing framework that finds concurrency bugs by inserting bytecode transformation hooks (before-read/before-write) and exhaustively exploring interleavings in a model checking mode (plus a faster stress mode). It reproduces failures with a reproducible trace that shows the exact thread switches, proved able to catch a ChatGPT-made bounded-queue bug where three enqueues succeed on capacity two, uncovered real bugs in coroutines’ channels and mutexes and in ConcurrentLinkedDeque, and drives fixing by running the concurrent implementation sequentially to check linearizability.
AI-written summary · about
chapters (17)
- 0:00Introduction to concurrency
- 1:30Why test concurrent code
- 3:18ChatGPT bounded queue example
- 5:29Problems with manual testing
- 7:14Ideal concurrent testing
- 8:15Introducing Lincheck
- 11:25Understanding linearizability
- 12:50Linearizability examples
- 18:02Bug reproduction with Lincheck
- 19:14How Lincheck works
- 21:24Verifying correctness automatically
- 23:08Bytecode transformation magic
- 24:52Counter test case
- 26:59Lincheck in Kotlin coroutines
- 27:42Bug found in Java library
- 28:46Large-scale algorithm testing
- 30:08Final recommendations
related talks
39mLincheck: Testing concurrency on the JVM
36mTesting Stateful and Concurrent Systems Using test.check
18mMulticoretests - Parallel Testing Libraries for OCaml 5.0
02h 01mWorkshop: Java Concurrency Stress (JCStress). Part 2
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
45mThe Hidden Art of Thread-Safe Programming: Exploring java.util.concurrent
50mThe Hidden Art of Thread-Safe Programming: Exploring java.util.con...
55mJava PathFinder: going to Mars without bugs and deadlocks