Reasoning about Distributed Reconfigurable Systems
summary
Claims a Hoare-style calculus for programs that create/delete nodes and connectors, using a resource logic in the spirit of separation logic and inductive predicates to describe unbounded topologies. Introduces havoc invariants checked by an assume/rely-guarantee style proof system and proves them with cyclic inductive proofs over interaction traces. Demonstrates the method by formally verifying reconfiguration routines for self-adjusting tree and ring architectures and shows the expected deadlock freedom and preservation of token/slot counts.
AI-written summary · about
chapters (17)
- 0:00Start
- 0:17Why is reconfiguration needed?
- 2:08What can possibly go wrong?
- 4:04Proving correctness of a system after reconfiguration
- 4:50What are the configurations?
- 5:16A Logic of Configurations (CL)
- 6:11Adding inductive definitions
- 7:30Programmed reconfigurability
- 8:29An example: token-ring node removal
- 9:43Local Reasoning
- 11:08Sequential composition
- 12:12Back to the proof
- 13:06Proving havoc invariance
- 13:33Havoc triples
- 13:46Cyclic proofs
- 14:36Conclusions
- 14:58References
related talks
24mFormal Verification of a Distributed Dynamic Reconfiguration Protocol
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
52mThink Abstractly, Work Concretely
18mDistributed Causal Memory for Higher-Order Distributed Separation Logic
40mRelational Reasoning in Object-based Programs
54mReasoning about Progress of Concurrent Objects
34mThe Math Behind Distributed Systems
14mA Refinement Methodology for Distributed Programs in Rust