Fenced separation logic formalization
- C11 concurrency model definition
- Program expressions and their semantics
- Assertions
- Additional lemmas about FSL assertions.
- The meaning of triples
- Auxiliary lemmas for the soundness proof
- Various helper lemmas
- Depth metric
- Some lemmas about validly annotated nodes
- Independent heap compatibility
- Synchronization paths
- Data race freedom
- Memory safety
- There are no reads from uninitialized locations
- Lemmas for tracking release and acquire permissions
- Lemmas about non-atomic accesses
- Helper lemmas for triples
- Further lemmas about acquire reads and RMWs
- Adequacy
- Soundness of the proof rules
- Frame
- Consequence
- Disjunction
- Existential quantification
- Values
- Sequential composition (let)
- Parallel composition
- Loops
- Non-atomic allocations
- Non-atomic stores
- Non-atomic loads
- Atomic allocations
- Fences
- Atomic stores
- Atomic loads
- Compare-and-swap (CAS)
- Introduction of ghosts
- Derived FSL rules
- Fetch and modify
- Atomic Reference Counter (ARC)
This page has been generated by coqdoc