Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Analyzing Mutable Checkpointing via Invariants

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, January 26, 2017 - 10:43:27 AM
Last modification on : Tuesday, September 15, 2020 - 4:34:02 PM
Long-term archiving on: : Thursday, April 27, 2017 - 2:55:28 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Deepanker Aggarwal, Astrid Kiehn. Analyzing Mutable Checkpointing via Invariants. 6th Fundamentals of Software Engineering (FSEN), Apr 2015, Tehran, Iran. pp.176-190, ⟨10.1007/978-3-319-24644-4_12⟩. ⟨hal-01446599⟩



Record views


Files downloads