{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:10:46Z","timestamp":1775790646725,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030112448","type":"print"},{"value":"9783030112455","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-11245-5_1","type":"book-chapter","created":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T18:45:18Z","timestamp":1547145918000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["On the Semantics of Snapshot Isolation"],"prefix":"10.1007","author":[{"given":"Azalea","family":"Raad","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,11]]},"reference":[{"key":"1_CR1","unstructured":"The Clojure Language: Refs and Transactions. http:\/\/clojure.org\/refs"},{"key":"1_CR2","unstructured":"Technical specification for C++ extensions for transactional memory (2015). http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2015\/n4514.pdf"},{"key":"1_CR3","unstructured":"Adya, A.: Weak consistency: a generalized theory and optimistic implementations for distributed transactions. Ph.D. thesis, MIT (1999)"},{"key":"1_CR4","unstructured":"Adya, A., Liskov, B., O\u2019Neil, P.: Generalized isolation level definitions. In: Proceedings of the 16th International Conference on Data Engineering, pp. 67\u201378 (2000)"},{"issue":"2","key":"1_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2627752","volume":"36","author":"Jade Alglave","year":"2014","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1\u20137:74 (2014)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 55\u201366 (2011)","DOI":"10.1145\/1926385.1926394"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Berenson, H., Bernstein, P., Gray, J., Melton, J., O\u2019Neil, E., O\u2019Neil, P.: A critique of ANSI SQL isolation levels. In: Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data, pp. 1\u201310 (1995)","DOI":"10.1145\/223784.223785"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Bieniusa, A., Fuhrmann, T.: Consistency in hindsight: a fully decentralized STM algorithm. In: Proceedings of the 2010 IEEE International Symposium on Parallel and Distributed Processing, IPDPS 2010, pp. 1\u201312 (2010)","DOI":"10.1109\/IPDPS.2010.5470446"},{"key":"1_CR9","unstructured":"Blundell, C., Lewis, E.C., Martin, M.M.K.: Deconstructing transactions: the subtleties of atomicity. In: 4th Annual Workshop on Duplicating, Deconstructing, and Debunking (2005)"},{"key":"1_CR10","unstructured":"Cerone, A., Bernardi, G., Gotsman, A.: A framework for transactional consistency models with atomic visibility. In: Proceedings of the 26th International Conference on Concurrency Theory, pp. 58\u201371 (2015)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Cerone, A., Gotsman, A.: Analysing snapshot isolation. In: Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, pp. 55\u201364 (2016)","DOI":"10.1145\/2933057.2933096"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-662-48653-5_26","volume-title":"Distributed Computing","author":"A Cerone","year":"2015","unstructured":"Cerone, A., Gotsman, A., Yang, H.: Transaction chopping for parallel snapshot isolation. In: Moses, Y. (ed.) DISC 2015. LNCS, vol. 9363, pp. 388\u2013404. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48653-5_26"},{"key":"1_CR13","unstructured":"Cerone, A., Gotsman, A., Yang, H.: Algebraic laws for weak consistency. In: CONCUR (2017)"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Crooks, N., Pu, Y., Alvisi, L., Clement, A.: Seeing is believing: a client-centric specification of database isolation. In: Proceedings of the ACM Symposium on Principles of Distributed Computing, PODC 2017, pp. 73\u201382. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3087801.3087802","DOI":"10.1145\/3087801.3087802"},{"key":"1_CR15","unstructured":"Daudjee, K., Salem, K.: Lazy database replication with snapshot isolation. In: Proceedings of the 32nd International Conference on Very Large Data Bases, pp. 715\u2013726 (2006)"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-31057-7_28","volume-title":"ECOOP 2012 \u2013 Object-Oriented Programming","author":"RJ Dias","year":"2012","unstructured":"Dias, R.J., Distefano, D., Seco, J.C., Louren\u00e7o, J.M.: Verification of snapshot isolation in transactional memory Java programs. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol. 7313, pp. 640\u2013664. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31057-7_28"},{"issue":"POPL","key":"1_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158106","volume":"2","author":"Brijesh Dongol","year":"2017","unstructured":"Dongol, B., Jagadeesan, R., Riely, J.: Transactions in relaxed memory architectures. Proc. ACM Program. Lang. 2(POPL), 18:1\u201318:29 (2017). https:\/\/doi.org\/10.1145\/3158106","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"1_CR18","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: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 371\u2013384. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2837614.2837625","DOI":"10.1145\/2837614.2837625"},{"key":"1_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01728-5","volume-title":"Transactional Memory","author":"T Harris","year":"2010","unstructured":"Harris, T., Larus, J., Rajwar, R.: Transactional Memory, 2nd edn. Morgan and Claypool Publishers, San Rafael (2010)","edition":"2"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Moss, J.E.B.: Transactional memory: architectural support for lock-free data structures. In: Proceedings of the 20th Annual International Symposium on Computer Architecture, pp. 289\u2013300 (1993)","DOI":"10.1145\/165123.165164"},{"issue":"POPL","key":"1_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158115","volume":"2","author":"Gowtham Kaki","year":"2017","unstructured":"Kaki, G., Nagar, K., Najafzadeh, M., Jagannathan, S.: Alone together: compositional reasoning and inference for weak isolation. Proc. ACM Program. Lang. 2(POPL), 27:1\u201327:34 (2017). https:\/\/doi.org\/10.1145\/3158115","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Khyzha, A., Attiya, H., Gotsman, A., Rinetzky, N.: Safe privatization in transactional memory. In: Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 233\u2013245 (2018)","DOI":"10.1145\/3178487.3178505"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 649\u2013662 (2016)","DOI":"10.1145\/2837614.2837643"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-662-47666-6_25","volume-title":"Automata, Languages, and Programming","author":"O Lahav","year":"2015","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-gries reasoning for weak memory models. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311\u2013323. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_25"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1145\/2692916.2555280","volume":"49","author":"H Litz","year":"2014","unstructured":"Litz, H., Cheriton, D., Firoozshahian, A., Azizi, O., Stevenson, J.P.: SI-TM: reducing transactional memory abort rates through snapshot isolation. SIGPLAN Not. 49, 383\u2013398 (2014)","journal-title":"SIGPLAN Not."},{"issue":"4","key":"1_CR26","doi-asserted-by":"publisher","first-page":"65:1","DOI":"10.1145\/2693260","volume":"11","author":"H Litz","year":"2015","unstructured":"Litz, H., Dias, R.J., Cheriton, D.R.: Efficient correction of anomalies in snapshot isolation transactions. ACM Trans. Archit. Code Optim. 11(4), 65:1\u201365:24 (2015). https:\/\/doi.org\/10.1145\/2693260","journal-title":"ACM Trans. Archit. Code Optim."},{"issue":"2","key":"1_CR27","first-page":"17","volume":"5","author":"M Martin","year":"2006","unstructured":"Martin, M., Blundell, C., Lewis, E.: Subtleties of transactional memory atomicity semantics. IEEE Comput. Archit. Lett. 5(2), 17 (2006)","journal-title":"IEEE Comput. Archit. Lett."},{"issue":"4","key":"1_CR28","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"CH Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM 26(4), 631\u2013653 (1979). https:\/\/doi.org\/10.1145\/322154.322158","journal-title":"J. ACM"},{"key":"1_CR29","unstructured":"Peng, D., Dabek, F.: Large-scale incremental processing using distributed transactions and notifications. In: Proceedings of the 9th USENIX Conference on Operating Systems Design and Implementation, pp. 251\u2013264 (2010)"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"940","DOI":"10.1007\/978-3-319-89884-1_33","volume-title":"Programming Languages and Systems","author":"A Raad","year":"2018","unstructured":"Raad, A., Lahav, O., Vafeiadis, V.: On parallel snapshot isolation and release\/acquire consistency. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 940\u2013967. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_33"},{"key":"1_CR31","unstructured":"Raad, A., Lahav, O., Vafeiadis, V.: The technical appendix for this paper. https:\/\/arxiv.org\/abs\/1805.06196 (2018)"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Serrano, D., Patino-Martinez, M., Jimenez-Peris, R., Kemme, B.: Boosting database replication scalability through partial replication and 1-copy-snapshot-isolation. In: Proceedings of the 13th Pacific Rim International Symposium on Dependable Computing, pp. 290\u2013297 (2007)","DOI":"10.1109\/PRDC.2007.39"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Shavit, N., Touitou, D.: Software transactional memory. In: Proceedings of the Fourteenth Annual ACM Symposium on Principles of Distributed Computing, pp. 204\u2013213 (1995)","DOI":"10.1145\/224964.224987"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Sovran, Y., Power, R., Aguilera, M.K., Li, J.: Transactional storage for geo-replicated systems. In: Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles, pp. 385\u2013400 (2011)","DOI":"10.1145\/2043556.2043592"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, pp. 867\u2013884 (2013)","DOI":"10.1145\/2509136.2509532"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-11245-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,10]],"date-time":"2022-09-10T02:10:15Z","timestamp":1662775815000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-11245-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030112448","9783030112455"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-11245-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cascais","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl19.sigplan.org\/track\/VMCAI-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}