%0 Conference Proceedings
%T Analyzing Mutable Checkpointing via Invariants
%+ Indraprastha Institute of Information Technology [New Delhi] (IIIT-Delhi)
%A Aggarwal, Deepanker
%A Kiehn, Astrid
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 6th Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Mehdi Dastani
%Y Marjan Sirjani
%I Springer
%3 Fundamentals of Software Engineering
%V LNCS-9392
%P 176-190
%8 2015-04-22
%D 2015
%R 10.1007/978-3-319-24644-4_12
%K snapshot
%K checkpointing
%K consistency
%K distributed computing
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-01446599/document
%2 https://inria.hal.science/hal-01446599/file/978-3-319-24644-4_12_Chapter.pdf
%L hal-01446599
%U https://inria.hal.science/hal-01446599
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-LNCS-9392
%~ IFIP-FSEN