Using cylindric algebra to support local variables in rely/guarantee concurrency

Local variable blocks are a simple but effective program structuring technique. In the context of concurrency, local variables have the added advantage of avoiding interference from threads running concurrently with the thread declaring the local variable. To provide mechanised support for verifying concurrent programs in Isabelle/HOL, we have found making use of algebraic properties of programs simplifies the development of refinement laws. The algebraic properties of local variable blocks are similar to those of existential quantifiers in predicate calculus, the algebra of which is Tarski’s cylindric algebra. Hence to support local variables, we make use of a variant of cylindric algebra that allows quantification of a variable over a command, rather than a predicate. The approach allows a local variable to become a shared variable of parallel threads that are local to the block that introduced the variable.