{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:08:11Z","timestamp":1784200091937,"version":"3.55.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"name":"NSERC Discovery Grants","award":["RGPIN-2020-05203, RGPIN-2025-06826"],"award-info":[{"award-number":["RGPIN-2020-05203, RGPIN-2025-06826"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>An important correctness gap exists between formally verifiable distributed system designs and their implementations. Recently proposed work bridges this gap by automatically extracting, or compiling, an implementation from the formally-verified design. The runtime behavior of this compiled implementation, however, may deviate from its design. For example, the compiler may contain bugs, the design may make incorrect assumptions about the deployment environment, or the implementation might be misconfigured.<\/jats:p>\n                  <jats:p>In this paper we develop TraceLink, a methodology to detect such deviations through trace validation. TraceLink maps traces, that capture an execution\u2019s behavior, to the corresponding formal design. Unlike previous work on trace validation, our approach is completely automated.<\/jats:p>\n                  <jats:p>\n                    We implement TraceLink for PGo, a compiler from Modular PlusCal to both TLA\n                    <jats:sup>+<\/jats:sup>\n                    and Go. We present a formal semantics for interpreting execution traces as TLA\n                    <jats:sup>+<\/jats:sup>\n                    , along with a templatization strategy to minimize the size of the TLA\n                    <jats:sup>+<\/jats:sup>\n                    tracing specification. We also present a novel trace path validation strategy, called\n                    <jats:italic toggle=\"yes\">sidestep<\/jats:italic>\n                    , which detects bugs faster and with little additional overhead.\n                  <\/jats:p>\n                  <jats:p>\n                    We evaluated TraceLink on several distributed systems, including an MPCal implementation of a Raft key-value store. Our evaluation demonstrates that TraceLink is able to find 9 previously undetected and diverse bugs in PGo\u2019s TCB, including a bug in the PGo compiler itself. We also show the effectiveness of the templatization approach and the\n                    <jats:italic toggle=\"yes\">sidestep<\/jats:italic>\n                    path validation strategy.\n                  <\/jats:p>","DOI":"10.1145\/3763128","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"2171-2198","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["TraceLinking Implementations with Their Verified Designs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8181-6938","authenticated-orcid":false,"given":"Finn","family":"Hackett","sequence":"first","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1676-8834","authenticated-orcid":false,"given":"Ivan","family":"Beschastnikh","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"crossref","unstructured":"Martin Abadi and Leslie Lamport. 1988. The Existence of Refinement Mappings. In Proceedings of the 3rd Annual Symposium on Logic in Computer Science. 165\u2013175.","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_3_2_3_1","doi-asserted-by":"crossref","unstructured":"Ezio Bartocci Yli\u00e8s Falcone Adrian Francalanza and Giles Reger. 2018. Introduction to Runtime Verification.","DOI":"10.1007\/978-3-319-75632-5"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3375633"},{"key":"e_1_3_2_5_1","doi-asserted-by":"crossref","unstructured":"James Bornholt Rajeev Joshi Vytautas Astrauskas Brendan Cully Bernhard Kragl Seth Markle Kyle Sauri Drew Schleit Grant Slatton Serdar Tasiran Jacob Van Geffen and Andrew Warfield. 2021. Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP).","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3712057"},{"key":"e_1_3_2_7_1","doi-asserted-by":"crossref","unstructured":"Sebastian Burckhardt Pravesh Kothari Madanlal Musuvathi and Santosh Nagarakatte. 2010. A randomized scheduler with probabilistic guarantees of finding bugs. In Proceedings of the Fifteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XV). 167\u2013178.","DOI":"10.1145\/1736020.1736040"},{"issue":"1","key":"e_1_3_2_8_1","first-page":"36","article-title":"A Survey of Compiler Testing","volume":"53","author":"Chen Junjie","year":"2020","unstructured":"Junjie Chen, Jibesh Patra, Michael Pradel, Yingfei Xiong, Hongyu Zhang, Dan Hao, and Lu Zhang. 2020. A Survey of Compiler Testing. ACM Comput. Surv. 53, 1, Article 4 (Feb. 2020), 36 pages.","journal-title":"ACM Comput. Surv"},{"key":"e_1_3_2_9_1","first-page":"126","volume-title":"22nd Intl. Conf. Software Engineering and Formal Methods (SEFM 2024) (LNCS, Vol. 15280)","author":"Cirstea Horatiu","year":"2024","unstructured":"Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, and Stephan Merz. 2024. Validating Traces of Distributed Programs Against TLA+ Specifications. In 22nd Intl. Conf. Software Engineering and Formal Methods (SEFM 2024) (LNCS, Vol. 15280), Alexandre Madeira and Alexander Knapp (Eds.). Springer, Aveiro, Portugal, 126\u2013143."},{"key":"e_1_3_2_10_1","doi-asserted-by":"crossref","unstructured":"Pantazis Deligiannis Narayanan Ganapathy Akash Lal and Shaz Qadeer. 2021. Building Reliable Cloud Services Using Coyote Actors. In Proceedings of the ACM Symposium on Cloud computing (SoCC).","DOI":"10.1145\/3472883.3486983"},{"key":"e_1_3_2_11_1","unstructured":"Star Dorminey. 2020. Kayfabe \u2013 model-based program testing. https:\/\/conf.tlapl.us\/2020\/"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-67321-4_6"},{"key":"e_1_3_2_13_1","unstructured":"Yli\u00e8s Falcone Klaus Havelund and Giles Reger. 2013. A Tutorial on Runtime Verification. In Engineering Dependable Software Systems Summer School Marktoberdorf."},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00609-z"},{"key":"e_1_3_2_15_1","first-page":"55","volume-title":"ACSC","author":"Fidge Colin J.","year":"1988","unstructured":"Colin J. Fidge. 1988. Timestamps in Message-Passing Systems that Preserve the Partial Ordering. In ACSC. University of Queensland, Australia, 55\u201366."},{"key":"e_1_3_2_16_1","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan and Patrice Godefroid. 2005. Dynamic partial-order reduction for model checking software. In Symposium on Principles of Programming Languages (POPL).","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_17_1","doi-asserted-by":"crossref","unstructured":"Pedro Fonseca Kaiyuan Zhang Xi Wang and Arvind Krishnamurthy. 2017. An Empirical Study on the Correctness of Formally Verified Distributed Systems. In Proceedings of the European Conference on Computer Systems (EuroSys).","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-35257-7_8"},{"key":"e_1_3_2_19_1","doi-asserted-by":"crossref","unstructured":"Adrian Francalanza Jorge A. P\u00e9rez and C\u00e9sar S\u00e1nchez. 2018. Runtime Verification for Decentralised and Distributed Systems.","DOI":"10.1007\/978-3-319-75632-5_6"},{"key":"e_1_3_2_20_1","doi-asserted-by":"crossref","unstructured":"Stewart Grant Hendrik Cech and Ivan Beschastnikh. 2018. Inferring and Asserting Distributed System Invariants. In Proceedings of the International Conference on Software Engineering (ICSE).","DOI":"10.1145\/3180155.3180199"},{"key":"e_1_3_2_21_1","unstructured":"Ege Berkay Gulcan Burcu Kulahcioglu Ozkan Rupak Majumdar and Srinidhi Nagendra. 2024. Model-guided Fuzzing of Distributed Systems. CoRR abs\/2410.02307 (2024)."},{"key":"e_1_3_2_22_1","unstructured":"Huayang Guo Ming Wu Lidong Zhou Gang Hu Junfeng Yang and Lintao Zhang. 2011. Practical Software Model Checking via Dynamic Interface Reduction. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)."},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Finn Hackett and Ivan Beschastnikh. 2025. TraceLinking Implementations with their Verified Designs (Evaluation). https:\/\/doi.org\/10.5281\/zenodo.16926533 10.5281\/zenodo.16926533","DOI":"10.5281\/zenodo.16926533"},{"key":"e_1_3_2_24_1","doi-asserted-by":"crossref","unstructured":"Finn Hackett Shayan Hosseini Renato Costa Matthew Do and Ivan Beschastnikh. 2023a. Compiling Distributed System Models with PGo. In International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS).","DOI":"10.1145\/3575693.3575695"},{"key":"e_1_3_2_25_1","doi-asserted-by":"crossref","unstructured":"Finn Hackett Joshua Rowe and Markus Alexander Kuppe. 2023b. Understanding Inconsistency in Azure Cosmos DB with TLA+. In International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP). 1\u201312.","DOI":"10.1109\/ICSE-SEIP58684.2023.00006"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3068608"},{"key":"e_1_3_2_27_1","unstructured":"Heidi Howard Markus A. Kuppe Edward Ashton Amaury Chamayou and Natacha Crooks. 2025. Smart Casual Verification of the Confidential Consortium Framework. In USENIX Symposium on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_28_1","doi-asserted-by":"crossref","unstructured":"Marian Hristov and Annette Bieniusa. 2024. Erla+: Translating TLA+ Models into Executable Actor-Based Implementations. In International Workshop on Erlang.","DOI":"10.1145\/3677995.3678190"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2024.3379947"},{"key":"e_1_3_2_30_1","unstructured":"Kyle Kingsbury. 2016. Jepsen. https:\/\/jepsen.io\/"},{"key":"e_1_3_2_31_1","first-page":"30","article-title":"TLA+ Model Checking Made Symbolic","volume":"3","author":"Konnov Igor","year":"2019","unstructured":"Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. 2019. TLA+ Model Checking Made Symbolic. Proceedings of the ACM on Programming Languages (OOPSLA) 3, Article 123 (2019), 30 pages.","journal-title":"Proceedings of the ACM on Programming Languages (OOPSLA)"},{"key":"e_1_3_2_32_1","doi-asserted-by":"crossref","unstructured":"Igor Konnov Markus Kuppe and Stephan Merz. 2022. Specification and Verification with the TLA+ Trifecta: TLC Apalache and TLAPS. In Leveraging Applications of Formal Methods Verification and Validation. Verification Principles.","DOI":"10.1007\/978-3-031-19849-6_6"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.310.6"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_36_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA."},{"key":"e_1_3_2_37_1","unstructured":"Leslie Lamport. 2018. A PlusCal\u2019s User Manual. Online material."},{"key":"e_1_3_2_38_1","unstructured":"Tanakorn Leesatapornwongsa Mingzhe Hao Pallavi Joshi Jeffrey F. Lukman and Haryadi S. Gunawi. 2014. SAMC: Semantic-aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In USENIX Symposium on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_39_1","doi-asserted-by":"crossref","unstructured":"Jeffrey F. Lukman Huan Ke Cesar A. Stuardo Riza O. Suminto Daniar H. Kurniawan Dikaimin Simon Satria Priambada Chen Tian Feng Ye Tanakorn Leesatapornwongsa Aarti Gupta Shan Lu and Haryadi S. Gunawi. 2019. FlyMC: Highly Scalable Testing of Complex Interleavings in Distributed Systems. In Proceedings of the European Conference on Computer Systems (EuroSys).","DOI":"10.1145\/3302424.3303986"},{"issue":"4","key":"e_1_3_2_40_1","first-page":"28","article-title":"Pivot Tracing: Dynamic Causal Monitoring for Distributed Systems","volume":"35","author":"Mace Jonathan","year":"2018","unstructured":"Jonathan Mace, Ryan Roelke, and Rodrigo Fonseca. 2018. Pivot Tracing: Dynamic Causal Monitoring for Distributed Systems. ACM Trans. Comput. Syst. 35, 4, Article 11 (Dec. 2018), 28 pages.","journal-title":"ACM Trans. Comput. Syst"},{"key":"e_1_3_2_41_1","unstructured":"Friedemann Mattern. 1989. Virtual Time and Global States of Distributed Systems. In Parallel and Distributed Algorithms. 215\u2013226."},{"key":"e_1_3_2_42_1","doi-asserted-by":"crossref","unstructured":"Stephan Merz and Hern\u00e1n Vanzetto. 2012. Automatic Verification of TLA+ Proof Obligations with SMT Solvers. In Logic for Programming Artificial Intelligence and Reasoning. 289\u2013303.","DOI":"10.1007\/978-3-642-28717-6_23"},{"key":"e_1_3_2_43_1","unstructured":"Microsoft. 2025. Azure Chaos Studio. https:\/\/azure.microsoft.com\/en-ca\/services\/chaos-studio\/ Accessed: 2025-03-25."},{"key":"e_1_3_2_44_1","doi-asserted-by":"crossref","unstructured":"Luke Nelson James Bornholt Ronghui Gu Andrew Baumann Emina Torlak and Xi Wang. 2019. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP).","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_2_46_1","doi-asserted-by":"crossref","unstructured":"Zhi Niu Luming Dong Yong Zhu and Li Chen. 2022. Verifying Zookeeper based on Model-Based runtime Trace-Checking using TLA+. In Proceedings of the 7th International Conference on Cyber Security and Information Engineering (ICCSIE \u201922). 13\u201318.","DOI":"10.1145\/3558819.3558822"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28121474"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276530"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360606"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330576"},{"key":"e_1_3_2_51_1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. 1977. The Temporal Logic of Programs. In Proceedings of the Annual Symposium on Foundations of Computer Science.","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_52_1","doi-asserted-by":"crossref","unstructured":"Giles Reger and Klaus Havelund. 2016. What Is a Trace? A Runtime Verification Perspective. In Leveraging Applications of Formal Methods Verification and Validation: Discussion Dissemination Applications.","DOI":"10.1007\/978-3-319-47169-3_25"},{"key":"e_1_3_2_53_1","unstructured":"Raja Sambasivan Rodrigo Fonseca Ilari Shafer and Gregory Ganger. 2014. So You Want to Trace Your Distributed System? Key Design Insights from Years of Practical Experience."},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)81041-7"},{"key":"e_1_3_2_55_1","unstructured":"Benjamin H. Sigelman Luiz Andr\u00e9 Barroso Mike Burrows Pat Stephenson Manoj Plakal Donald Beaver Saul Jaspan and Chandan Shanbhag. 2010. Dapper a Large-Scale Distributed Systems Tracing Infrastructure. Technical Report. Google Inc."},{"key":"e_1_3_2_56_1","unstructured":"Jiri Simsa Randy Bryant and Garth Gibson. 2010. dBug: Systematic Evaluation of Distributed Systems. In Proceedings of the 5th International Conference on Systems Software Verification (SSV)."},{"key":"e_1_3_2_57_1","doi-asserted-by":"crossref","unstructured":"Dong Wang Wensheng Dou Yu Gao Chenao Wu Jun Wei and Tao Huang. 2023. Model Checking Guided Testing for Distributed Systems. In Proceedings of the Eighteenth European Conference on Computer Systems (EuroSys \u201923). 127\u2013143.","DOI":"10.1145\/3552326.3587442"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737958"},{"key":"e_1_3_2_59_1","unstructured":"Junfeng Yang Tisheng Chen Ming Wu Zhilei Xu Xuezheng Liu Haoxiang Lin Mao Yang Fan Long Lintao Zhang and Lidong Zhou. 2009. MODIST: Transparent Model Checking of Unmodified Distributed Systems. In Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993532"},{"key":"e_1_3_2_61_1","doi-asserted-by":"crossref","unstructured":"Yuan Yu Panagiotis Manolios and Leslie Lamport. 1999. Model Checking TLA+ Specifications. In Correct Hardware Design and Verification Methods. 54\u201366.","DOI":"10.1007\/3-540-48153-2_6"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763128","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:09:33Z","timestamp":1784196573000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763128"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":60,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763128"],"URL":"https:\/\/doi.org\/10.1145\/3763128","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}