Case Studies
Bugs Laplace finds that production CI did not
Each study reproduces a real deadlock or starvation pattern Laplace surfaced under Ki-DPOR exhaustive verification — with the trace, the minimal repro, and the upstream notification status.
-
std::sync::RwLock + async runtime • 2026-07-11
Case Study 03: Async ref deadlock
A disclosure-pending case study showing how a synchronous RwLock read guard can freeze a single-thread async runtime.
case-study async RwLock deadlock -
crossbeam-channel + parking_lot • 2026-07-11
Case Study 02: Channel mutex AB-BA
A disclosure-pending case study on a bounded channel schedule that exposes AB-BA lock ordering.
case-study crossbeam-channel parking_lot mutex -
rayon • 2026-07-11
Case Study 05: Nested scope deadlock
A disclosure-pending case study showing how nested rayon scopes can preserve a mutex dependency the parent cannot release.
case-study rayon scope mutex -
parking_lot::RwLock • 2026-07-11
Case Study 04: RwLock upgrade
A disclosure-pending case study on a lock upgrade pattern that closes a wait-for cycle through a shared invalidation mutex.
case-study parking_lot RwLock upgrade -
tokio • 2026-07-11
Case Study 01: Tokio watch mutex race
A disclosure-pending case study showing how a watch notification can expose a synchronous mutex held across an async yield.
case-study tokio watch mutex
Want to compare tools head-to-head?
See the same five scenarios run on Loom, Shuttle, Stateright, and madsim on the Benchmark Comparison page.