todo:
Concurrent separation logic is an extension of separation logic to handle concurrency. Since the frame rule already takes care of most of the work, the main extension is how to reason about locks, mutexes, and other synchronization mechanisms. Often the answer is that the synchronization mechanism logically owns the resource when the lock (or whatever) is not held.
Papers related to Concurrent separation logic
- A semantics for concurrent separation logic [brookes:tcs:2006]
- Separation logic [ohearn:cacm:2019]
- Resources, concurrency, and local reasoning [ohearn:tcs:2007]
- Sound formal verification of Linux's USB BP keyboard driver [penninckx:nfm:2012]