2017/10/09 by Ian J. Hayes, Larissa Meinicke, Hayes, Ian J. +5 · 1 citation
Computer Science · #Distributed systems and fault tolerance #Parallel Computing and Optimization Techniques #Formal Methods in Verification
paper · pdf · doi:10.48550/arxiv.1710.03352
This research started with an algebra for reasoning about rely/guarantee\nconcurrency for a shared memory model. The approach taken led to a more\nabstract algebra of atomic steps, in which atomic steps synchronise (rather\nthan interleave) when composed in parallel. The algebra of rely/guarantee\nconcurrency then becomes an instantiation of the more abstract algebra. Many of\nthe core properties needed for rely/guarantee reasoning can be shown to hold in\nthe abstract algebra where their proofs are simpler and hence allow a higher\ndegree of automation. The algebra has been encoded in Isabelle/HOL to provide a\nbasis for tool support for program verification.\n In rely/guarantee concurrency, programs are specified to guarantee certain\nbehaviours until assumptions about the behaviour of their environment are\nviolated. When assumptions are violated, program behaviour is unconstrained\n(aborting), and guarantees need no longer hold. To support these guarantees a\nsecond synchronous operator, weak conjunction, was introduced: both processes\nin a weak conjunction must agree to take each atomic step, unless one aborts in\nwhich case the whole aborts. In developing the laws for parallel and weak\nconjunction we found many properties were shared by the operators and that the\nproofs of many laws were essentially the same. This insight led to the idea of\ngeneralising synchronisation to an abstract operator with only the axioms that\nare shared by the parallel and weak conjunction operator, so that those two\noperators can be viewed as instantiations of the abstract synchronisation\noperator. The main differences between parallel and weak conjunction are how\nthey combine individual atomic steps; that is left open in the axioms for the\nabstract operator.\n