Fenced Separation Logic
Fenced separation logic (FSL) is a program logic for reasoning about concurrent programs under the C11 memory model. FSL is an extension of relaxed separation logic (RSL) with added support for reasoning about memory fences. Specifically, it extends RSL with two modalidities for describing state that is protected by fences (either by a previous release fence or by a later acquire fence).
Papers
- A program logic for C11 memory fences. (VMCAI 2016)
Marko Doko, Viktor Vafeiadis.
[Paper] [Slides] Coq formalization: [proofs hidden] [proofs visible] [sources] - Tackling Real-Life Relaxed Concurrency with FSL++ (ESOP 2017)
Marko Doko, Viktor Vafeiadis.
[Paper] [Slides] Coq formalization: [proofs hidden] [proofs visible] [sources]
People
- Marko Doko, MPI-SWS
- Viktor Vafeiadis, MPI-SWS