GoTxn: Verifying a Crash-Safe, Concurrent Transaction System
Bugs related to concurrency and crash safety are infamous for being subtle and hard to reproduce. Formal verification provides a way to combat such bugs through the use of machine-checked proofs about program behavior. However, reasoning about concurrency and crashes can be tricky, especially when s...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Published: |
Massachusetts Institute of Technology
2022
|
| Online Access: | https://hdl.handle.net/1721.1/143253 |
| _version_ | 1811072579167846400 |
|---|---|
| author | Theng, Mark |
| author2 | Kaashoek, M. Frans |
| author_facet | Kaashoek, M. Frans Theng, Mark |
| author_sort | Theng, Mark |
| collection | MIT |
| description | Bugs related to concurrency and crash safety are infamous for being subtle and hard to reproduce. Formal verification provides a way to combat such bugs through the use of machine-checked proofs about program behavior. However, reasoning about concurrency and crashes can be tricky, especially when scaling up to larger systems that must also have good performance.
This thesis discusses the verification of GoTxn, the concurrent, crash-safe transaction system underlying the verified Network File System (NFS) server DaisyNFS. It focuses on the specification and proof of the write-ahead log and the automatic two-phase locking interface used to enforce crash and concurrent atomicity in transactions, detailing how the verification framework Perennial can be used to manage assertions about crash behavior across multiple threads. By effectively harnessing concurrency to hide disk access latency, GoTxn enables performance in DaisyNFS similar to the unverified Linux NFS server. |
| first_indexed | 2024-09-23T09:08:16Z |
| format | Thesis |
| id | mit-1721.1/143253 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T09:08:16Z |
| publishDate | 2022 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1432532022-06-16T03:50:58Z GoTxn: Verifying a Crash-Safe, Concurrent Transaction System Theng, Mark Kaashoek, M. Frans Zeldovich, Nickolai Chajed, Tej Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Bugs related to concurrency and crash safety are infamous for being subtle and hard to reproduce. Formal verification provides a way to combat such bugs through the use of machine-checked proofs about program behavior. However, reasoning about concurrency and crashes can be tricky, especially when scaling up to larger systems that must also have good performance. This thesis discusses the verification of GoTxn, the concurrent, crash-safe transaction system underlying the verified Network File System (NFS) server DaisyNFS. It focuses on the specification and proof of the write-ahead log and the automatic two-phase locking interface used to enforce crash and concurrent atomicity in transactions, detailing how the verification framework Perennial can be used to manage assertions about crash behavior across multiple threads. By effectively harnessing concurrency to hide disk access latency, GoTxn enables performance in DaisyNFS similar to the unverified Linux NFS server. M.Eng. 2022-06-15T13:07:30Z 2022-06-15T13:07:30Z 2022-02 2022-02-22T18:32:25.308Z Thesis https://hdl.handle.net/1721.1/143253 In Copyright - Educational Use Permitted Copyright MIT http://rightsstatements.org/page/InC-EDU/1.0/ application/pdf Massachusetts Institute of Technology |
| spellingShingle | Theng, Mark GoTxn: Verifying a Crash-Safe, Concurrent Transaction System |
| title | GoTxn: Verifying a Crash-Safe, Concurrent Transaction System |
| title_full | GoTxn: Verifying a Crash-Safe, Concurrent Transaction System |
| title_fullStr | GoTxn: Verifying a Crash-Safe, Concurrent Transaction System |
| title_full_unstemmed | GoTxn: Verifying a Crash-Safe, Concurrent Transaction System |
| title_short | GoTxn: Verifying a Crash-Safe, Concurrent Transaction System |
| title_sort | gotxn verifying a crash safe concurrent transaction system |
| url | https://hdl.handle.net/1721.1/143253 |
| work_keys_str_mv | AT thengmark gotxnverifyingacrashsafeconcurrenttransactionsystem |