{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T00:29:36Z","timestamp":1790641776198,"version":"4.1.0"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"name":"CRII: SHF: Certified Byzantine Fault-tolerant Systems","award":["1657204"],"award-info":[{"award-number":["1657204"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>Distributed system replication is widely used as a means of fault-tolerance and scalability. However, it provides a spectrum of consistency choices that impose a dilemma for clients between correctness, responsiveness and availability. Given a sequential object and its integrity properties, we automatically synthesize a replicated object that guarantees state integrity and convergence and avoids unnecessary coordination. Our approach is based on a novel sufficient condition for integrity and convergence called well-coordination that requires certain orders between conflicting and dependent operations. We statically analyze the given sequential object to decide its conflicting and dependent methods and use this information to avoid coordination. We present novel coordination protocols that are parametric in terms of the analysis results and provide the well-coordination requirements. We implemented a tool called Hamsaz that can automatically analyze the given object, instantiate the protocols and synthesize replicated objects. We have applied Hamsaz to a suite of use-cases and synthesized replicated objects that are significantly more responsive than the strongly consistent baseline.<\/jats:p>","DOI":"10.1145\/3290387","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T08:33:51Z","timestamp":1546590831000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["Hamsaz: replication coordination analysis and synthesis"],"prefix":"10.1145","volume":"3","author":[{"given":"Farzin","family":"Houshmand","sequence":"first","affiliation":[{"name":"University of California at Riverside, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohsen","family":"Lesani","sequence":"additional","affiliation":[{"name":"University of California at Riverside, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2012.33"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110214"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542488"},{"key":"e_1_2_2_5_1","unstructured":"Appendix. 2018. Appendix. https:\/\/www.cs.ucr.edu\/~lesani\/companion\/popl19\/Appendix.pdf . (2018).  Appendix. 2018. Appendix. https:\/\/www.cs.ucr.edu\/~lesani\/companion\/popl19\/Appendix.pdf . (2018)."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.14778\/2735508.2735509"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2723372.2737784"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2391229.2391251"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.14778\/2212351.2212359"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741972"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2723872.2723889"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_7"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories","author":"Barrett Clark","year":"2010"},{"key":"e_1_2_2_15_1","volume-title":"PRACTI Replication. In Proc. NSDI.","author":"Belaramani Nalini","year":"2006"},{"key":"e_1_2_2_16_1","volume-title":"LIPIcs-Leibniz International Proceedings in Informatics","volume":"59","author":"Bernardi Giovanni","year":"2016"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/323647.323636"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535877"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/362342.362367"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009895"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_2_2_22_1","volume-title":"Introduction to Reliable and Secure Distributed Programming","author":"Cachin Christian","edition":"2"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","volume-title":"Set theory for computing: from decision procedures to declarative programming with sets","author":"Cantone Domenico","DOI":"10.1007\/978-1-4757-3452-2"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/647938.741244"},{"key":"e_1_2_2_25_1","unstructured":"Nuno Carvalho and et. al. 2011. APPIA Framework. http:\/\/appia.di.fc.ul.pt\/wiki\/index.php?title=Main_Page . (2011). Accessed: 2018-06-23.  Nuno Carvalho and et. al. 2011. APPIA Framework. http:\/\/appia.di.fc.ul.pt\/wiki\/index.php?title=Main_Page . (2011). Accessed: 2018-06-23."},{"key":"e_1_2_2_26_1","volume-title":"LIPIcs-Leibniz International Proceedings in Informatics","volume":"42","author":"Cerone Andrea","year":"2015"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3166089.3166090"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.14778\/1454159.1454167"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294281"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_26"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065167.1065193"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1071610.1071615"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/564585.564601"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2011.389"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_2_37_1","unstructured":"Rachid Guerraoui Matej Pavlovic and Dragos-Adrian Seredinschi. 2016. Incremental Consistency Guarantees for Replicated Objects.. In OSDI. 169\u2013184.   Rachid Guerraoui Matej Pavlovic and Dragos-Adrian Seredinschi. 2016. Incremental Consistency Guarantees for Replicated Objects.. In OSDI. 169\u2013184."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.18"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2987550.2987559"},{"key":"e_1_2_2_40_1","volume-title":"NetChain: Scale-Free Sub-RT T Coordination. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18)","author":"Jin Xin","year":"2018"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158115"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.14778\/1687627.1687657"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_15"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/138873.138877"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/2643634.2643664"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2745947.2745955"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/2387880.2387906"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_2_53_1","volume-title":"Proceedings of the 11th USENIX Conference on Networked Systems Design and Implementation (NSDI\u201914)","author":"Liu Jed"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043593"},{"key":"e_1_2_2_55_1","volume-title":"Andersen","author":"Lloyd Wyatt","year":"2013"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2004.34"},{"key":"e_1_2_2_57_1","doi-asserted-by":"crossref","unstructured":"P. Madhusudan and P.S. Thiagarajan. 2001. Distributed Controller Synthesis for Local Specifications. In Automata Languages and Programming Fernando Orejas Paul G. Spirakis and Jan van Leeuwen (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 396\u2013407.   P. Madhusudan and P.S. Thiagarajan. 2001. Distributed Controller Synthesis for Local Specifications. In Automata Languages and Programming Fernando Orejas Paul G. Spirakis and Jan van Leeuwen (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 396\u2013407.","DOI":"10.1007\/3-540-48224-5_33"},{"key":"e_1_2_2_58_1","volume-title":"Relational Constraint Solving in SMT. In International Conference on Automated Deduction. Springer, 148\u2013165","author":"Meng Baoluo","year":"2017"},{"key":"e_1_2_2_59_1","doi-asserted-by":"crossref","unstructured":"Matthew Milano and Andrew C Myers. 2018. MixT: A Language for Mixing Consistency in Geodistributed Transactions. (2018).  Matthew Milano and Andrew C Myers. 2018. MixT: A Language for Mixing Consistency in Geodistributed Transactions. (2018).","DOI":"10.1145\/3192366.3192375"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2911151.2911160"},{"key":"e_1_2_2_61_1","volume-title":"Exploiting Concurrency Efficiently and Correctly Workshop.","author":"Nardelli Francesco Zappa","year":"2009"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/62546.62549"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/2643634.2643666"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/268998.266711"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.476504"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2723372.2723720"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737981"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043592"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946312"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522731"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1137\/0206036"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/1466443.1466448"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.5555\/1251229.1251250"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290387","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290387","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:58:04Z","timestamp":1750193884000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290387"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":75,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290387"],"URL":"https:\/\/doi.org\/10.1145\/3290387","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}