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 containing 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 Henkin, Monk and 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.
Mon 15 MayDisplayed time zone: Hobart change
11:00 - 12:30 | |||
11:00 30mPaper | A Dafny-based approach to thread-local information flow analysis FormaliSE 2023 Graeme Smith The University of Queensland | ||
11:30 30mPaper | Transparent Actor Model FormaliSE 2023 Fatemeh Ghassemi University of Tehran, Marjan Sirjani Malardalen University, Ehsan Khamespanah University of Tehran, Mahrokh Mirani Tehran Institute for Advanced Studies, Hossein Hojjat Tehran Institute for Advanced Studies | ||
12:00 30mPaper | Using cylindric algebra to support local variables in rely/guarantee concurrency FormaliSE 2023 |