DisLog: A Separation Logic for Disentanglement

on YouTube ↗17m

" summary

Claims a first static program logic that proves disentanglement for fork‑join programs and gives a high‑level variant that yields disentanglement for race‑free code DisLog+. Logic embeds unique time stamps so loads require clock assertions and a precedence preorder; weakest preconditions become WP indexed by time and postconditions carry resulting timestamps. Mechanization uses Coq on top of Iris, includes invariants to handle racy patterns, and verifies case studies (spinlock, parallel lookup, lazy collection and two parallel deduplication implementations).

AI-written summary · about

" chapters (14)

1. 0:00Introduction
2. 0:24Disentanglement in parallel programs
3. 2:09Disentanglement for memory
4. 3:56DisLog variants overview
5. 4:20Time stamps and definition
6. 5:44Clock assertions
7. 6:52Precedence assertions and rules
8. 8:37Parallel composition
9. 9:42Races in DisLog Plus
10. 11:28Monotonic predicates
11. 12:53Switching between logics
12. 13:37Read-write races case studies
13. 13:58Conclusion
14. 14:42Q&A