Subsystems Coq Development

This is a machine-checked formalization of the metatheory for the subsystems programming mechanism for provably correct exception handling.

Sources: subsystems.zip

• MyClassical - Some axioms of classical logic
• Syntax - Syntax of commands
• Heap - The heap
• InitState - The initial store, the initial heap.
• Semantics - Step rules
• SemanticsFacts - Some lemmas about the semantics
• DependencySafety - The dependency safety proof
• WaitDependencySafety - The wait dependency safety proof
• Java - Step rules without subsystems (for the erasure property)
• Erasure - The erasure property
• Seplogic - A semantic definition of predicates and separate conjunction (no syntax)
• ProofRules - The program logic
• ExtSeplogic - Predicates that can mention the current subsystem and the set of failed subsystems
• Valid - Validity of a command wrt a normal postcondition and an exceptional postcondition (needed as an intermediary between the proof rules and the small step semantics)
• CorrectValid - Correctness per the proof rules implies validity
• ValidPreservation - Validity of a configuration is preserved by execution steps
• Soundness - Correctness implies absence of assert failures and data races
• ProofRulesExamples - Correctness proofs for some example programs
• ActionTraceRunner - Function that computes the resulting configuration for a given trace of actions
• SemanticsExamples - Some example executions that go wrong.

Global index

Changelog:

• 2008-08-20: Added formalization and proof of wait dependency safety. Minor changes in other places to facilitate the formalization.