Workshop. Lincheck: Testing concurrency on the JVM (Part 1)
summary
Lincheck is a JVM testing tool (Kotlin examples) that declares operations and a correctness contract (default: linearizability) and runs either stress or bounded model‑checking. A simple volatile counter test reproduces a lost update because add isn’t atomic (counter shows lost update). Stress finds failures but not traces; model checking explores bounded context switches and model checking produces exact interleaving so you get a reproducible trace. Example findings: LongAdder is not linearizable for inc+dec+sum and a GC‑tools nonblocking hashmap put/get bug is exposed. Use IntelliJ; iterations default to thousands.
AI-written summary · about
chapters (22)
- 0:00Intro
- 3:27Workshop overview
- 6:06Counter example
- 8:28Running the test
- 14:29Results
- 16:24What is correctness
- 18:16Language ability
- 21:59Writing the test
- 29:29Troubleshooting
- 31:47Stress testing
- 32:33Stress
- 33:17Model checking
- 35:34How model checking works
- 38:29Where to use stress and model checking
- 39:46Scenario configurations
- 39:58Scenario actors
- 41:35Weak memory test
- 44:39Parameter generation annotation
- 48:33Shared parameter generation annotation
- 49:39Custom parameter generation annotation
- 51:56Example
- 53:38Questions
related talks
39mLincheck: Testing concurrency on the JVM
45mHow we test concurrent algorithms in Kotlin Coroutines
36mTesting Stateful and Concurrent Systems Using test.check
30mJCStress: Diving into Concurrency and Distributed Systems in Java
50mThe Hidden Art of Thread-Safe Programming: Exploring java.util.con...
45mThe Hidden Art of Thread-Safe Programming: Exploring java.util.concurrent
18mMulticoretests - Parallel Testing Libraries for OCaml 5.0
10mEfficient Decrease-And-Conquer Linearizability Monitoring