The reads-from equivalence for the TSO and PSO memory models
Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. 2021. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 5(OOPSLA), 164.
Download
DOI
Journal Article
| Published
| English
Scopus indexed
Author
Bui, Truc Lam;
Chatterjee, KrishnenduISTA ;
Gautam, Tushar;
Pavlogiannis, AndreasISTA ;
Toman, ViktorISTA
Department
Grant
Abstract
In this work we solve the algorithmic problem of consistency verification for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and VPSO-rf, respectively. For an execution of n events over k threads and d variables, we establish novel bounds that scale as nk+1 for TSO and as nk+1· min(nk2, 2k· d) for PSO. Moreover, based on our solution to these problems, we develop an SMC algorithm under TSO and PSO that uses the RF equivalence. The algorithm is exploration-optimal, in the sense that it is guaranteed to explore each class of the RF partitioning exactly once, and spends polynomial time per class when k is bounded. Finally, we implement all our algorithms in the SMC tool Nidhugg, and perform a large number of experiments over benchmarks from existing literature. Our experimental results show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO, which yields a significant speedup in the model checking task.
Keywords
Publishing Year
Date Published
2021-10-15
Journal Title
Proceedings of the ACM on Programming Languages
Publisher
Association for Computing Machinery
Acknowledgement
The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science
and Technology Fund (WWTF) through project ICT15-003.
Volume
5
Issue
OOPSLA
Article Number
164
eISSN
IST-REx-ID
Cite this
Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 2021;5(OOPSLA). doi:10.1145/3485541
Bui, T. L., Chatterjee, K., Gautam, T., Pavlogiannis, A., & Toman, V. (2021). The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3485541
Bui, Truc Lam, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, and Viktor Toman. “The Reads-from Equivalence for the TSO and PSO Memory Models.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2021. https://doi.org/10.1145/3485541.
T. L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, and V. Toman, “The reads-from equivalence for the TSO and PSO memory models,” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA. Association for Computing Machinery, 2021.
Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. 2021. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 5(OOPSLA), 164.
Bui, Truc Lam, et al. “The Reads-from Equivalence for the TSO and PSO Memory Models.” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA, 164, Association for Computing Machinery, 2021, doi:10.1145/3485541.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
2021_ProcACMPL_Bui.pdf
2.90 MB
Access Level
Open Access
Date Uploaded
2021-11-04
MD5 Checksum
9d6dce7b611853c529bb7b1915ac579e
Material in ISTA:
Dissertation containing ISTA record
Export
Marked PublicationsOpen Data ISTA Research Explorer
Sources
arXiv 2011.11763