Stateless model checking under a reads-value-from equivalence
Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. 2021. Stateless model checking under a reads-value-from equivalence. 33rd International Conference on Computer-Aided Verification . CAV: Computer Aided Verification , LNCS, vol. 12759, 341–366.
Download
Conference Paper
| Published
| English
Scopus indexed
Author
Agarwal, Pratyush;
Chatterjee, KrishnenduISTA ;
Pathak, Shreya;
Pavlogiannis, AndreasISTA ;
Toman, ViktorISTA
Department
Grant
Series Title
LNCS
Abstract
Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present RVF-SMC , a new SMC algorithm that uses a novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover, RVF-SMC generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.
Publishing Year
Date Published
2021-07-15
Proceedings Title
33rd International Conference on Computer-Aided Verification
Publisher
Springer Nature
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
12759
Page
341-366
Conference
CAV: Computer Aided Verification
Conference Location
Virtual
Conference Date
2021-07-20 – 2021-07-23
ISBN
ISSN
eISSN
IST-REx-ID
Cite this
Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. Stateless model checking under a reads-value-from equivalence. In: 33rd International Conference on Computer-Aided Verification . Vol 12759. Springer Nature; 2021:341-366. doi:10.1007/978-3-030-81685-8_16
Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., & Toman, V. (2021). Stateless model checking under a reads-value-from equivalence. In 33rd International Conference on Computer-Aided Verification (Vol. 12759, pp. 341–366). Virtual: Springer Nature. https://doi.org/10.1007/978-3-030-81685-8_16
Agarwal, Pratyush, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. “Stateless Model Checking under a Reads-Value-from Equivalence.” In 33rd International Conference on Computer-Aided Verification , 12759:341–66. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-81685-8_16.
P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, and V. Toman, “Stateless model checking under a reads-value-from equivalence,” in 33rd International Conference on Computer-Aided Verification , Virtual, 2021, vol. 12759, pp. 341–366.
Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. 2021. Stateless model checking under a reads-value-from equivalence. 33rd International Conference on Computer-Aided Verification . CAV: Computer Aided Verification , LNCS, vol. 12759, 341–366.
Agarwal, Pratyush, et al. “Stateless Model Checking under a Reads-Value-from Equivalence.” 33rd International Conference on Computer-Aided Verification , vol. 12759, Springer Nature, 2021, pp. 341–66, doi:10.1007/978-3-030-81685-8_16.
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_LNCS_Agarwal.pdf
1.52 MB
Access Level
Open Access
Date Uploaded
2022-05-13
MD5 Checksum
4b346e5fbaa8b9bdf107819c7b2aadee
Material in ISTA:
Dissertation containing ISTA record
Export
Marked PublicationsOpen Data ISTA Research Explorer
Web of Science
View record in Web of Science®Sources
arXiv 2105.06424