Formal Verification of Python Software Transactional Memory Serializability Based on the Push/Pull Semantic Model
Article No.: 6, Pages 1 - 8
Abstract
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.
References
[1]
M. Herlihy and J. E. B. Moss. Transactional memory: Architectural support for lock-free data structures. In Proceedings of the 20th Annual International Symposium on Computer Architecture, pages 289--300, 1993.
[2]
T. Harris, J. R. Larus, and R. Rajwar. Transactional Memory, 2nd edition, Morgan and Claypool, 2010.
[3]
N. Shavit and D. Touitou. Software transactional memory. In Proceedings of the 14th Annual ACM Symposium on Principles of Distributed Computing (PODC), pages 204--213, 1995.
[4]
M. Popovic and B. Kordic. PSTM: Python software transactional memory. In Proceedings of the 22nd Telecommunications Forum (TELFOR), pages 1106--1109, Belgrade, Serbia, 2014.
[5]
M. Goldstein, E. Fredj, B. Gerber. A New Hybrid Algorithm for Finding the Lowest Minima of Potential Surfaces: Approach and Application to Peptides. In Journal of Computational Chemistry, Volume 32, pages 1785--1800, 2011.
[6]
M. Amitay, M. Goldstein. Evaluating the peptide structure prediction capabilities of a purely ab-initio method. In Protein Engineering, Design and Selection, Volume 30, Issue 10, pages 723--727, 2017.
[7]
M. Popovic, B. Kordic, and I. Basicevic. Transaction Scheduling for Software Transactional Memory. In Proceedings of the 2nd IEEE International Conference on Cloud Computing and Big Data Analysis, pages 191--195, Chengdu, China, 2017.
[8]
M. Popovic, B. Kordic, M. Popovic, I. Basicevic. Online Algorithms for Scheduling Transactions on Python Software Transactional Memory. In Serbian Journal of Electrical Engineering, Volume 16, Issue 1, pages 85--104, 2019.
[9]
M. Popovic, B. Kordic, M. Popovic, and I. Basicevic. A Solution of Concurrent List on PSTM. In Proceedings of the 5th International Conference on Electrical, Electronic and Computer Engineering (IcETRAN), Article RTI2.1, pages 1--6, Palic, Serbia, 2018.
[10]
M. Herlihy and N. Shavit. The art of multiprocessor programming, revised printing, Morgan Kaufmann, 2014.
[11]
M. Popovic, B. Kordic, M. Popovic, and I. Basicevic. A Solution of Concurrent Queue on PSTM. In Proceedings of the 25th IEEE Telecommunications Forum (TELFOR), pages 735--738, Belgrade, Serbia, 2018.
[12]
B. Kordic, M. Popovic, S. Ghilezan, and I. Basicevic. An Approach to Formal Verification of Python Software Transactional Memory. In Proceedings of the 5th European Conference on the Engineering of Computer Based Systems, Article No. 13, pages 1--10, Larnaca, Cyprus, 2017.
[13]
A. Liu, M. Popovic, H. Zhu. Formalization and Verification of the PSTM Architecture. In Proceedings of the 24th Asia-Pacific Software Engineering Conference, pages 427--435, Nanjing, Jiangsu, China, 2017.
[14]
E. Koskinen, M. Parkinson. The Push/Pull Model of Transactions. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 186--195, Portland, Oregon, USA, 2015.
[15]
D. Dimitrov, V. Raychev, M. Vechev, E. Koskinen. Commutativity Race Detection. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 305--315, Edinburgh, UK, 2014.
Index Terms
- Formal Verification of Python Software Transactional Memory Serializability Based on the Push/Pull Semantic Model
Recommendations
An efficient software transactional memory using commit-time invalidation
CGO '10: Proceedings of the 8th annual IEEE/ACM international symposium on Code generation and optimizationTo improve the performance of transactional memory (TM), researchers have found many eager and lazy optimizations for conflict detection, the process of determining if transactions can commit. Despite these optimizations, nearly all TMs perform one ...
Safe privatization in transactional memory
PPoPP '18Transactional memory (TM) facilitates the development of concurrent applications by letting the programmer designate certain code blocks as atomic. Programmers using a TM often would like to access the same data both inside and outside transactions, ...
Safe privatization in transactional memory
PPoPP '18: Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel ProgrammingTransactional memory (TM) facilitates the development of concurrent applications by letting the programmer designate certain code blocks as atomic. Programmers using a TM often would like to access the same data both inside and outside transactions, ...
Comments
Information & Contributors
Information
Published In
September 2019
182 pages
ISBN:9781450376365
DOI:10.1145/3352700
Copyright © 2019 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 02 September 2019
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
ECBS '19
ECBS '19: 6th Conference on the Engineering of Computer Based Systems
September 2 - 3, 2019
Bucharest, Romania
Acceptance Rates
ECBS '19 Paper Acceptance Rate 25 of 49 submissions, 51%;
Overall Acceptance Rate 25 of 49 submissions, 51%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 77Total Downloads
- Downloads (Last 12 months)4
- Downloads (Last 6 weeks)1
Reflects downloads up to 06 Jan 2025
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in