Name
Abstract | ||
|---|---|---|
This paper describes ShadowDB, a replicated version of the BerkeleyDB database. ShadowDB is a primary-backup based replication protocol where failure handling, the critical part of the protocol, is taken care of by a synthesized consensus service that is correct by construction. The service has been proven correct semiautomatically by the Nuprl proof assistant. We describe the design and process to prove the consensus protocol correct and present the database replication protocol. The performance of ShadowDB is good in the normal case and recovering from a failure only takes seconds. Our approach offers simplified means to diversify the code in a way that preserves correctness. |
Year | Venue | Keywords |
|---|---|---|
2012 | HotDep | database replication protocol,consensus protocol,nuprl proof assistant,replication protocol,synthesized consensus service,correct semiautomatically,critical part,synthesized consensus core,failure handling,berkeleydb database,normal case |
Field | DocType | Citations |
Replication (computing),Computer science,Nuprl,Correctness,Database,Proof assistant | Conference | 5 |
PageRank | References | Authors |
0.44 | 13 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nicolas Schiper | 1 | 173 | 10.18 |
| Vincent Rahli | 2 | 43 | 9.21 |
| Robbert van Renesse | 3 | 4018 | 507.30 |
| M. Bickford | 4 | 101 | 8.60 |
| Robert L. Constable | 5 | 778 | 242.51 |