Modular Verification of Distributed Systems with Grove
Grove is a new framework for machine-checked verification of distributed systems. Grove focuses on modular verification. It enables developers to state and prove specifications for their components (e.g. an RPC library), and to use those specifications when proving the correctness of components that...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Published: |
Massachusetts Institute of Technology
2023
|
| Online Access: | https://hdl.handle.net/1721.1/147388 |
| _version_ | 1826216879041019904 |
|---|---|
| author | Sharma, Upamanyu |
| author2 | Kaashoek, M. Frans |
| author_facet | Kaashoek, M. Frans Sharma, Upamanyu |
| author_sort | Sharma, Upamanyu |
| collection | MIT |
| description | Grove is a new framework for machine-checked verification of distributed systems. Grove focuses on modular verification. It enables developers to state and prove specifications for their components (e.g. an RPC library), and to use those specifications when proving the correctness of components that build on it (e.g. a key value service built on RPC).
To enable modular specification and verification in a distributed systems, Grove uses the idea of ownership from separation logic. Using Grove, we built a verified unreliable RPC library, where we captured unreliability in the formal specification by using duplicable ownership. We also built a verified exactly-once RPC library, where we reasoned about ownership transfer from the client to server (and back) over an unreliable network by using the escrow pattern.
Overall, we developed and verified an example system written in Go consisting of the RPC libraries, a sharded key-value store with support for dynamically adding new servers and rebalancing shards, a lock service, and a bank application that supports atomic transfers across accounts that live in different shards, built on top of these services. The key-value service scales well with the number of servers and the number of cores per server. The proofs are mechanized in the Coq proof assistant using the Iris library and Goose. |
| first_indexed | 2024-09-23T16:54:52Z |
| format | Thesis |
| id | mit-1721.1/147388 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T16:54:52Z |
| publishDate | 2023 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1473882023-01-20T03:01:40Z Modular Verification of Distributed Systems with Grove Sharma, Upamanyu Kaashoek, M. Frans Zeldovich, Nickolai Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Grove is a new framework for machine-checked verification of distributed systems. Grove focuses on modular verification. It enables developers to state and prove specifications for their components (e.g. an RPC library), and to use those specifications when proving the correctness of components that build on it (e.g. a key value service built on RPC). To enable modular specification and verification in a distributed systems, Grove uses the idea of ownership from separation logic. Using Grove, we built a verified unreliable RPC library, where we captured unreliability in the formal specification by using duplicable ownership. We also built a verified exactly-once RPC library, where we reasoned about ownership transfer from the client to server (and back) over an unreliable network by using the escrow pattern. Overall, we developed and verified an example system written in Go consisting of the RPC libraries, a sharded key-value store with support for dynamically adding new servers and rebalancing shards, a lock service, and a bank application that supports atomic transfers across accounts that live in different shards, built on top of these services. The key-value service scales well with the number of servers and the number of cores per server. The proofs are mechanized in the Coq proof assistant using the Iris library and Goose. S.M. 2023-01-19T18:49:55Z 2023-01-19T18:49:55Z 2022-09 2022-10-19T18:58:50.592Z Thesis https://hdl.handle.net/1721.1/147388 In Copyright - Educational Use Permitted Copyright MIT http://rightsstatements.org/page/InC-EDU/1.0/ application/pdf Massachusetts Institute of Technology |
| spellingShingle | Sharma, Upamanyu Modular Verification of Distributed Systems with Grove |
| title | Modular Verification of Distributed Systems with Grove |
| title_full | Modular Verification of Distributed Systems with Grove |
| title_fullStr | Modular Verification of Distributed Systems with Grove |
| title_full_unstemmed | Modular Verification of Distributed Systems with Grove |
| title_short | Modular Verification of Distributed Systems with Grove |
| title_sort | modular verification of distributed systems with grove |
| url | https://hdl.handle.net/1721.1/147388 |
| work_keys_str_mv | AT sharmaupamanyu modularverificationofdistributedsystemswithgrove |