Name
Abstract | ||
|---|---|---|
The well-known coordinated snapshot algorithm of mutable checkpointing [7,8,9] is studied. We equip it with a concise formal model and analyze its operational behavior via an invariant characterizing the snapshot computation. By this we obtain a clear understanding of the intermediate behavior and a correctness proof of the final snapshot based on a strong notion of consistency (reachability within the partial order representing the underlying computation). The formal model further enables a comparison with the blocking queue algorithm [13] introduced for the same scenario and with the same objective. From a broader perspective, we advocate the use of formal semantics to formulate and prove correctness of distributed algorithms. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-24644-4_12 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
snapshot,checkpointing,consistency,distributed computing | Correctness proofs,Computer science,Snapshot algorithm,Parallel computing,Queue,Theoretical computer science,Reachability,Invariant (mathematics),Snapshot (computer storage),Technical report,Distributed computing,Computation | Conference |
Volume | ISSN | Citations |
9392 | 0302-9743 | 1 |
PageRank | References | Authors |
0.38 | 7 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Deepanker Aggarwal | 1 | 1 | 0.38 |
| A. Kiehn | 2 | 249 | 22.96 |