Formal Verification of Local and Distributed Python Software Transactional Memories

Abstract

Both local and distributed Python STMs are targeting a wide range of application domains, including critical infrastructures, such as cyber-physical systems, internet of things, etc., and formal verification of such software components is considered mandatory. Recently, the push/pull semantic model of transactions has appeared as a solution that unifies a wide range of transactional memory algorithms. In this paper, we formally prove that both local and distributed Python STM implementations are serializable by constructing their push/pull model and by showing that the push/pull model satisfies the correctness criteria for the relevant push/pull semantic rules. The main contributions of the paper are the following: (i) the PSTM and DPSTM push/pull semantic model, (ii) the proofs of the relevant push/pull semantic rules, and (iii) the way how the model and the proofs have been constructed.