{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:32Z","timestamp":1750221272872,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,1,11]],"date-time":"2018-01-11T00:00:00Z","timestamp":1515628800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2018,1,11]]},"abstract":"<jats:p>Modern geo-replicated data stores provide high availability by relaxing the underlying consistency requirements. Programs layered over such data stores are called weakly consistent programs. Due to the reduced consistency requirements, they exhibit highly nondeterministic behaviors, some of which might violate program invariants. Therefore, implementing correct weakly consistent programs and reasoning about them is challenging. In this paper, we present a systematic scheduling approach that is aware of the underlying consistency model. Our approach dynamically explores all possible program behaviors allowed by the used data store consistency model, and it evaluates program invariants during the exploration. We implement the approach in a prototype model checker for Antidote, which is a causally consistent key-value data store with convergent con ict handling. We evaluate our tool on several benchmarks. The results show that our approach is e effective in detecting buggy behaviors in weakly consistent programs.<\/jats:p>","DOI":"10.1145\/3149485.3149493","type":"journal-article","created":{"date-parts":[[2018,1,12]],"date-time":"2018-01-12T13:49:50Z","timestamp":1515764990000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Consistency-Aware Scheduling for Weakly Consistent Programs"],"prefix":"10.1145","volume":"42","author":[{"given":"Maryam","family":"Dabaghchian","sequence":"first","affiliation":[{"name":"University of Utah Salt Lake City, UT, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zvonimir","family":"Rakamaric","sequence":"additional","affiliation":[{"name":"University of Utah Salt Lake City, UT, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Burcu K.","family":"Ozkan","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erdal","family":"Mutlu","sequence":"additional","affiliation":[{"name":"Ko\u00e7 University Istanbul, Turkey"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[{"name":"Ko\u00e7 University Istanbul, Turkey"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,1,11]]},"reference":[{"volume-title":"Causal memory: De nitions, implementation, and programming. Distributed Computing, 9(1)","year":"1995","author":"Ahamad M.","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2016.98"},{"key":"e_1_2_1_3_1","unstructured":"Antidote Reference Platform. http:\/\/github.com\/SyncFree\/antidote.  Antidote Reference Platform. http:\/\/github.com\/SyncFree\/antidote."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741972"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2596631.2596632"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009895"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","DOI":"10.1561\/9781601988591","volume-title":"Principles of Eventual Consistency","author":"Burckhardt S.","year":"2014"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"volume-title":"CONCUR","year":"2015","author":"Cerone A.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","unstructured":"Commander. http:\/\/github.com\/Maryam81609\/commander.  Commander. http:\/\/github.com\/Maryam81609\/commander."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294281"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926432"},{"volume-title":"Timestamps in message-passing systems that preserve the partial ordering","year":"1987","author":"Fidge C. J.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/564585.564601"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3102980.3102994"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043593"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2911151.2911160"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_1_23_1","unstructured":"Riak - A Key-Value Store. http:\/\/basho.com\/products\/riak-overview.  Riak - A Key-Value Store. http:\/\/basho.com\/products\/riak-overview."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2050613.2050642"},{"key":"e_1_2_1_25_1","unstructured":"SyncFree Project. https:\/\/syncfree.lip6.fr.  SyncFree Project. https:\/\/syncfree.lip6.fr."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224070"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064889.3064893"},{"volume-title":"SEFM","year":"2016","author":"Zeller P.","key":"e_1_2_1_28_1"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3149485.3149493","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3149485.3149493","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:07Z","timestamp":1750212667000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3149485.3149493"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,11]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,1,11]]}},"alternative-id":["10.1145\/3149485.3149493"],"URL":"https:\/\/doi.org\/10.1145\/3149485.3149493","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2018,1,11]]},"assertion":[{"value":"2018-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}