{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T02:41:06Z","timestamp":1761964866596,"version":"3.41.0"},"reference-count":86,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,5,26]],"date-time":"2017-05-26T00:00:00Z","timestamp":1495756800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1414078, CCF-1248184, CCF-0964196, CNS-0831298, and CCF-0613913"],"award-info":[{"award-number":["CCF-1414078, CCF-1248184, CCF-0964196, CNS-0831298, and CCF-0613913"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006146","name":"Office of Naval Reactors","doi-asserted-by":"publisher","award":["N000141512208, N000140910651, and N000140710928"],"award-info":[{"award-number":["N000141512208, N000140910651, and N000140710928"]}],"id":[{"id":"10.13039\/100006146","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2017,9,30]]},"abstract":"<jats:p>This article describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows in which complex synchronization conditions can be expressed using high-level queries, especially logic quantifications, over message history sequences. Unfortunately, the programs would be extremely inefficient, including consuming unbounded memory, if executed straightforwardly.<\/jats:p>\n          <jats:p>We present new optimizations that automatically transform complex synchronization conditions into incremental updates of necessary auxiliary values as messages are sent and received. The core of the optimizations is the first general method for efficient implementation of logic quantifications. We have developed an operational semantics of the language, implemented a prototype of the compiler and the optimizations, and successfully used the language and implementation on a variety of important distributed algorithms.<\/jats:p>","DOI":"10.1145\/2994595","type":"journal-article","created":{"date-parts":[[2017,5,31]],"date-time":"2017-05-31T19:32:40Z","timestamp":1496259160000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["From Clarity to Efficiency for Distributed Algorithms"],"prefix":"10.1145","volume":"39","author":[{"given":"Yanhong A.","family":"Liu","sequence":"first","affiliation":[{"name":"Stony Brook University, NY, USA"}]},{"given":"Scott D.","family":"Stoller","sequence":"additional","affiliation":[{"name":"Stony Brook University, NY, USA"}]},{"given":"Bo","family":"Lin","sequence":"additional","affiliation":[{"name":"Stony Brook University, NY, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,5,26]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1186632.1186634"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/7929"},{"volume-title":"Reduction of operator strength","author":"Allen Frances E.","key":"e_1_2_1_3_1","unstructured":"Frances E. Allen, John Cocke, and Ken Kennedy. 1981. Reduction of operator strength. In Program Flow Analysis, Steven S. Muchnick and Neil D. Jones (Eds.). Prentice-Hall, Upper Saddle River, NJ. 79--101."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1713254.1713261"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/135321"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02846-5_24"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/983102"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1267074.1267082"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.12.007"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87877-3_54"},{"key":"e_1_2_1_11_1","volume-title":"Dirk Van Gucht, and Marc Gyssens","author":"Badia Antonio","year":"1995","unstructured":"Antonio Badia, Dirk Van Gucht, and Marc Gyssens. 1995. Query languages with generalized quantifiers. In Applications of Logic in Databases, R. Ramakrishnan (Ed.). Kluwer Academic, Dordrecht, The Netherlands."},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the Conference on Innovative Database Research. 223--234","author":"Baker Jason","year":"2011","unstructured":"Jason Baker, Chris Bond, James C. Corbett, J. J. Furman, Andrey Khorlin, James Larson, Jean-Michel L\u00e9on, Yawei Li, Alexander Lloyd, and Vadim Yushprakh. 2011. Megastore: Providing scalable, highly available storage for interactive services. In Proceedings of the Conference on Innovative Database Research. 223--234."},{"key":"e_1_2_1_13_1","volume-title":"Bloom Programming Language. Retrieved","author":"Berkeley Orders","year":"2017","unstructured":"Berkeley Orders of Magnitude 2013. Bloom Programming Language. Retrieved April 8, 2017 from http:\/\/www.bloom-lang.net."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02414-6_9"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1238844.1238855"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1298455.1298487"},{"volume-title":"Constructing Programs from Specifications","author":"Cai Jiazhen","key":"e_1_2_1_17_1","unstructured":"Jiazhen Cai, Philippe Facon, Fritz Henglein, Robert Paige, and Edmond Schonberg. 1991. Type analysis and data structure selection. In Constructing Programs from Specifications, Bernhard M\u00f6ller (Ed.). North-Holland, Amsterdam, The Netherlands, 126--164."},{"key":"e_1_2_1_18_1","volume-title":"Stoller","author":"Chand Saksham","year":"2016","unstructured":"Saksham Chand, Yanhong A. Liu, and Scott D. Stoller. 2016. Formal verification of multi-Paxos for distributed consensus. In Proceedings of the 21st International Symposium on Formal Methods. Springer, 119--136."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1365815.1365816"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/645923.673649"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1614191"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068414000167"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1327452.1327492"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1323293.1294281"},{"volume-title":"DistAlgo: A Language for Distributed Algorithms. Retrieved","year":"2017","key":"e_1_2_1_25_1","unstructured":"DistAlgo. 2016. DistAlgo: A Language for Distributed Algorithms. Retrieved April 8, 2017 from http:\/\/github.com\/DistAlgo."},{"volume-title":"Erlang Programming Language. Retrieved","year":"2017","key":"e_1_2_1_26_1","unstructured":"Erlang. 2015. Erlang Programming Language. Retrieved April 8, 2017 from http:\/\/www.erlang.org\/."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 11th Australian Computer Science Conference. 56--66","author":"Fidge Colin J.","year":"1988","unstructured":"Colin J. Fidge. 1988. Timestamps in message-passing systems that preserve the partial ordering. In Proceedings of the 11th Australian Computer Science Conference. 56--66."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.3233\/IA-2011-0014"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/513752"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111041"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220882.3220988"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1165389.945450"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869631.1869635"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1759148.1759160"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/170035.170066"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(03)00074-8"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855840.1855851"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/3019255"},{"volume-title":"An experiment in compiler design for a concurrent object-based programming language. Master\u2019s thesis","author":"Kr\u00fcger Ingolf Heiko","key":"e_1_2_1_40_1","unstructured":"Ingolf Heiko Kr\u00fcger. 1996. An experiment in compiler design for a concurrent object-based programming language. Master\u2019s thesis. The University of Texas at Austin, Austin, TX."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/1374804"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1773912.1773922"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/579617"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03466-4_2"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1467247.1467263"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/42392.42399"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/2500946"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968610"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1621607.1621617"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023068020483"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1552309.1552311"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094848"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053471"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33536-5_11"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384645"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111562"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000360"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.5555\/525656"},{"key":"e_1_2_1_60_1","volume-title":"Proceedings of the International Workshop on Parallel and Distributed Algorithms. North-Holland","author":"Mattern Friedemann","year":"1989","unstructured":"Friedemann Mattern. 1989. Virtual time and global states of distributed systems. In Proceedings of the International Workshop on Parallel and Distributed Algorithms. North-Holland, Amsterdam, The Netherlands, 120--131."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/646334.687801"},{"key":"e_1_2_1_62_1","volume-title":"Message Passing Interface Forum. Retrieved","author":"MPI.","year":"2017","unstructured":"MPI. 2015. Message Passing Interface Forum. Retrieved April 8, 2017 from http:\/\/www.mpi-forum.org\/."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/504282.504294"},{"key":"e_1_2_1_64_1","volume-title":"Proceedings of the International Conference on Computing and Information. Canadian Scholars Press","author":"Paige Robert","year":"1989","unstructured":"Robert Paige. 1989. Real-time simulation of a set machine on a RAM. In Proceedings of the International Conference on Computing and Information. Canadian Scholars Press, Toronto, ON, 69--73."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357177"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/646398.691304"},{"key":"e_1_2_1_67_1","unstructured":"PRL Project. 2013. EventML. Retrieved April 8 2017 from http:\/\/www.nuprl.org\/software\/#WhatisEventML."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75305"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158710"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/49077"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855117"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/2517679"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449913.1449923"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.5555\/646591.697650"},{"volume-title":"Proceedings of the 19th International Conference on Logic Programming. Springer, 392--406","author":"Saha Diptikalyan","key":"e_1_2_1_75_1","unstructured":"Diptikalyan Saha and C. R. Ramakrishnan. 2003. Incremental evaluation of tabled logic programs. In Proceedings of the 19th International Conference on Logic Programming. Springer, 392--406."},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(91)90008-W"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.03.026"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSST.2010.5496972"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2002.808407"},{"key":"e_1_2_1_80_1","volume-title":"The XSB System Version 3.7,x. Retrieved","author":"Swift Theresa","year":"2017","unstructured":"Theresa Swift, David S. Warren, and others. 2016. The XSB System Version 3.7,x. Retrieved April 8, 2017 from http:\/\/xsb.sourceforge.net."},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.5555\/517021"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","unstructured":"Robbert van Renesse and Deniz Altinbuken. 2015. Paxos made moderately complex. Computer Surveys 47 3 42:1--42:36. 10.1145\/2673577","DOI":"10.1145\/2673577"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.5555\/1251254.1251261"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/602259.602281"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2002.1848"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2003.818784"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2994595","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2994595","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2994595","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:39:48Z","timestamp":1750217988000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2994595"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,26]]},"references-count":86,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,9,30]]}},"alternative-id":["10.1145\/2994595"],"URL":"https:\/\/doi.org\/10.1145\/2994595","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2017,5,26]]},"assertion":[{"value":"2015-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-05-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}