This project contains the Isabelle/HOL formalisation and soundness proof for a rely/guarantee logic tailored to weak memory models based on a notion of interfering local operation pairs.
- State.thy
- Syntax.thy
- Atomics.thy
- Reordering.thy
- Semantics.thy: Weak memory small step semantics, based on Rob's reordering + forwarding
- Interference.thy: Abstract definition the thread-local interference analysis
- Rules.thy: Thread-local rely/guarantee reasoning
- Transition_Rules.thy
- Soundness.thy: Definition and proof of soundness
- SimAsm