Chapar: certified causally consistent distributed key-value stores
© 2016 ACM. Today's Internet services are often expected to stay available and render high responsiveness even in the face of site crashes and network partitions. Theoretical results state that causal consistency is one of the strongest consistency guarantees that is possible under these requir...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
ACM
2021
|
| Online Access: | https://hdl.handle.net/1721.1/137718 |
| _version_ | 1826188332155011072 |
|---|---|
| author | Lesani, Mohsen Bell, Christian J. Chlipala, Adam |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Lesani, Mohsen Bell, Christian J. Chlipala, Adam |
| author_sort | Lesani, Mohsen |
| collection | MIT |
| description | © 2016 ACM. Today's Internet services are often expected to stay available and render high responsiveness even in the face of site crashes and network partitions. Theoretical results state that causal consistency is one of the strongest consistency guarantees that is possible under these requirements, and many practical systems provide causally consistent key-value stores. In this paper, we present a framework called Chapar for modular verification of causal consistency for replicated key-value store implementations and their client programs. Specifically, we formulate separate correctness conditions for key-value store implementations and for their clients. The interface between the two is a novel operational semantics for causal consistency. We have verified the causal consistency of two key-value store implementations from the literature using a novel proof technique. We have also implemented a simple automatic model checker for the correctness of client programs. The two independently verified results for the implementations and clients can be composed to conclude the correctness of any of the programs when executed with any of the implementations. We have developed and checked our framework in Coq, extracted it to OCaml, and built executable stores. |
| first_indexed | 2024-09-23T07:58:03Z |
| format | Article |
| id | mit-1721.1/137718 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T07:58:03Z |
| publishDate | 2021 |
| publisher | ACM |
| record_format | dspace |
| spelling | mit-1721.1/1377182023-03-29T19:38:59Z Chapar: certified causally consistent distributed key-value stores Lesani, Mohsen Bell, Christian J. Chlipala, Adam Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science © 2016 ACM. Today's Internet services are often expected to stay available and render high responsiveness even in the face of site crashes and network partitions. Theoretical results state that causal consistency is one of the strongest consistency guarantees that is possible under these requirements, and many practical systems provide causally consistent key-value stores. In this paper, we present a framework called Chapar for modular verification of causal consistency for replicated key-value store implementations and their client programs. Specifically, we formulate separate correctness conditions for key-value store implementations and for their clients. The interface between the two is a novel operational semantics for causal consistency. We have verified the causal consistency of two key-value store implementations from the literature using a novel proof technique. We have also implemented a simple automatic model checker for the correctness of client programs. The two independently verified results for the implementations and clients can be composed to conclude the correctness of any of the programs when executed with any of the implementations. We have developed and checked our framework in Coq, extracted it to OCaml, and built executable stores. 2021-11-08T17:14:02Z 2021-11-08T17:14:02Z 2016-01-11 2019-10-04T16:37:52Z Article http://purl.org/eprint/type/ConferencePaper https://hdl.handle.net/1721.1/137718 Lesani, Mohsen, Bell, Christian J. and Chlipala, Adam. 2016. "Chapar: certified causally consistent distributed key-value stores." en 10.1145/2837614.2837622 Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf ACM Prof. Chlipala via Phoebe Ayers |
| spellingShingle | Lesani, Mohsen Bell, Christian J. Chlipala, Adam Chapar: certified causally consistent distributed key-value stores |
| title | Chapar: certified causally consistent distributed key-value stores |
| title_full | Chapar: certified causally consistent distributed key-value stores |
| title_fullStr | Chapar: certified causally consistent distributed key-value stores |
| title_full_unstemmed | Chapar: certified causally consistent distributed key-value stores |
| title_short | Chapar: certified causally consistent distributed key-value stores |
| title_sort | chapar certified causally consistent distributed key value stores |
| url | https://hdl.handle.net/1721.1/137718 |
| work_keys_str_mv | AT lesanimohsen chaparcertifiedcausallyconsistentdistributedkeyvaluestores AT bellchristianj chaparcertifiedcausallyconsistentdistributedkeyvaluestores AT chlipalaadam chaparcertifiedcausallyconsistentdistributedkeyvaluestores |