{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,28]],"date-time":"2025-07-28T06:24:22Z","timestamp":1753683862802,"version":"3.40.3"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720186"},{"type":"electronic","value":"9783030720193"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Concurrent accesses to databases are typically encapsulated in transactions in order to enable isolation from other concurrent computations and resilience to failures. Modern databases provide transactions with various semantics corresponding to different trade-offs between consistency and availability. Since a weaker consistency model provides better performance, an important issue is investigating the weakest level of consistency needed by a given program (to satisfy its specification). As a way of dealing with this issue, we investigate the problem of checking whether a given program has the same set of behaviors when replacing a consistency model with a weaker one. This property known as <jats:italic>robustness<\/jats:italic> generally implies that any specification of the program is preserved when weakening the consistency. We focus on the robustness problem for consistency models which are weaker than standard serializability, namely, causal consistency, prefix consistency, and snapshot isolation. We show that checking robustness between these models is polynomial time reducible to a state reachability problem under serializability. We use this reduction to also derive a pragmatic proof technique based on Lipton\u2019s reduction theory that allows to prove programs robust. We have applied our techniques to several challenging applications drawn from the literature of distributed systems and databases.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_4","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T14:03:10Z","timestamp":1616421790000},"page":"87-117","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Checking Robustness Between Weak Transactional Consistency Models"],"prefix":"10.1007","author":[{"given":"Sidi Mohamed","family":"Beillahi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: Context-bounded analysis for POWER. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10206, pp. 56\u201374 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_4, https:\/\/doi.org\/10.1007\/978-3-662-54580-5_4","DOI":"10.1007\/978-3-662-54580-5_4"},{"key":"4_CR2","unstructured":"Adya, A.: Weak consistency: A generalized theory and optimistic implementations for distributed transactions. Ph.D. thesis (1999)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Alglave, J., Cousot, P.: Ogre and pythia: an invariance proof method for weak consistency models. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 3\u201318. ACM (2017), http:\/\/dl.acm.org\/citation.cfm?id=3009883","DOI":"10.1145\/3093333.3009883"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8044, pp. 141\u2013157. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9, https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. pp. 7\u201318. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706303, https:\/\/doi.org\/10.1145\/1706299.1706303","DOI":"10.1145\/1706299.1706303"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: What\u2019s decidable about weak memory models? In: Seidl, H. (ed.) Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7211, pp. 26\u201346. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_2, https:\/\/doi.org\/10.1007\/978-3-642-28869-2_2","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6806, pp. 99\u2013115. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_9, https:\/\/doi.org\/10.1007\/978-3-642-22110-1_9","DOI":"10.1007\/978-3-642-22110-1_9"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures. Lecture Notes in Computer Science, vol. 4111, pp. 364\u2013387. Springer (2005). https:\/\/doi.org\/10.1007\/11804192_17, https:\/\/doi.org\/10.1007\/11804192_17","DOI":"10.1007\/11804192_17"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Checking robustness against snapshot isolation. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. Lecture Notes in Computer Science, vol. 11562, pp. 286\u2013304. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_17, https:\/\/doi.org\/10.1007\/978-3-030-25543-5_17","DOI":"10.1007\/978-3-030-25543-5_17"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Robustness against transactional causal consistency. In: Fokkink, W.J., van Glabbeek, R. (eds.) 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands. LIPIcs, vol. 140, pp. 30:1\u201330:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.30, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.30.","DOI":"10.4230\/LIPIcs.CONCUR.2019.30"},{"key":"4_CR11","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Checking robustness between weak transactional consistency models. CoRR abs\/2101.09032 (2021), http:\/\/arxiv.org\/abs\/2101.09032"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Berenson, H., Bernstein, P.A., Gray, J., Melton, J., O\u2019Neil, E.J., O\u2019Neil, P.E.: A critique of ANSI SQL isolation levels. In: Carey, M.J., Schneider, D.A. (eds.) Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data, San Jose, California, USA, May 22-25, 1995. pp. 1\u201310. ACM Press (1995). https:\/\/doi.org\/10.1145\/223784.223785, https:\/\/doi.org\/10.1145\/223784.223785","DOI":"10.1145\/223784.223785"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Bernardi, G., Gotsman, A.: Robustness against consistency models with atomic visibility. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Qu\u00e9bec City, Canada. LIPIcs, vol. 59, pp. 7:1\u20137:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.7, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.7","DOI":"10.4230\/LIPIcs.CONCUR.2016.7"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Biswas, R., Enea, C.: On the complexity of checking transactional consistency. Proc. ACM Program. Lang. 3(OOPSLA), 165:1\u2013165:28 (2019). https:\/\/doi.org\/10.1145\/3360591, https:\/\/doi.org\/10.1145\/3360591","DOI":"10.1145\/3360591"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7792, pp. 533\u2013553. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29, https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 626\u2013638. ACM (2017), http:\/\/dl.acm.org\/citation.cfm?id=3009888","DOI":"10.1145\/3093333.3009888"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Meyer, R., M\u00f6hlmann, E.: Deciding robustness against total store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II. Lecture Notes in Computer Science, vol. 6756, pp. 428\u2013440. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22012-8_34, https:\/\/doi.org\/10.1007\/978-3-642-22012-8_34","DOI":"10.1007\/978-3-642-22012-8_34"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Brutschy, L., Dimitrov, D., M\u00fcller, P., Vechev, M.T.: Serializability for eventual consistency: criterion, analysis, and applications. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 458\u2013472. ACM (2017), http:\/\/dl.acm.org\/citation.cfm?id=3009895","DOI":"10.1145\/3009837.3009895"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Brutschy, L., Dimitrov, D., M\u00fcller, P., Vechev, M.T.: Static serializability analysis for causal consistency. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018. pp. 90\u2013104. ACM (2018). https:\/\/doi.org\/10.1145\/3192366.3192415, https:\/\/doi.org\/10.1145\/3192366.3192415","DOI":"10.1145\/3192366.3192415"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Burckhardt, S.: Principles of eventual consistency. Found. Trends Program. Lang. 1(1-2), 1\u2013150 (2014). https:\/\/doi.org\/10.1561\/2500000011, https:\/\/doi.org\/10.1561\/2500000011","DOI":"10.1561\/2500000011"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Burckhardt, S., Gotsman, A., Yang, H., Zawirski, M.: Replicated data types: specification, verification, optimality. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014. pp. 271\u2013284. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535848, https:\/\/doi.org\/10.1145\/2535838.2535848","DOI":"10.1145\/2535838.2535848"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Burckhardt, S., Leijen, D., Protzenko, J., F\u00e4hndrich, M.: Global sequence protocol: A robust abstraction for replicated shared state. In: Boyland, J.T. (ed.) 29th European Conference on Object-Oriented Programming, ECOOP 2015, July 5-10, 2015, Prague, Czech Republic. LIPIcs, vol. 37, pp. 568\u2013590. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2015.568, https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2015.568","DOI":"10.4230\/LIPIcs.ECOOP.2015.568"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Cahill, M.J., R\u00f6hm, U., Fekete, A.D.: Serializable isolation for snapshot databases. ACM Trans. Database Syst. 34(4), 20:1\u201320:42 (2009). https:\/\/doi.org\/10.1145\/1620585.1620587, https:\/\/doi.org\/10.1145\/1620585.1620587","DOI":"10.1145\/1620585.1620587"},{"key":"4_CR24","unstructured":"Cassandra-lock: https:\/\/github.com\/dekses\/cassandra-lock"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Cerone, A., Bernardi, G., Gotsman, A.: A framework for transactional consistency models with atomic visibility. In: Aceto, L., de Frutos-Escrig, D. (eds.) 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015. LIPIcs, vol. 42, pp. 58\u201371. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.58, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.58","DOI":"10.4230\/LIPIcs.CONCUR.2015.58"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Cerone, A., Gotsman, A.: Analysing snapshot isolation. J. ACM 65(2), 11:1\u201311:41 (2018). https:\/\/doi.org\/10.1145\/3152396, https:\/\/doi.org\/10.1145\/3152396","DOI":"10.1145\/3152396"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Cerone, A., Gotsman, A., Yang, H.: Algebraic laws for weak consistency. In: Meyer, R., Nestmann, U. (eds.) 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany. LIPIcs, vol. 85, pp. 26:1\u201326:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2017.26, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2017.26","DOI":"10.4230\/LIPIcs.CONCUR.2017.26"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Dan, A.M., Meshman, Y., Vechev, M.T., Yahav, E.: Effective abstractions for verification under relaxed memory models. Comput. Lang. Syst. Struct. 47, 62\u201376 (2017). https:\/\/doi.org\/10.1016\/j.cl.2016.02.003, https:\/\/doi.org\/10.1016\/j.cl.2016.02.003","DOI":"10.1016\/j.cl.2016.02.003"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Derevenetc, E., Meyer, R.: Robustness against power is pspace-complete. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II. Lecture Notes in Computer Science, vol. 8573, pp. 158\u2013170. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-662-43951-7_14, https:\/\/doi.org\/10.1007\/978-3-662-43951-7_14","DOI":"10.1007\/978-3-662-43951-7_14"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Difallah, D.E., Pavlo, A., Curino, C., Cudr\u00e9-Mauroux, P.: Oltp-bench: An extensible testbed for benchmarking relational databases. Proc. VLDB Endow. 7(4), 277\u2013288 (2013). https:\/\/doi.org\/10.14778\/2732240.2732246, http:\/\/www.vldb.org\/pvldb\/vol7\/p277-difallah.pdf","DOI":"10.14778\/2732240.2732246"},{"key":"4_CR31","unstructured":"Experiments: https:\/\/github.com\/relative-robustness\/artifact"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Gotsman, A., Yang, H., Ferreira, C., Najafzadeh, M., Shapiro, M.: \u2019cause i\u2019m strong enough: reasoning about consistency choices in distributed systems. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 371\u2013384. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837625, https:\/\/doi.org\/10.1145\/2837614.2837625","DOI":"10.1145\/2837614.2837625"},{"key":"4_CR33","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II. Lecture Notes in Computer Science, vol. 9207, pp. 449\u2013465. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_26, https:\/\/doi.org\/10.1007\/978-3-319-21668-3_26","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Holt, B., Bornholt, J., Zhang, I., Ports, D.R.K., Oskin, M., Ceze, L.: Disciplined inconsistency with consistency types. In: Aguilera, M.K., Cooper, B., Diao, Y. (eds.) Proceedings of the Seventh ACM Symposium on Cloud Computing, Santa Clara, CA, USA, October 5\u20137, 2016. pp. 279\u2013293. ACM (2016). https:\/\/doi.org\/10.1145\/2987550.2987559, https:\/\/doi.org\/10.1145\/2987550.2987559","DOI":"10.1145\/2987550.2987559"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Lower bounds for natural proof systems. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977. pp. 254\u2013266. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.16, https:\/\/doi.org\/10.1109\/SFCS.1977.16","DOI":"10.1109\/SFCS.1977.16"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Lahav, O., Margalit, R.: Robustness against release\/acquire semantics. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019. pp. 126\u2013141. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314604, https:\/\/doi.org\/10.1145\/3314221.3314604","DOI":"10.1145\/3314221.3314604"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-gries reasoning for weak memory models. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II. Lecture Notes in Computer Science, vol. 9135, pp. 311\u2013323. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_25, https:\/\/doi.org\/10.1007\/978-3-662-47666-6_25","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"4_CR38","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978). https:\/\/doi.org\/10.1145\/359545.359563, https:\/\/doi.org\/10.1145\/359545.359563","DOI":"10.1145\/359545.359563"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975). https:\/\/doi.org\/10.1145\/361227.361234, https:\/\/doi.org\/10.1145\/361227.361234","DOI":"10.1145\/361227.361234"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Nagar, K., Jagannathan, S.: Automated detection of serializability violations under weak consistency. In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China. LIPIcs, vol. 118, pp. 41:1\u201341:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.41, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.41","DOI":"10.4230\/LIPIcs.CONCUR.2018.41"},{"key":"4_CR41","doi-asserted-by":"publisher","unstructured":"Najafzadeh, M., Gotsman, A., Yang, H., Ferreira, C., Shapiro, M.: The CISE tool: proving weakly-consistent applications correct. In: Alvaro, P., Bessani, A. (eds.) Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, PaPoC@EuroSys 2016, London, United Kingdom, April 18, 2016. pp. 2:1\u20132:3. ACM (2016). https:\/\/doi.org\/10.1145\/2911151.2911160, https:\/\/doi.org\/10.1145\/2911151.2911160","DOI":"10.1145\/2911151.2911160"},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM 26(4), 631\u2013653 (1979). https:\/\/doi.org\/10.1145\/322154.322158, https:\/\/doi.org\/10.1145\/322154.322158","DOI":"10.1145\/322154.322158"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Perrin, M., Most\u00e9faoui, A., Jard, C.: Causal consistency: beyond memory. In: Asenjo, R., Harris, T. (eds.) Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, Barcelona, Spain, March 12-16, 2016. pp. 26:1\u201326:12. ACM (2016). https:\/\/doi.org\/10.1145\/2851141.2851170, https:\/\/doi.org\/10.1145\/2851141.2851170","DOI":"10.1145\/2851141.2851170"},{"key":"4_CR44","doi-asserted-by":"publisher","unstructured":"Raad, A., Lahav, O., Vafeiadis, V.: On the semantics of snapshot isolation. In: Enea, C., Piskac, R. (eds.) Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11388, pp. 1\u201323. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_1, https:\/\/doi.org\/10.1007\/978-3-030-11245-5_1","DOI":"10.1007\/978-3-030-11245-5_1"},{"key":"4_CR45","doi-asserted-by":"publisher","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223\u2013231 (1978). https:\/\/doi.org\/10.1016\/0304-3975(78)90036-1, https:\/\/doi.org\/10.1016\/0304-3975(78)90036-1","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"4_CR46","doi-asserted-by":"publisher","unstructured":"Shapiro, M., Ardekani, M.S., Petri, G.: Consistency in 3d. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Qu\u00e9bec City, Canada. LIPIcs, vol. 59, pp. 3:1\u20133:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.3, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.3","DOI":"10.4230\/LIPIcs.CONCUR.2016.3"},{"key":"4_CR47","doi-asserted-by":"publisher","unstructured":"Shasha, D.E., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10(2), 282\u2013312 (1988). https:\/\/doi.org\/10.1145\/42190.42277, https:\/\/doi.org\/10.1145\/42190.42277","DOI":"10.1145\/42190.42277"},{"key":"4_CR48","unstructured":"Trade: https:\/\/github.com\/Haiyan2\/Trade"},{"key":"4_CR49","unstructured":"Twitter: https:\/\/github.com\/edmundophie\/cassandra-twitter"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72019-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T03:04:45Z","timestamp":1635131085000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}