{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:16:44Z","timestamp":1760044604015,"version":"3.41.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006602","name":"Air Force Research Lab","doi-asserted-by":"crossref","award":["FA8750-17-1-0006"],"award-info":[{"award-number":["FA8750-17-1-0006"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-SHF 1717741"],"award-info":[{"award-number":["CCF-SHF 1717741"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>Serializability is a well-understood correctness criterion that simplifies reasoning about the behavior of concurrent transactions by ensuring they are isolated from each other while they execute. However, enforcing serializable isolation comes at a steep cost in performance because it necessarily restricts opportunities to exploit concurrency even when such opportunities would not violate application-specific invariants. As a result, database systems in practice support, and often encourage, developers to implement transactions using weaker alternatives. These alternatives break the strong isolation guarantees offered by serializable transactions to permit greater concurrency. Unfortunately, the semantics of weak isolation is poorly understood, and usually explained only informally in terms of low-level implementation artifacts. Consequently, verifying high-level correctness properties in such environments remains a challenging problem. To address this issue, we present a novel program logic that enables compositional reasoning about the behavior of concurrently executing weakly-isolated transactions. Recognizing that the proof burden necessary to use this logic may dissuade application developers, we also describe an inference procedure based on this foundation that ascertains the weakest isolation level that still guarantees the safety of high-level consistency assertions associated with such transactions. The key to effective inference is the observation that weakly-isolated transactions can be viewed as functional (monadic) computations over an abstract database state, allowing us to treat their operations as state transformers over the database. This interpretation enables automated verification using off-the-shelf SMT solvers. Our development is parametric over a transaction\u2019s specific isolation semantics, allowing it to be applicable over a range of concurrency control mechanisms. Case studies and experiments on real-world applications (written in an embedded DSL in OCaml) demonstrate the utility of our approach, and provide strong evidence that automated verification of weakly-isolated transactions can be placed on the same formal footing as their strongly-isolated serializable counterparts.<\/jats:p>","DOI":"10.1145\/3158115","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Alone together: compositional reasoning and inference for weak isolation"],"prefix":"10.1145","volume":"2","author":[{"given":"Gowtham","family":"Kaki","sequence":"first","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Kartik","family":"Nagar","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Mahsa","family":"Najafzadeh","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"unstructured":"Atul Adya. 1999. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. Ph.D. Dissertation. Cambridge MA USA. AAI0800775.  Atul Adya. 1999. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. Ph.D. Dissertation. Cambridge MA USA. AAI0800775.","key":"e_1_2_2_1_1"},{"volume-title":"CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings. 249\u2013260","author":"Alvaro Peter","unstructured":"Peter Alvaro , Neil Conway , Joe Hellerstein , and William R. Marczak . 2011. Consistency Analysis in Bloom: a CALM and Collected Approach . In CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings. 249\u2013260 . Peter Alvaro, Neil Conway, Joe Hellerstein, and William R. Marczak. 2011. Consistency Analysis in Bloom: a CALM and Collected Approach. In CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings. 249\u2013260.","key":"e_1_2_2_2_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_3_1","DOI":"10.1145\/2463676.2465296"},{"doi-asserted-by":"publisher","key":"e_1_2_2_4_1","DOI":"10.14778\/2732232.2732237"},{"doi-asserted-by":"publisher","key":"e_1_2_2_5_1","DOI":"10.14778\/2735508.2735509"},{"doi-asserted-by":"publisher","key":"e_1_2_2_6_1","DOI":"10.1145\/2723372.2737784"},{"key":"e_1_2_2_7_1","volume-title":"Proceedings of the 14th USENIX Conference on Hot Topics in Operating Systems (HotOS\u201913)","author":"Bailis Peter","year":"2013","unstructured":"Peter Bailis , Alan Fekete , Ali Ghodsi , Joseph M. Hellerstein , and Ion Stoica . 2013 b. HAT, Not CAP: Towards Highly Available Transactions . In Proceedings of the 14th USENIX Conference on Hot Topics in Operating Systems (HotOS\u201913) . USENIX Association, Berkeley, CA, USA, 24\u201324. http:\/\/dl.acm.org\/citation.cfm?id=2490483.2490507 Peter Bailis, Alan Fekete, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. 2013b. HAT, Not CAP: Towards Highly Available Transactions. In Proceedings of the 14th USENIX Conference on Hot Topics in Operating Systems (HotOS\u201913). USENIX Association, Berkeley, CA, USA, 24\u201324. http:\/\/dl.acm.org\/citation.cfm?id=2490483.2490507"},{"doi-asserted-by":"publisher","key":"e_1_2_2_8_1","DOI":"10.1145\/2741948.2741972"},{"doi-asserted-by":"publisher","key":"e_1_2_2_9_1","DOI":"10.1145\/223784.223785"},{"doi-asserted-by":"publisher","key":"e_1_2_2_10_1","DOI":"10.1109\/ICDE.2000.839387"},{"doi-asserted-by":"publisher","key":"e_1_2_2_11_1","DOI":"10.1145\/2463676.2465339"},{"doi-asserted-by":"publisher","key":"e_1_2_2_12_1","DOI":"10.1145\/319996.319998"},{"unstructured":"Bitcoin Bug 2016. How I Stole Roughly 100 BTC From an Exchange and How I Could Have Stolen More! https:\/\/goo.gl\/4SqaP2  Bitcoin Bug 2016. How I Stole Roughly 100 BTC From an Exchange and How I Could Have Stolen More! https:\/\/goo.gl\/4SqaP2","key":"e_1_2_2_13_1"},{"volume-title":"The Classical Decision Problem","author":"B\u00f6rger Ergon","unstructured":"Ergon B\u00f6rger , Erich Gr\u00e4del , and Yuri Gurevich . 1996. The Classical Decision Problem . Springer-Verlag Telos . Ergon B\u00f6rger, Erich Gr\u00e4del, and Yuri Gurevich. 1996. The Classical Decision Problem. Springer-Verlag Telos.","key":"e_1_2_2_14_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_15_1","DOI":"10.1145\/2535838.2535848"},{"doi-asserted-by":"publisher","key":"e_1_2_2_16_1","DOI":"10.1145\/1376616.1376690"},{"doi-asserted-by":"publisher","key":"e_1_2_2_17_1","DOI":"10.4230\/LIPIcs.CONCUR.2015.58"},{"doi-asserted-by":"publisher","key":"e_1_2_2_18_1","DOI":"10.1145\/2933057.2933096"},{"doi-asserted-by":"publisher","key":"e_1_2_2_19_1","DOI":"10.1145\/3087801.3087802"},{"doi-asserted-by":"publisher","key":"e_1_2_2_20_1","DOI":"10.1145\/5505.5508"},{"doi-asserted-by":"publisher","key":"e_1_2_2_21_1","DOI":"10.1145\/360363.360369"},{"doi-asserted-by":"publisher","key":"e_1_2_2_22_1","DOI":"10.14778\/1687627.1687681"},{"doi-asserted-by":"publisher","key":"e_1_2_2_23_1","DOI":"10.1145\/1071610.1071615"},{"doi-asserted-by":"publisher","key":"e_1_2_2_24_1","DOI":"10.1145\/2737924.2738006"},{"key":"e_1_2_2_25_1","volume-title":"Database Systems: The Complete Book (2 ed.)","author":"Garcia-Molina Hector","year":"2008","unstructured":"Hector Garcia-Molina , Jeffrey D. Ullman , and Jennifer Widom . 2008 . Database Systems: The Complete Book (2 ed.) . Prentice Hall Press , Upper Saddle River, NJ, USA. Hector Garcia-Molina, Jeffrey D. Ullman, and Jennifer Widom. 2008. Database Systems: The Complete Book (2 ed.). Prentice Hall Press, Upper Saddle River, NJ, USA."},{"doi-asserted-by":"publisher","key":"e_1_2_2_26_1","DOI":"10.1145\/564585.564601"},{"doi-asserted-by":"publisher","key":"e_1_2_2_27_1","DOI":"10.1145\/2837614.2837625"},{"unstructured":"J. N. Gray R. A. Lorie G. R. Putzolu and I. L. Traiger. 1976. Granularity of Locks and Degrees of Consistency in a Shared Data Base. 365\u2013394.  J. N. Gray R. A. Lorie G. R. Putzolu and I. L. Traiger. 1976. Granularity of Locks and Degrees of Consistency in a Shared Data Base. 365\u2013394.","key":"e_1_2_2_28_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_29_1","DOI":"10.1007\/978-3-319-21668-3_26"},{"doi-asserted-by":"publisher","key":"e_1_2_2_30_1","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_2_31_1","volume-title":"Alone Together: Compositional Reasoning and Inference for Weak Isolation. https:\/\/arxiv.org\/abs\/1710.09844.","author":"Kaki Gowtham","year":"2018","unstructured":"Gowtham Kaki , Kartik Nagar , Mahsa Najafzadeh , and Suresh Jagannathan . 2018 . Alone Together: Compositional Reasoning and Inference for Weak Isolation. https:\/\/arxiv.org\/abs\/1710.09844. Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan. 2018. Alone Together: Compositional Reasoning and Inference for Weak Isolation. https:\/\/arxiv.org\/abs\/1710.09844."},{"doi-asserted-by":"publisher","key":"e_1_2_2_32_1","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_2_33_1","volume-title":"Proceedings of USENIX Annual Technical Conference (USENIX ATC\u201914)","author":"Li Cheng","year":"2014","unstructured":"Cheng Li , Jo\u00e3o Leit\u00e3o , Allen Clement , Nuno Pregui\u00e7a , Rodrigo Rodrigues , and Viktor Vafeiadis . 2014 . Automating the Choice of Consistency Levels in Replicated Systems . In Proceedings of USENIX Annual Technical Conference (USENIX ATC\u201914) . USENIX Association, Berkeley, CA, USA, 281\u2013292. http:\/\/dl.acm.org\/citation.cfm?id=2643634.2643664 Cheng Li, Jo\u00e3o Leit\u00e3o, Allen Clement, Nuno Pregui\u00e7a, Rodrigo Rodrigues, and Viktor Vafeiadis. 2014. Automating the Choice of Consistency Levels in Replicated Systems. In Proceedings of USENIX Annual Technical Conference (USENIX ATC\u201914). USENIX Association, Berkeley, CA, USA, 281\u2013292. http:\/\/dl.acm.org\/citation.cfm?id=2643634.2643664"},{"doi-asserted-by":"publisher","key":"e_1_2_2_34_1","DOI":"10.5555\/2387880.2387906"},{"unstructured":"MySQL 2016. Transaction Isolation Levels. https:\/\/dev.mysql.com\/doc\/refman\/5.6\/en\/innodb- transaction- isolation- levels. html Accessed: 2016-07-1 10:00:00.  MySQL 2016. Transaction Isolation Levels. https:\/\/dev.mysql.com\/doc\/refman\/5.6\/en\/innodb- transaction- isolation- levels. html Accessed: 2016-07-1 10:00:00.","key":"e_1_2_2_35_1"},{"unstructured":"Oracle 2016. Data Concurrency and Consistency. https:\/\/docs.oracle.com\/cd\/B28359_01\/server.111\/b28318\/consist.htm Accessed: 2016-07-1 10:00:00.  Oracle 2016. Data Concurrency and Consistency. https:\/\/docs.oracle.com\/cd\/B28359_01\/server.111\/b28318\/consist.htm Accessed: 2016-07-1 10:00:00.","key":"e_1_2_2_36_1"},{"unstructured":"Poloniex Bug 2016. BTC Stolen from Poloniex. https:\/\/bitcointalk.org\/index.php?topic=499580  Poloniex Bug 2016. BTC Stolen from Poloniex. https:\/\/bitcointalk.org\/index.php?topic=499580","key":"e_1_2_2_37_1"},{"unstructured":"PostgreSQL 2016. Transaction Isolation. https:\/\/www.postgresql.org\/docs\/9.1\/static\/transaction- iso.html Accessed: 2016-07-1 10:00:00.  PostgreSQL 2016. Transaction Isolation. https:\/\/www.postgresql.org\/docs\/9.1\/static\/transaction- iso.html Accessed: 2016-07-1 10:00:00.","key":"e_1_2_2_38_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_39_1","DOI":"10.1109\/ICDE.2011.5767853"},{"doi-asserted-by":"publisher","key":"e_1_2_2_40_1","DOI":"10.1109\/LICS.2002.1029817"},{"unstructured":"SciMed Bug 2016. Avoid Race Conditions that Violate Uniqueness Validation - Rails. http:\/\/goo.gl\/0QhMQj  SciMed Bug 2016. Avoid Race Conditions that Violate Uniqueness Validation - Rails. http:\/\/goo.gl\/0QhMQj","key":"e_1_2_2_41_1"},{"key":"e_1_2_2_42_1","volume-title":"Database Tuning: Principles, Experiments, and Troubleshooting Techniques","author":"Shasha Dennis","year":"2003","unstructured":"Dennis Shasha and Philippe Bonnet . 2003 . Database Tuning: Principles, Experiments, and Troubleshooting Techniques . Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA. Dennis Shasha and Philippe Bonnet. 2003. Database Tuning: Principles, Experiments, and Troubleshooting Techniques. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA."},{"doi-asserted-by":"publisher","key":"e_1_2_2_43_1","DOI":"10.1145\/2737924.2737981"},{"doi-asserted-by":"publisher","key":"e_1_2_2_44_1","DOI":"10.1145\/2043556.2043592"},{"unstructured":"Starbucks Bug 2016. Hacking Starbucks for unlimited coffee. http:\/\/sakurity.com\/blog\/2015\/05\/21\/starbucks.html  Starbucks Bug 2016. Hacking Starbucks for unlimited coffee. http:\/\/sakurity.com\/blog\/2015\/05\/21\/starbucks.html","key":"e_1_2_2_45_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_46_1","DOI":"10.1007\/978-3-642-14295-6_40"},{"doi-asserted-by":"publisher","key":"e_1_2_2_47_1","DOI":"10.1007\/978-3-642-11319-2_25"},{"key":"e_1_2_2_48_1","volume-title":"CONCUR 2007 \u2013 Concurrency Theory. Springer Berlin Heidelberg","author":"Parkinson Viktor","year":"2007","unstructured":"Vafeiadis, Viktor and Parkinson , Matthew. 2007 . A Marriage of Rely\/Guarantee and Separation Logic . In CONCUR 2007 \u2013 Concurrency Theory. Springer Berlin Heidelberg , Berlin, Heidelberg, 256\u2013271. Vafeiadis, Viktor and Parkinson, Matthew. 2007. A Marriage of Rely\/Guarantee and Separation Logic. In CONCUR 2007 \u2013 Concurrency Theory. Springer Berlin Heidelberg, Berlin, Heidelberg, 256\u2013271."},{"doi-asserted-by":"publisher","key":"e_1_2_2_49_1","DOI":"10.1145\/3035918.3064037"},{"doi-asserted-by":"publisher","key":"e_1_2_2_50_1","DOI":"10.1007\/s00778-013-0318-x"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158115","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158115","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158115","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158115"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":50,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158115"],"URL":"https:\/\/doi.org\/10.1145\/3158115","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}