Concurrent Incorrectness Separation Logic
summary
Develops CISL as a parametric extension of Incorrectness Separation Logic that models concurrency with histories and lock-aware events, instantiates to race, deadlock and memory-safety detectors, and proves a meta-theorem that each instance inherits no false positives. Shows thread-local analysis rules for local and data-agnostic global bugs, encodes existing tools (RacerD, PulseX-like analyses) rather than shipping a new tool, and notes data-dependent races and mechanization remain future work.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:40Overview
- 3:07Problem
- 3:20State of the Art
- 3:52The Problem
- 4:43The Next 700
- 5:18Sizzle
- 6:31Exit Condition
- 7:22Local Bugs
- 9:17Global Bugs
- 10:08Data Dependent Bugs
- 11:44Thread Local Analysis
- 13:44Data Races
- 17:37ReadWrite Access
- 18:28Witness History
- 19:28Example
- 19:57Conclusion
- 20:10Questions
related talks
14mSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
26mDegrees of Separation: A Flexible Type System for Data Race Prevention
20mDegrees of Separation: A Flexible Type System for Safe Concurrency
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
24mA Concurrent Program Logic with a Future and History
15mLilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency