Authors: Popović, Marko
Popović, Miroslav
Ghilezan, Silvia 
Kordić, Branislav
Title: Formal Verification of Local and Distributed Python Software Transactional Memories
Journal: Revue roumaine des sciences techniques Série Électrotechnique et Énergétique
Volume: 64
Issue: 4
First page: 423
Last page: 428
Issue Date: 14-Oct-2019
Rank: M23
ISSN: 0035-4066
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)
Publisher: Editura Academiei Romane

Show full item record

Page view(s)

checked on May 9, 2024

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.