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

https://hal.inria.fr/hal-01446599
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

File

978-3-319-24644-4_12_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

55

Files downloads

81