[{"citation":{"chicago":"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.","mla":"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.","short":"T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings of the ACM on Programming Languages 5 (2021).","ista":"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.","ieee":"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.","apa":"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"},"publication":"Proceedings of the ACM on Programming Languages","article_type":"original","date_published":"2021-10-15T00:00:00Z","dc":{"description":["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.\r\n\r\n"],"identifier":["https://research-explorer.ista.ac.at/record/10191","https://research-explorer.ista.ac.at/download/10191/10215"],"type":["info:eu-repo/semantics/article","doc-type:article","text","http://purl.org/coar/resource_type/c_6501"],"creator":["Bui, Truc Lam","Chatterjee, Krishnendu","Gautam, Tushar","Pavlogiannis, Andreas","Toman, Viktor"],"title":["The reads-from equivalence for the TSO and PSO memory models"],"relation":["info:eu-repo/semantics/altIdentifier/doi/10.1145/3485541","info:eu-repo/semantics/altIdentifier/issn/2475-1421","info:eu-repo/semantics/altIdentifier/arxiv/2011.11763","info:eu-repo/grantAgreement/EC/H2020/863818","info:eu-repo/grantAgreement/FWF//ICT15-003"],"publisher":["Association for Computing Machinery"],"subject":["safety","risk","reliability and quality","software","ddc:000"],"source":["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"],"rights":["info:eu-repo/semantics/openAccess"],"language":["eng"],"date":["2021"]},"scopus_import":"1","keyword":[],"article_processing_charge":"No","uri_base":"https://research-explorer.ista.ac.at","has_accepted_license":"1","day":"15","_id":"10191","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","intvolume":" 5","status":"public","ddc":[],"file":[{"access_level":"open_access","file_name":"2021_ProcACMPL_Bui.pdf","content_type":"application/pdf","file_size":2903485,"creator":"cchlebak","relation":"main_file","file_id":"10215","checksum":"9d6dce7b611853c529bb7b1915ac579e","success":1,"date_created":"2021-11-04T07:24:48Z","date_updated":"2021-11-04T07:24:48Z"}],"oa_version":"Published Version","type":"journal_article","issue":"OOPSLA","abstract":[{"lang":"eng"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":[]},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","language":[{}],"publication_identifier":{"eissn":[]},"month":"10","acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science\r\nand Technology Fund (WWTF) through project ICT15-003.","department":[{"_id":"GradSch","tree":[{"_id":"Various"},{"_id":"IST"}]},{"tree":[{"_id":"ResearchGroups"},{"_id":"IST"}],"_id":"KrCh"}],"publication_status":"published","related_material":{"record":[{"id":"10199","relation":"dissertation_contains","status":"public"}]},"author":[{"last_name":"Bui","first_name":"Truc Lam"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Tushar","last_name":"Gautam"},{"first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"},{"orcid":"0000-0001-9036-063X","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","last_name":"Toman","first_name":"Viktor"}],"volume":5,"dini_type":"doc-type:article","date_updated":"2023-09-07T13:30:27Z","date_created":"2021-10-27T15:05:34Z","article_number":"164","ec_funded":1,"file_date_updated":"2021-11-04T07:24:48Z","creator":{"login":"vtoman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}}]