{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T10:39:39Z","timestamp":1790937579080,"version":"4.1.0"},"reference-count":79,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"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":[[2018,10,24]]},"abstract":"<jats:p>A real-world distributed system is rarely implemented as a standalone monolithic system. Instead, it is composed of multiple independent interacting components that together ensure the desired system-level specification. One can scale systematic testing to large, industrial-scale implementations by decomposing the system-level testing problem into a collection of simpler component-level testing problems.<\/jats:p>\n                  <jats:p>This paper proposes techniques for compositional programming and testing of distributed systems with two central contributions: (1) We propose a module system based on the theory of compositional trace refinement for dynamic systems consisting of asynchronously-communicating state machines, where state machines can be dynamically created, and communication topology of the existing state machines can change at runtime; (2) We present ModP, a programming system that implements our module system to enable compositional reasoning (assume-guarantee) of distributed systems.<\/jats:p>\n                  <jats:p>We demonstrate the efficacy of our framework by building two practical fault-tolerant distributed systems, a transaction-commit service and a replicated hash-table. ModP helps implement these systems modularly and validate them via compositional testing. We empirically demonstrate that the abstraction-based compositional reasoning approach helps amplify the coverage during testing and scale it to real-world distributed systems. The distributed services built using ModP achieve performance comparable to open-source equivalents.<\/jats:p>","DOI":"10.1145\/3276529","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T07:57:18Z","timestamp":1540367838000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Compositional programming and testing of dynamic distributed systems"],"prefix":"10.1145","volume":"2","author":[{"given":"Ankush","family":"Desai","sequence":"first","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amar","family":"Phanishayee","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/7929"},{"key":"e_1_2_2_3_1","unstructured":"Akka. 2017. Akka Programming Language. http:\/\/akka.io\/ . (2017). Akka. 2017. Akka Programming Language. http:\/\/akka.io\/ . (2017)."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"e_1_2_2_5_1","volume-title":"10th International Conference, CAV \u201998, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings. 521\u2013525","author":"Alur Rajeev","year":"1998"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000031"},{"key":"e_1_2_2_7_1","volume-title":"Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf.","author":"Armstrong Joe","year":"2007"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411273.1411275"},{"key":"e_1_2_2_9_1","volume-title":"CONCUR","author":"Attie C.","year":"2001"},{"key":"e_1_2_2_10_1","unstructured":"Philip A Bernstein Vassos Hadzilacos and Nathan Goodman. 1986. Concurrency Control and Recovery in Database Systems. Addison-Wesley Longman Publishing Co. Inc. Boston MA USA. Philip A Bernstein Vassos Hadzilacos and Nathan Goodman. 1986. Concurrency Control and Recovery in Database Systems. Addison-Wesley Longman Publishing Co. Inc. Boston MA USA."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1118537.1123060"},{"key":"e_1_2_2_12_1","unstructured":"Edwin Brady. 2016. State Machines All The Way Down An Architecture for Dependently Typed Applications. (2016). Edwin Brady. 2016. State Machines All The Way Down An Architecture for Dependently Typed Applications. (2016)."},{"key":"e_1_2_2_13_1","volume-title":"Orleans: A Framework for Cloud Computing. Technical Report.","author":"Bykov Sergey","year":"2010"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599437"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.798322"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281103"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.9"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"Ankush Desai Tommaso Dreossi and Sanjit A. Seshia. 2017a. Combining Model Checking and Runtime Verification for Safe Robotics. Ankush Desai Tommaso Dreossi and Sanjit A. Seshia. 2017a. Combining Model Checking and Runtime Verification for Safe Robotics.","DOI":"10.1007\/978-3-319-67531-2_11"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462184"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786861"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3055004.3055022"},{"key":"e_1_2_2_24_1","volume-title":"International Workshop on Web Services and Formal Methods. Springer, 1\u201328","author":"Dezani-Ciancaglini Mariangiola","year":"2009"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762193"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Jasmin Fisher Thomas A. Henzinger Dejan Nickovic Nir Piterman Anmol V. Singh and Moshe Y. Vardi. 2011. Dynamic Reactive Modules. Jasmin Fisher Thomas A. Henzinger Dejan Nickovic Nir Piterman Anmol V. Singh and Moshe Y. Vardi. 2011. Dynamic Reactive Modules.","DOI":"10.1007\/978-3-642-23217-6_27"},{"key":"e_1_2_2_27_1","volume-title":"Program Verification","author":"Floyd Robert W"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237805"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/646731.703841"},{"key":"e_1_2_2_30_1","volume-title":"LIPIcs-Leibniz International Proceedings in Informatics","volume":"42","author":"Gavran Ivan","year":"2015"},{"key":"e_1_2_2_31_1","volume-title":"Operating Systems, An Advanced Course.","author":"Gray Jim"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132863.1132867"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043582"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_36_1","volume-title":"Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI).","author":"Hawblitzel Chris","year":"2014"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3089"},{"key":"e_1_2_2_38_1","volume-title":"Proceedings of the 1999 IEEE\/ACM International Conference on Computer-aided Design.","author":"Henzinger Thomas A."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_2_42_1","volume-title":"Verification and Validation (ICST), 2016 IEEE International Conference on. IEEE, 135\u2013145","author":"Hughes John","year":"2016"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250755"},{"key":"e_1_2_2_44_1","volume-title":"Symposium on Networked Systems Design and Implementation.","author":"Killian Charles Edwin","year":"2007"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_2_47_1","first-page":"4","article-title":"Paxos Made Simple","volume":"32","author":"Lamport Leslie","year":"2001","journal-title":"ACM SIGACT News"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.88"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398857.2384645"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2844108"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/3077629.3077651"},{"key":"e_1_2_2_54_1","doi-asserted-by":"crossref","unstructured":"Kenneth Lauchlin McMillan. 1992. Symbolic Model Checking: An Approach to the State Explosion Problem. Ph.D. Dissertation. Pittsburgh PA USA. Kenneth Lauchlin McMillan. 1992. Symbolic Model Checking: An Approach to the State Explosion Problem. Ph.D. Dissertation. Pittsburgh PA USA.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00030-1"},{"key":"e_1_2_2_56_1","unstructured":"Kenneth Lauchlin McMillan. 2017. SMV Model Checker. http:\/\/www.kenmcmil.com\/smv.html . (2017). Kenneth Lauchlin McMillan. 2017. SMV Model Checker. http:\/\/www.kenmcmil.com\/smv.html . (2017)."},{"key":"e_1_2_2_57_1","unstructured":"R. Milner. 1982. A Calculus of Communicating Systems. Springer-Verlag New York Inc. Secaucus NJ USA. R. Milner. 1982. A Calculus of Communicating Systems. Springer-Verlag New York Inc. Secaucus NJ USA."},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_2_59_1","unstructured":"Iulian Moraru David G Andersen and Michael Kaminsky. 2013a. EPaxos Code. https:\/\/github.com\/efficient\/epaxos\/ . (2013). Iulian Moraru David G Andersen and Michael Kaminsky. 2013a. EPaxos Code. https:\/\/github.com\/efficient\/epaxos\/ . (2013)."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2517350"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_62_1","unstructured":"P-GitHub. 2018. The P Programming Langugage. https:\/\/github.com\/p- org\/P . (2018). P-GitHub. 2018. The P Programming Langugage. https:\/\/github.com\/p- org\/P . (2018)."},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_2_64_1","doi-asserted-by":"crossref","unstructured":"Benjamin Pierce and Davide Sangiorgi. 1996. Typing and Subtyping for Mobile Processes. In Mathematical Strustures In Computer Science. 376\u2013385. Benjamin Pierce and Davide Sangiorgi. 1996. Typing and Subtyping for Mobile Processes. In Mathematical Strustures In Computer Science. 376\u2013385.","DOI":"10.1109\/LICS.1993.287570"},{"key":"e_1_2_2_65_1","doi-asserted-by":"crossref","unstructured":"Benjamin C. Pierce and David N. Turner. 2000. Proof Language and Interaction. Chapter Pict: A Programming Language Based on the Pi-Calculus. Benjamin C. Pierce and David N. Turner. 2000. Proof Language and Interaction. Chapter Pict: A Programming Language Based on the Pi-Calculus.","DOI":"10.7551\/mitpress\/5641.003.0022"},{"key":"e_1_2_2_66_1","unstructured":"Pony. 2017. Pony Programming Langugage. https:\/\/www.ponylang.org . (2017). Pony. 2017. Pony Programming Langugage. https:\/\/www.ponylang.org . (2017)."},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268978"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693017_25"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786830"},{"key":"e_1_2_2_71_1","volume-title":"Programming and Proving with Distributed Protocols. In 45th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201918)","author":"Sergey Ilya","year":"2018"},{"key":"e_1_2_2_72_1","volume-title":"Actor Services. In Proceedings of the 25th European Symposium on Programming Languages and Systems -","volume":"9632","author":"Alexander"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392200.2392220"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2673577"},{"key":"e_1_2_2_75_1","volume-title":"Proc. 6th USENIX OSDI","author":"van Renesse Robbert"},{"key":"e_1_2_2_76_1","volume-title":"Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI).","author":"Wang Xi","year":"2014"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211617"},{"key":"e_1_2_2_79_1","volume-title":"Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI).","author":"Yang Junfeng","year":"2009"},{"key":"e_1_2_2_80_1","unstructured":"Jianqiao Yang Ankush Desai and Koushik Sen. 2017. Multi-Path Symbolic Execution for P Language. https:\/\/github.com\/ thisiscam\/MultiPathP . (2017). Jianqiao Yang Ankush Desai and Koushik Sen. 2017. Multi-Path Symbolic Execution for P Language. https:\/\/github.com\/ thisiscam\/MultiPathP . (2017)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276529","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276529","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T21:28:36Z","timestamp":1775251716000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276529"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":79,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276529"],"URL":"https:\/\/doi.org\/10.1145\/3276529","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}