{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:02:57Z","timestamp":1779087777690,"version":"3.51.4"},"reference-count":87,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>Understanding and debugging the performance of distributed systems is a notoriously hard task, but a critical one. Traditional techniques like logging, tracing, and benchmarking represent a best-effort way to find performance bugs, but they either require a full deployment to be effective or can only find bugs after they manifest. Even with such techniques in place, real deployments often exhibit performance bugs that cause unwanted behavior.<\/jats:p>\n          <jats:p>In this paper, we present Performal, a novel methodology that leverages the recent advances in formal verification to provide rigorous latency guarantees for real, complex distributed systems. The task is not an easy one: it requires carefully decoupling the formal proofs from the execution environment, formally defining latency properties, and proving them on real, distributed implementations. We used Performal to prove rigorous upper bounds for the latency of three applications: a distributed lock, ZooKeeper and a MultiPaxos-based State Machine Replication system. Our experimental evaluation shows that these bounds are a good proxy for the behavior of the deployed system and can be used to identify performance bugs in real-world systems.<\/jats:p>","DOI":"10.1145\/3591235","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"368-393","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Performal: Formal Verification of Latency Properties for Distributed Systems"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-0288-8270","authenticated-orcid":false,"given":"Tony Nuda","family":"Zhang","sequence":"first","affiliation":[{"name":"University of Michigan, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5446-3284","authenticated-orcid":false,"given":"Upamanyu","family":"Sharma","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4368-7418","authenticated-orcid":false,"given":"Manos","family":"Kapritsos","sequence":"additional","affiliation":[{"name":"University of Michigan, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7812534"},{"key":"e_1_2_1_2_1","unstructured":"Akamai. 2017. The state of online retail performance. https:\/\/www.akamai.com\/newsroom\/press-release\/akamai-releases-spring-2017-state-of-online-retail-performance-report \t\t\t\t  Akamai. 2017. The state of online retail performance. https:\/\/www.akamai.com\/newsroom\/press-release\/akamai-releases-spring-2017-state-of-online-retail-performance-report"},{"key":"e_1_2_1_3_1","volume-title":"Timed Automata","author":"Alur Rajeev","unstructured":"Rajeev Alur . 1999. Timed Automata . In Computer Aided Verification, Nicolas Halbwachs and Doron Peled (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 8\u201322. isbn:978-3-540-48683-1 Rajeev Alur. 1999. Timed Automata. In Computer Aided Verification, Nicolas Halbwachs and Doron Peled (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 8\u201322. isbn:978-3-540-48683-1"},{"key":"e_1_2_1_4_1","volume-title":"Model-checking in dense real-time. Information and computation, 104, 1","author":"Alur Rajeev","year":"1993","unstructured":"Rajeev Alur , Costas Courcoubetis , and David Dill . 1993. Model-checking in dense real-time. Information and computation, 104, 1 ( 1993 ), 2\u201334. Rajeev Alur, Costas Courcoubetis, and David Dill. 1993. Model-checking in dense real-time. Information and computation, 104, 1 (1993), 2\u201334."},{"key":"e_1_2_1_5_1","volume-title":"A theory of timed automata. Theoretical computer science, 126, 2","author":"Alur Rajeev","year":"1994","unstructured":"Rajeev Alur and David L Dill . 1994. A theory of timed automata. Theoretical computer science, 126, 2 ( 1994 ), 183\u2013235. Rajeev Alur and David L Dill. 1994. A theory of timed automata. Theoretical computer science, 126, 2 (1994), 183\u2013235."},{"key":"e_1_2_1_6_1","first-page":"18","article-title":"Using Magpie for request extraction and workload modelling","volume":"4","author":"Barham Paul","year":"2004","unstructured":"Paul Barham , Austin Donnelly , Rebecca Isaacs , and Richard Mortier . 2004 . Using Magpie for request extraction and workload modelling .. In OSDI. 4 , 18 \u2013 18 . Paul Barham, Austin Donnelly, Rebecca Isaacs, and Richard Mortier. 2004. Using Magpie for request extraction and workload modelling.. In OSDI. 4, 18\u201318.","journal-title":"OSDI."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360582"},{"key":"e_1_2_1_8_1","volume-title":"pwcet: A tool for probabilistic worst-case execution time analysis of real-time systems","author":"Bernat Guillem","unstructured":"Guillem Bernat , Antoine Colin , and Stefan Petters . 2003. pwcet: A tool for probabilistic worst-case execution time analysis of real-time systems . University of York , Department of Computer Science. Guillem Bernat, Antoine Colin, and Stefan Petters. 2003. pwcet: A tool for probabilistic worst-case execution time analysis of real-time systems. University of York, Department of Computer Science."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.75415"},{"key":"e_1_2_1_10_1","volume-title":"10th International Workshop on Worst-Case Execution Time Analysis (WCET","author":"Betts Adam","year":"2010","unstructured":"Adam Betts , Nicholas Merriam , and Guillem Bernat . 2010 . Hybrid measurement-based WCET analysis at the source level using object-level traces . In 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010). Adam Betts, Nicholas Merriam, and Guillem Bernat. 2010. Hybrid measurement-based WCET analysis at the source level using object-level traces. In 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010)."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.WCET.2013.64"},{"key":"e_1_2_1_14_1","volume-title":"13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18)","author":"Chajed Tej","year":"2018","unstructured":"Tej Chajed , Frans Kaashoek , Butler Lampson , and Nickolai Zeldovich . 2018 . Verifying concurrent software using movers in CSPEC . In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18) . USENIX Association, Carlsbad, CA. 306\u2013322. isbn:978-1-939133-08-3 https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/chajed Tej Chajed, Frans Kaashoek, Butler Lampson, and Nickolai Zeldovich. 2018. Verifying concurrent software using movers in CSPEC. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18). USENIX Association, Carlsbad, CA. 306\u2013322. isbn:978-1-939133-08-3 https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/chajed"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1807128.1807152"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/18.61109"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755952.1755967"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_22_1","volume-title":"Revisiting the Paxos algorithm","author":"Prisco Roberto De","unstructured":"Roberto De Prisco , Butler Lampson , and Nancy Lynch . 1997. Revisiting the Paxos algorithm . In Distributed Algorithms, Marios Mavronicolas and Philippas Tsigas (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 111\u2013125. isbn:978-3-540-69600-1 Roberto De Prisco, Butler Lampson, and Nancy Lynch. 1997. Revisiting the Paxos algorithm. In Distributed Algorithms, Marios Mavronicolas and Philippas Tsigas (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 111\u2013125. isbn:978-3-540-69600-1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/974044.974059"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/355604.361591"},{"key":"e_1_2_1_25_1","unstructured":"DynamoDB. 2015. https:\/\/aws.amazon.com\/message\/5467D2\/ \t\t\t\t  DynamoDB. 2015. https:\/\/aws.amazon.com\/message\/5467D2\/"},{"key":"e_1_2_1_26_1","unstructured":"Yoav Einav. 2019. Amazon Found Every 100ms of Latency cost them 1 percent in sales. https:\/\/www.gigaspaces.com\/blog\/amazon-found-every-100ms-of-latency-cost-them-1-in-sales \t\t\t\t  Yoav Einav. 2019. Amazon Found Every 100ms of Latency cost them 1 percent in sales. https:\/\/www.gigaspaces.com\/blog\/amazon-found-every-100ms-of-latency-cost-them-1-in-sales"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382553.2382555"},{"key":"e_1_2_1_28_1","volume-title":"Inferring Inductive Invariants from Phase Structures","author":"Feldman Yotam M. Y.","unstructured":"Yotam M. Y. Feldman , James R. Wilcox , Sharon Shoham , and Mooly Sagiv . 2019. Inferring Inductive Invariants from Phase Structures . In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing , Cham . 405\u2013425. Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, and Mooly Sagiv. 2019. Inferring Inductive Invariants from Phase Structures. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham. 405\u2013425."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 4th USENIX Conference on Networked Systems Design & Implementation (NSDI\u201907)","author":"Fonseca Rodrigo","year":"2007","unstructured":"Rodrigo Fonseca , George Porter , Randy H. Katz , Scott Shenker , and Ion Stoica . 2007 . X-Trace: A Pervasive Network Tracing Framework . In Proceedings of the 4th USENIX Conference on Networked Systems Design & Implementation (NSDI\u201907) . USENIX Association, USA. 20. Rodrigo Fonseca, George Porter, Randy H. Katz, Scott Shenker, and Ion Stoica. 2007. X-Trace: A Pervasive Network Tracing Framework. In Proceedings of the 4th USENIX Conference on Networked Systems Design & Implementation (NSDI\u201907). USENIX Association, USA. 20."},{"key":"e_1_2_1_30_1","volume-title":"A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification","author":"Gu\u00e9neau Arma\u00ebl","unstructured":"Arma\u00ebl Gu\u00e9neau , Arthur Chargu\u00e9raud , and Fran\u00e7ois Pottier . 2018. A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification . In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing , Cham . 533\u2013560. isbn:978-3-319-89884-1 Arma\u00ebl Gu\u00e9neau, Arthur Chargu\u00e9raud, and Fran\u00e7ois Pottier. 2018. A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham. 533\u2013560. isbn:978-3-319-89884-1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2670979.2670986"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2787496"},{"key":"e_1_2_1_33_1","first-page":"25","article-title":"Rules for Ordering Uncertain Prospects","volume":"59","author":"Hadar Josef","year":"1969","unstructured":"Josef Hadar and William R. Russell . 1969 . Rules for Ordering Uncertain Prospects . The American Economic Review , 59 , 1 (1969), 25 \u2013 34 . issn:00028282 http:\/\/www.jstor.org\/stable\/1811090 Josef Hadar and William R. Russell. 1969. Rules for Ordering Uncertain Prospects. The American Economic Review, 59, 1 (1969), 25\u201334. issn:00028282 http:\/\/www.jstor.org\/stable\/1811090","journal-title":"The American Economic Review"},{"key":"e_1_2_1_34_1","volume-title":"Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)","author":"Hance Travis","year":"2021","unstructured":"Travis Hance , Marijn Heule , Ruben Martins , and Bryan Parno . 2021 . Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21) . USENIX Association, 115\u2013131. isbn:978-1-939133-21-2 https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, 115\u2013131. isbn:978-1-939133-21-2 https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"e_1_2_1_35_1","volume-title":"9th international workshop on worst-case execution time analysis (WCET\u201909)","author":"Hansen Jeffery","year":"2009","unstructured":"Jeffery Hansen , Scott Hissam , and Gabriel A Moreno . 2009 . Statistical-based wcet estimation and validation . In 9th international workshop on worst-case execution time analysis (WCET\u201909) . Jeffery Hansen, Scott Hissam, and Gabriel A Moreno. 2009. Statistical-based wcet estimation and validation. In 9th international workshop on worst-case execution time analysis (WCET\u201909)."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3486169"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3068608"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1041"},{"key":"e_1_2_1_40_1","volume-title":"Resource Aware ML","author":"Hoffmann Jan","unstructured":"Jan Hoffmann , Klaus Aehlig , and Martin Hofmann . 2012. Resource Aware ML . In Computer Aided Verification, P. Madhusudan and Sanjit A. Seshia (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 781\u2013786. isbn:978-3-642-31424-7 Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012. Resource Aware ML. In Computer Aided Verification, P. Madhusudan and Sanjit A. Seshia (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 781\u2013786. isbn:978-3-642-31424-7"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_2_1_42_1","volume-title":"Amortized Resource Analysis with Polynomial Potential","author":"Hoffmann Jan","year":"1957","unstructured":"Jan Hoffmann and Martin Hofmann . 2010. Amortized Resource Analysis with Polynomial Potential . In Programming Languages and Systems, Andrew D. Gordon (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 287\u2013306. isbn:978-3-642-1 1957 -6 Jan Hoffmann and Martin Hofmann. 2010. Amortized Resource Analysis with Polynomial Potential. In Programming Languages and Systems, Andrew D. Gordon (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 287\u2013306. isbn:978-3-642-11957-6"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 2010 USENIX Conference on USENIX Annual Technical Conference (USENIXATC\u201910)","author":"Hunt Patrick","year":"2010","unstructured":"Patrick Hunt , Mahadev Konar , Flavio P. Junqueira , and Benjamin Reed . 2010 . ZooKeeper: Wait-Free Coordination for Internet-Scale Systems . In Proceedings of the 2010 USENIX Conference on USENIX Annual Technical Conference (USENIXATC\u201910) . USENIX Association, USA. 11. Patrick Hunt, Mahadev Konar, Flavio P. Junqueira, and Benjamin Reed. 2010. ZooKeeper: Wait-Free Coordination for Internet-Scale Systems. In Proceedings of the 2010 USENIX Conference on USENIX Annual Technical Conference (USENIXATC\u201910). USENIX Association, USA. 11."},{"key":"e_1_2_1_44_1","volume-title":"13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18)","author":"Ileri Atalay","year":"2018","unstructured":"Atalay Ileri , Tej Chajed , Adam Chlipala , Frans Kaashoek , and Nickolai Zeldovich . 2018 . Proving confidentiality in a file system using DiskSec . In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18) . USENIX Association, Carlsbad, CA. 323\u2013338. isbn:978-1-939133-08-3 https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/ileri Atalay Ileri, Tej Chajed, Adam Chlipala, Frans Kaashoek, and Nickolai Zeldovich. 2018. Proving confidentiality in a file system using DiskSec. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18). USENIX Association, Carlsbad, CA. 323\u2013338. isbn:978-1-939133-08-3 https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/ileri"},{"key":"e_1_2_1_45_1","volume-title":"Performance Interfaces for Network Functions. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Iyer Rishabh","year":"2022","unstructured":"Rishabh Iyer , Katerina Argyraki , and George Candea . 2022 . Performance Interfaces for Network Functions. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22) . USENIX Association, Renton, WA. 567\u2013584. isbn:978-1-939133-27-4 https:\/\/www.usenix.org\/conference\/nsdi22\/presentation\/iyer Rishabh Iyer, Katerina Argyraki, and George Candea. 2022. Performance Interfaces for Network Functions. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22). USENIX Association, Renton, WA. 567\u2013584. isbn:978-1-939133-27-4 https:\/\/www.usenix.org\/conference\/nsdi22\/presentation\/iyer"},{"key":"e_1_2_1_46_1","volume-title":"Performance Contracts for Software Network Functions. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 19)","author":"Iyer Rishabh","year":"2019","unstructured":"Rishabh Iyer , Luis Pedrosa , Arseniy Zaostrovnykh , Solal Pirelli , Katerina Argyraki , and George Candea . 2019 . Performance Contracts for Software Network Functions. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 19) . USENIX Association, Boston, MA. 517\u2013530. isbn:978-1-93 1971-49-2 https:\/\/www.usenix.org\/conference\/nsdi19\/presentation\/iyer Rishabh Iyer, Luis Pedrosa, Arseniy Zaostrovnykh, Solal Pirelli, Katerina Argyraki, and George Candea. 2019. Performance Contracts for Software Network Functions. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 19). USENIX Association, Boston, MA. 517\u2013530. isbn:978-1-931971-49-2 https:\/\/www.usenix.org\/conference\/nsdi19\/presentation\/iyer"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2787479"},{"key":"e_1_2_1_48_1","unstructured":"Apache Jira. 2012. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-1465 \t\t\t\t  Apache Jira. 2012. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-1465"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882297"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_1_51_1","first-page":"51","article-title":"Paxos Made Simple","volume":"32","author":"Lamport Leslie","year":"2001","unstructured":"Leslie Lamport . 2001 . Paxos Made Simple . ACM SIGACT News (Distributed Computing Column) , 32 , 4 (2001), Dec. , 51 \u2013 58 . Leslie Lamport. 2001. Paxos Made Simple. ACM SIGACT News (Distributed Computing Column), 32, 4 (2001), Dec., 51\u201358.","journal-title":"ACM SIGACT News (Distributed Computing Column)"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3267809.3267841"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1755809"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39611-3_2"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.014"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208104"},{"key":"e_1_2_1_60_1","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Mahgoub Ashraf","year":"2022","unstructured":"Ashraf Mahgoub , Edgardo Barsallo Yi , Karthick Shankar , Sameh Elnikety , Somali Chaterji , and Saurabh Bagchi . 2022 . ORION and the Three Rights: Sizing, Bundling, and Prewarming for Serverless DAGs . In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22) . USENIX Association, Carlsbad, CA. 303\u2013320. isbn:978-1-939133-28-1 https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/mahgoub Ashraf Mahgoub, Edgardo Barsallo Yi, Karthick Shankar, Sameh Elnikety, Somali Chaterji, and Saurabh Bagchi. 2022. ORION and the Three Rights: Sizing, Bundling, and Prewarming for Serverless DAGs. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA. 303\u2013320. isbn:978-1-939133-28-1 https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/mahgoub"},{"key":"e_1_2_1_61_1","volume-title":"A Coq Library for Internal Verification of Running-Times","author":"McCarthy Jay","unstructured":"Jay McCarthy , Burke Fetscher , Max New , Daniel Feltey , and Robert Bruce Findler . 2016. A Coq Library for Internal Verification of Running-Times . In Functional and Logic Programming, Oleg Kiselyov and Andy King (Eds.). Springer International Publishing , Cham . 144\u2013162. isbn:978-3-319-29604-3 Jay McCarthy, Burke Fetscher, Max New, Daniel Feltey, and Robert Bruce Findler. 2016. A Coq Library for Internal Verification of Running-Times. In Functional and Logic Programming, Oleg Kiselyov and Andy King (Eds.). Springer International Publishing, Cham. 144\u2013162. isbn:978-3-319-29604-3"},{"key":"e_1_2_1_62_1","unstructured":"Stefan K Muller and Jan Hoffmann. 2019. Combining Source and Target Level Cost Analyses for OCaml Programs. \t\t\t\t  Stefan K Muller and Jan Hoffmann. 2019. Combining Source and Target Level Cost Analyses for OCaml Programs."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_2_1_65_1","volume-title":"Real-Time: Theory in Practice","author":"Nicollin Xavier","unstructured":"Xavier Nicollin and Joseph Sifakis . 1992. An overview and synthesis on timed process algebras . In Real-Time: Theory in Practice , J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg (Eds.). Springer Berlin Heidelberg, Berlin , Heidelberg . 526\u2013548. isbn:978-3-540-47218-6 Xavier Nicollin and Joseph Sifakis. 1992. An overview and synthesis on timed process algebras. In Real-Time: Theory in Practice, J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 526\u2013548. isbn:978-3-540-47218-6"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_1_67_1","volume-title":"Execution-time profiles. Technical report","author":"Petters Stefan M","unstructured":"Stefan M Petters . 2007. Execution-time profiles. Technical report , NICTA , Sydney, Australia . Stefan M Petters. 2007. Execution-time profiles. Technical report, NICTA, Sydney, Australia."},{"key":"e_1_2_1_68_1","volume-title":"7th International Workshop on Worst-Case Execution Time Analysis (WCET\u201907)","author":"Petters Stefan M","year":"2007","unstructured":"Stefan M Petters , Patryk Zadarnowski , and Gernot Heiser . 2007 . Measurements or static analysis or both? In 7th International Workshop on Worst-Case Execution Time Analysis (WCET\u201907) . Stefan M Petters, Patryk Zadarnowski, and Gernot Heiser. 2007. Measurements or static analysis or both? In 7th International Workshop on Worst-Case Execution Time Analysis (WCET\u201907)."},{"key":"e_1_2_1_69_1","volume-title":"Analysis of asynchronous concurrent systems by timed Petri nets.. Ph. D. Dissertation","author":"Ramchandani Chander","unstructured":"Chander Ramchandani . 1973. Analysis of asynchronous concurrent systems by timed Petri nets.. Ph. D. Dissertation . Massachusetts Institute of Technology . Chander Ramchandani. 1973. Analysis of asynchronous concurrent systems by timed Petri nets.. Ph. D. Dissertation. Massachusetts Institute of Technology."},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1555815.1555800"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.803382"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-017-9286-3"},{"key":"e_1_2_1_73_1","volume-title":"Mike Burrows, Pat Stephenson, Manoj Plakal, Donald Beaver, Saul Jaspan, and Chandan Shanbhag.","author":"Sigelman Benjamin H","year":"2010","unstructured":"Benjamin H Sigelman , Luiz Andre Barroso , Mike Burrows, Pat Stephenson, Manoj Plakal, Donald Beaver, Saul Jaspan, and Chandan Shanbhag. 2010 . Dapper , a large-scale distributed systems tracing infrastructure. Benjamin H Sigelman, Luiz Andre Barroso, Mike Burrows, Pat Stephenson, Manoj Plakal, Donald Beaver, Saul Jaspan, and Chandan Shanbhag. 2010. Dapper, a large-scale distributed systems tracing infrastructure."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213836.2213945"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.842141"},{"key":"e_1_2_1_76_1","volume-title":"Towards Pre-Deployment Detection of Performance Failures in Cloud Distributed Systems. In 7th USENIX Workshop on Hot Topics in Cloud Computing (HotCloud 15)","author":"Suminto Riza O.","unstructured":"Riza O. Suminto , Agung Laksono , Anang D. Satria , Thanh Do , and Haryadi S. Gunawi . 2015 . Towards Pre-Deployment Detection of Performance Failures in Cloud Distributed Systems. In 7th USENIX Workshop on Hot Topics in Cloud Computing (HotCloud 15) . USENIX Association, Santa Clara, CA. https:\/\/www.usenix.org\/conference\/hotcloud15\/workshop-program\/presentation\/suminto Riza O. Suminto, Agung Laksono, Anang D. Satria, Thanh Do, and Haryadi S. Gunawi. 2015. Towards Pre-Deployment Detection of Performance Failures in Cloud Distributed Systems. In 7th USENIX Workshop on Hot Topics in Cloud Computing (HotCloud 15). USENIX Association, Santa Clara, CA. https:\/\/www.usenix.org\/conference\/hotcloud15\/workshop-program\/presentation\/suminto"},{"key":"e_1_2_1_77_1","volume-title":"Distributed Network Monitoring and Debugging with SwitchPointer. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18)","author":"Tammana Praveen","year":"2018","unstructured":"Praveen Tammana , Rachit Agarwal , and Myungjin Lee . 2018 . Distributed Network Monitoring and Debugging with SwitchPointer. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18) . USENIX Association, Renton, WA. 453\u2013456. isbn:978-1-939133-01-4 https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/tammana Praveen Tammana, Rachit Agarwal, and Myungjin Lee. 2018. Distributed Network Monitoring and Debugging with SwitchPointer. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). USENIX Association, Renton, WA. 453\u2013456. isbn:978-1-939133-01-4 https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/tammana"},{"key":"e_1_2_1_78_1","unstructured":"J.J. Vereijken. 1994. Fischer\u2019s protocol in timed process algebra. Technische Universiteit Eindhoven. \t\t\t\t  J.J. Vereijken. 1994. Fischer\u2019s protocol in timed process algebra. Technische Universiteit Eindhoven."},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3267809.3267839"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_1_81_1","volume-title":"Zeno: Diagnosing Performance Problems with Temporal Provenance. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 19)","author":"Wu Yang","year":"2019","unstructured":"Yang Wu , Ang Chen , and Linh Thi Xuan Phan . 2019 . Zeno: Diagnosing Performance Problems with Temporal Provenance. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 19) . USENIX Association, Boston, MA. 395\u2013420. isbn:978-1-93 1971-49-2 https:\/\/www.usenix.org\/conference\/nsdi19\/presentation\/wu Yang Wu, Ang Chen, and Linh Thi Xuan Phan. 2019. Zeno: Diagnosing Performance Problems with Temporal Provenance. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 19). USENIX Association, Boston, MA. 395\u2013420. isbn:978-1-931971-49-2 https:\/\/www.usenix.org\/conference\/nsdi19\/presentation\/wu"},{"key":"e_1_2_1_82_1","volume-title":"Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Yao Jianan","year":"2022","unstructured":"Jianan Yao , Runzhou Tao , Ronghui Gu , and Jason Nieh . 2022 . DuoAI: Fast , Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22) . USENIX Association, Carlsbad, CA. 485\u2013501. isbn:978-1-939133-28-1 https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/yao Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. 2022. DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA. 485\u2013501. isbn:978-1-939133-28-1 https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/yao"},{"key":"e_1_2_1_83_1","volume-title":"DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao , Runzhou Tao , Ronghui Gu , Jason Nieh , Suman Jana , and Gabriel Ryan . 2021 . DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21) . USENIX Association, 405\u2013421. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 405\u2013421. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao"},{"key":"e_1_2_1_84_1","volume-title":"Automatic verification of real-time communicating systems by constraint-solving","author":"Yi Wang","unstructured":"Wang Yi , Paul Pettersson , and Mats Daniels . 1995. Automatic verification of real-time communicating systems by constraint-solving . In Formal Description Techniques VII. Springer , 243\u2013258. Wang Yi, Paul Pettersson, and Mats Daniels. 1995. Automatic verification of real-time communicating systems by constraint-solving. In Formal Description Techniques VII. Springer, 243\u2013258."},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544271"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/2987550.2987585"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127479.3132245"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591235","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591235","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:46Z","timestamp":1750178866000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591235"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":87,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591235"],"URL":"https:\/\/doi.org\/10.1145\/3591235","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}