Authors: Popović, Miroslav
Popović, Marko
Ghilezan, Silvia 
Kordić, Branislav
Title: Formal verification of python software transactional memory serializability based on the push/pull semantic model
Journal: ACM International Conference Proceeding Series
Conference: 6th Conference on the Engineering of Computer-Based Systems, ECBS 2019; Bucharest; Romania; 2 September 2019 through 3 September 2019
Issue Date: 2-Sep-2019
ISBN: 978-1-450-37636-5
DOI: 10.1145/3352700.3352706
The Push/Pull semantic model of transactions has appeared recently as a solution that unifies a wide range of transactional memory algorithms. It has been proved that the push/pull semantic model satisfies serializability, thus one may prove that a given STM satisfies serializability by constructing its push/pull model such that this model satisfies respective correctness criteria. In this paper, we prove that a Python STM implementation is serializable by constructing its Push/Pull model and by showing that the model satisfies the correctness criteria for the relevant push/pull semantic rules. We first identify that modeling Python STM requires only four, out of seven, push/pull operations, namely the operations pull, apply, push, and commit. Next, we introduce the detailed specification of the PSTM transactional algorithm. Then we map the steps of the PSTM transactional algorithm to the respective push/pull semantic rules. Finally, we prove that the PSTM algorithm satisfies the correctness criteria of the respective push/pull semantic rules. We have envisaged this paper to provide interested researchers with a better understanding of PSTM semantics, in order to construct push/pull models of their own STMs more easily.
Keywords: Formal Verification | Push/Pull Semantic Model | Python | Serializability | Software Transactional Memory
Publisher: Association for Computing Machinery
Project: Development of embedded systems with connected services and digital technology 
Development of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education 
Representations of logical structures and formal languages and their application in computing 

Show full item record


checked on May 23, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




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