Loading...
Please wait, while we are loading the content...
Similar Documents
Analyzing mutable checkpointing via invariants
| Content Provider | Indraprastha Institute of Information Technology, Delhi |
|---|---|
| Author | Aggarwal, Deepanker Kiehn, Astrid |
| Abstract | The well-known coordinated snapshot algorithm of mutable checkpointing [7{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 fi nal 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. |
| File Format | |
| Language | English |
| Access Restriction | Open |
| Subject Keyword | Snapshot Checkpointing Consistency Distributed computing |
| Content Type | Text |
| Resource Type | Technical Report |
| Subject | Data processing & computer science |
