{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T14:59:46Z","timestamp":1780930786532,"version":"3.54.1"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906596","type":"print"},{"value":"9783031906602","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Modern web services crucially rely on high-performance distributed databases, where concurrent transactions are isolated from each other using concurrency control protocols. Relaxed isolation levels, which permit more complex concurrent behaviors than strong levels like serializability, are used in practice for higher performance and availability.<\/jats:p>\n          <jats:p>In this paper, we present Eiger-PORT+, a concurrency control protocol that achieves a strong form of causal consistency, called TCCv (Transactional Causal Consistency with convergence). We show that Eiger-PORT+ also provides performance-optimal read transactions in the presence of transactional writes, thus refuting an open conjecture that this is impossible for TCCv. We also deductively verify that Eiger-PORT+ satisfies this isolation level by refining an abstract model of transactions. This yields the first deductive verification of a complex concurrency control protocol. Furthermore, we conduct a performance evaluation showing Eiger-PORT+ \u2019s superior performance over the state-of-the-art.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_3","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:37:45Z","timestamp":1746005865000},"page":"43-62","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions"],"prefix":"10.1007","author":[{"given":"Shabnam","family":"Ghasemirad","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Sprenger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Si","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luca","family":"Multazzu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"3_CR1","unstructured":"Adya, A.: Weak consistency: a generalized theory and optimistic implementations for distributed transactions. Ph.D. thesis, Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science (1999)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Ahamad, M., Neiger, G., Burns, J.E., Kohli, P., Hutto, P.W.: Causal memory: Definitions, implementation, and programming. Distributed Comput. 9(1), 37\u201349 (1995)","DOI":"10.1007\/BF01784241"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Akkoorath, D.D., Tomsic, A.Z., Bravo, M., Li, Z., Crain, T., Bieniusa, A., Pregui\u00e7a, N.M., Shapiro, M.: Cure: Strong semantics meets high availability and low latency. In: ICDCS 2016. pp. 405\u2013414. IEEE Computer Society (2016)","DOI":"10.1109\/ICDCS.2016.98"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Attiya, H., Ellen, F., Morrison, A.: Limitations of highly-available eventually-consistent data stores. In: PODC 2015. pp. 385\u2013394. ACM (2015)","DOI":"10.1145\/2767386.2767419"},{"key":"3_CR5","unstructured":"Azure: azure-cosmos-tla. https:\/\/github.com\/Azure\/azure-cosmos-tla (2022)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Bailis, P., Fekete, A., Ghodsi, A., Hellerstein, J.M., Stoica, I.: Scalable atomic visibility with ramp transactions. ACM Transactions on Database Systems (TODS) 41(3), 1\u201345 (2016)","DOI":"10.1145\/2909870"},{"key":"3_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. ACM SIGMOD Record 24(2), 1\u201310 (1995)","DOI":"10.1145\/568271.223785"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Biswas, R., Enea, C.: On the complexity of checking transactional consistency. Proc. ACM Program. Lang. 3(OOPSLA), 165:1\u2013165:28 (2019)","DOI":"10.1145\/3360591"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Cerone, A., Gotsman, A.: Analysing snapshot isolation. J. ACM 65(2), 11:1\u201311:41 (2018)","DOI":"10.1145\/3152396"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Chkliaev, D., Hooman, J., van\u00a0der Stok, P.: Mechanical verification of transaction processing systems. In: ICFEM 2000. pp. 89\u2013100. IEEE Computer Society (2000)","DOI":"10.1109\/ICFEM.2000.873809"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Didona, D., Guerraoui, R., Wang, J., Zwaenepoel, W.: Causal consistency and latency optimality: Friend or foe? Proc. VLDB Endow. 11(11), 1618\u20131632 (2018)","DOI":"10.14778\/3236187.3236210"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Du, J., Elnikety, S., Zwaenepoel, W.: Clock-si: Snapshot isolation for partitioned data stores using loosely synchronized clocks. In: SRDS \u201913. pp. 173\u2013184. IEEE Computer Society (2013)","DOI":"10.1109\/SRDS.2013.26"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Duplyakin, D., Ricci, R., Maricq, A., Wong, G., Duerig, J., Eide, E., Stoller, L., Hibler, M., Johnson, D., Webb, K., Akella, A., Wang, K., Ricart, G., Landweber, L., Elliott, C., Zink, M., Cecchet, E., Kar, S., Mishra, P.: The design and operation of CloudLab. In: USENIX ATC\u201919. pp. 1\u201314 (Jul 2019)","DOI":"10.1109\/ICNP.2019.8888128"},{"key":"3_CR14","unstructured":"ElectricSQL: https:\/\/electric-sql.com\/ (2024)"},{"key":"3_CR15","unstructured":"Ghasemirad, S., Liu, S., Sprenger, C., Liu, S., Multazzua, L., Basin, D.: VerIso: Verifiable isolation guarantees for database transactions. Proc. VLDB Endow. 18 (2025), To appear."},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Ghasemirad, S., Sprenger, C., Liu, S., Multazzu, L., Basin, D.: Pushing the limit: Verified performance-optimal causally-consistent database transactions. CoRR abs\/2411.07049 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2411.07049","DOI":"10.48550\/ARXIV.2411.07049"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Ghasemirad, S., Sprenger, C., Liu, S., Multazzu, L., Basin, D.: Pushing the limit: Verified performance-optimal causally-consistent database transactions (artifacts) (Jan 2025). https:\/\/doi.org\/10.5281\/zenodo.14622073","DOI":"10.5281\/zenodo.14622073"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Grov, J., \u00d6lveczky, P.C.: Formal modeling and analysis of Google\u2019s Megastore in Real-Time Maude. In: Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi. LNCS, vol.\u00a08373, pp. 494\u2013519. Springer (2014)","DOI":"10.1007\/978-3-642-54624-2_25"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Gu, L., Liu, S., Xing, T., Wei, H., Chen, Y., Basin, D.: IsoVista: Black-box checking database isolation guarantees. Proc. VLDB Endow. 17(12) (2024)","DOI":"10.14778\/3685800.3685866"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Huang, K., Liu, S., Chen, Z., Wei, H., Basin, D., Li, H., Pan, A.: Efficient black-box checking of snapshot isolation in databases. Proc. VLDB Endow. 16(6), 1264\u20131276 (2023)","DOI":"10.14778\/3583140.3583145"},{"key":"3_CR21","unstructured":"Jepsen: Jepsen Analyses (2024), https:\/\/jepsen.io\/analyses"},{"key":"3_CR22","unstructured":"Jiang, Z.M., Liu, S., Rigger, M., Su, Z.: Detecting transactional bugs in database engines via graph-based oracle construction. In: OSDI\u201923. USENIX Association (2023)"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Katsarakis, A., Ma, Y., Tan, Z., Bainbridge, A., Balkwill, M., Dragojevic, A., Grot, B., Radunovic, B., Zhang, Y.: Zeus: locality-aware distributed transactions. In: EuroSys \u201921. pp. 145\u2013161. ACM (2021)","DOI":"10.1145\/3447786.3456234"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Kingsbury, K., Alvaro, P.: Elle: Inferring isolation anomalies from experimental observations. Proc. VLDB Endow. 14(3), 268\u2013280 (2020)","DOI":"10.14778\/3430915.3430918"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (jul 1978)","DOI":"10.1145\/359545.359563"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","DOI":"10.1145\/361227.361234"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Liu, S.: All in one: Design, verification, and implementation of SNOW-optimal read atomic transactions. ACM Trans. Softw. Eng. Methodol. 31(3) (Mar 2022)","DOI":"10.1145\/3494517"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Liu, S., Gu, L., Wei, H., Basin, D.: Plume: Efficient and complete black-box checking of weak isolation levels. Proc. ACM Program. Lang. 8(OOPSLA2) (2024)","DOI":"10.1145\/3689742"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Liu, S., Multazzu, L., Wei, H., Basin, D.: NOC-NOC: Towards Performance-optimal Distributed Transactions. Proc. ACM Manag. Data 2(1) (mar 2024)","DOI":"10.1145\/3639264"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Rahman, M.R., Ganhotra, J., Gupta, I., Meseguer, J.: Formal modeling and analysis of RAMP transaction systems. In: Proceedings of the 31st Annual ACM Symposium on Applied Computing, 2016. ACM (2016)","DOI":"10.1145\/2851613.2851838"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Wang, Q., Gupta, I., Meseguer, J.: Read atomic transactions with prevention of lost updates: ROLA and its formal analysis. Formal Aspects Comput. 31(5), 503\u2013540 (2019)","DOI":"10.1007\/s00165-019-00489-w"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Wang, Q., Meseguer, J.: Formal modeling and analysis of the Walter transactional data store. In: WRLA \u201918. LNCS, vol. 11152, pp. 136\u2013152. Springer (2018)","DOI":"10.1007\/978-3-319-99840-4_8"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Liu, S., Rahman, M.R., Skeirik, S., Gupta, I., Meseguer, J.: Formal modeling and analysis of Cassandra in Maude. In: ICFEM \u201914. LNCS, vol.\u00a08829, pp. 332\u2013347. Springer (2014)","DOI":"10.1007\/978-3-319-11737-9_22"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Lloyd, W., Freedman, M.J., Kaminsky, M., Andersen, D.G.: Don\u2019t settle for eventual: scalable causal consistency for wide-area storage with COPS. In: SOSP 2011. pp. 401\u2013416. ACM (2011)","DOI":"10.1145\/2043556.2043593"},{"key":"3_CR35","unstructured":"Lloyd, W., Freedman, M.J., Kaminsky, M., Andersen, D.G.: Stronger semantics for low-latency geo-replicated storage. In: NSDI 2013. pp. 313\u2013328. USENIX Association (2013)"},{"key":"3_CR36","unstructured":"Lu, H., Hodsdon, C., Ngo, K., Mu, S., Lloyd, W.: The SNOW theorem and latency-optimal read-only transactions. In: OSDI 2016. pp. 135\u2013150. USENIX Association (2016)"},{"key":"3_CR37","unstructured":"Lu, H., Mu, S., Sen, S., Lloyd, W.: NCC: Natural concurrency control for strictly serializable datastores by avoiding the Timestamp-Inversion pitfall. In: OSDI \u201923. pp. 305\u2013323. USENIX Association (2023)"},{"key":"3_CR38","unstructured":"Lu, H., Mu, S., Sen, S., Lloyd, W.: NCC: Natural concurrency control for strictly serializable datastores by avoiding the Timestamp-Inversion pitfall. In: OSDI \u201923. pp. 305\u2013323. USENIX Association (2023)"},{"key":"3_CR39","unstructured":"Mehdi, S.A., Littley, C., Crooks, N., Alvisi, L., Bronson, N., Lloyd, W.: I can\u2019t believe it\u2019s not causal! scalable causal consistency with no slowdown cascades. In: NSDI 2017. pp. 453\u2013468. USENIX Association (2017)"},{"key":"3_CR40","unstructured":"Microsoft: Azure CosmosDB DB. https:\/\/learn.microsoft.com\/en-us\/azure\/cosmos-db\/consistency-levels (2024)"},{"key":"3_CR41","unstructured":"Neo4j: https:\/\/neo4j.com\/ (2024)"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Formalizing and validating the P-Store replicated data store in Maude. In: WADT \u201916. LNCS, vol. 10644, pp. 189\u2013207. Springer (2016)","DOI":"10.1007\/978-3-319-72044-9_13"},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Papadimitriou, C.H.: The serializability of concurrent database updates. Journal of the ACM (JACM) 26(4), 631\u2013653 (1979)","DOI":"10.1145\/322154.322158"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Perrin, M., Mostefaoui, A., Jard, C.: Causal consistency: Beyond memory. SIGPLAN Not. 51(8), 26:1\u201326:12 (Feb 2016)","DOI":"10.1145\/3016078.2851170"},{"key":"3_CR45","unstructured":"PingCAP: tla-plus. https:\/\/github.com\/pingcap\/tla-plus (2022)"},{"key":"3_CR46","unstructured":"Silberschatz, A., Korth, H.F., Sudarshan, S.: Database System Concepts, Seventh Edition. McGraw-Hill Book Company (2020), https:\/\/www.db-book.com\/"},{"key":"3_CR47","doi-asserted-by":"crossref","unstructured":"Spirovska, K., Didona, D., Zwaenepoel, W.: Optimistic causal consistency for geo-replicated key-value stores. IEEE Trans. Parallel Distributed Syst. 32(3), 527\u2013542 (2021)","DOI":"10.1109\/TPDS.2020.3026778"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Sprenger, C., Klenze, T., Eilers, M., Wolf, F., M\u00fcller, P., Clochard, M., Basin, D.: Igloo: Soundly linking compositional refinement and separation logic for distributed systems verification. In: ACM Program. Lang. 4, OOPSLA, Article 152 (2020)","DOI":"10.1145\/3428220"},{"key":"3_CR49","unstructured":"Tan, C., Zhao, C., Mu, S., Walfish, M.: Cobra: Making transactional key-value stores verifiably serializable. In: 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020. pp. 63\u201380. USENIX Association (2020)"},{"key":"3_CR50","unstructured":"Xiong, S., Cerone, A., Raad, A., Gardner, P.: Data consistency in transactional storage systems: A centralised semantics. In: 34th European Conference on Object-Oriented Programming, ECOOP 2020. LIPIcs, vol.\u00a0166, pp. 21:1\u201321:31. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Yadav, D., Butler, M.J.: Rigorous design of fault-tolerant transactions for replicated database systems using Event B. In: Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project]. LNCS, vol.\u00a04157, pp. 343\u2013363. Springer (2006)","DOI":"10.1007\/11916246_18"},{"key":"3_CR52","doi-asserted-by":"crossref","unstructured":"Yang, J., Yue, Y., Rashmi, K.V.: A large-scale analysis of hundreds of in-memory key-value cache clusters at Twitter. ACM Trans. Storage 17(3), 17:1\u201317:35 (2021)","DOI":"10.1145\/3468521"},{"key":"3_CR53","doi-asserted-by":"crossref","unstructured":"Zhang, I., Sharma, N.K., Szekeres, A., Krishnamurthy, A., Ports, D.R.K.: Building consistent transactions with inconsistent replication. In: SOSP \u201915. p. 263-278. ACM (2015)","DOI":"10.1145\/2815400.2815404"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90660-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:13Z","timestamp":1746005893000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}