Skip to Main content Skip to Navigation
Reports

A Fault Tolerance protocol for ASP calculus: Design and Proof

Françoise Baude 1 Denis Caromel 1 Christian Delbé 1 Ludovic Henrio 1
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : This research report first details a communication induced checkpointing fault tolerance protocol adapted to ProActive, a Java library that implements the ASP model. This model is based n a request/reply mechanism. In order to prove the correctness of this protocol, we introduce a local partial order between events occurring on a given process. This order is extended into a global order by the Lamport's happened-before relation. Finally, we prove that from a cut that is ''consistent enough'', a second execution is constrained to go equivalently to the first one until a consistent global state of the first one (the history closure). Thus, the protocol described in this report ensures that, even from a inconsistent recovery line, a reexecution cannot lead to an inconsistent state that could not exist in a normal execution.
Document type :
Reports
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00070752
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 9:30:39 PM
Last modification on : Monday, October 12, 2020 - 10:30:26 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:05:56 PM

Identifiers

  • HAL Id : inria-00070752, version 1

Collections

Citation

Françoise Baude, Denis Caromel, Christian Delbé, Ludovic Henrio. A Fault Tolerance protocol for ASP calculus: Design and Proof. [Research Report] RR-5246, INRIA. 2004, pp.37. ⟨inria-00070752⟩

Share

Metrics

Record views

312

Files downloads

368