Paper title: FORMAL VERIFICATION OF LOCAL AND DISTRIBUTED PYTHON SOFTWARE TRANSACTIONAL MEMORIES
Author(s): MARKO POPOVIC, MIROSLAV POPOVIC, SILVIA GHILEZAN, BRANISLAV KORDIC,
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.
Keywords: Formal verification, Push/pull semantic model, Serializability, Python, Software transactional memory (STM) Year: 2019 | Tome: 64 | Issue: 4 | Pp.: 423-428
Full text : PDF (267 KB) |