nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Checkpoint/Rollback vs Causally-Consistent Reversibility

verfasst von : Martin Vassor, Jean-Bernard Stefani

Erschienen in: Reversible Computation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This paper analyzes the relationship between a distributed checkpoint/rollback scheme based on causal logging, called Manetho, and a reversible concurrent model of computation, based on the \(\pi \)-calculus with imperative rollback developed by Lanese et al. in [14]. We show a rather tight relationship between rollback based on causal logging as performed in Manetho and the rollback algorithm underlying the calculus in [14]. Our main result is that the latter can faithfully simulate Manetho, where the notion of simulation we use is that of weak barbed simulation, and that the converse only holds if possible rollbacks in are restricted.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Data Structures and Dynamic Memory Management in Reversible Languages

Nächstes Kapitel : A Typed Functional Reversible Core Language

The description of the Manetho protocol differs slightly between the publication [8] and Elnozahy’s PhD thesis [6]. In particular, the latter involves a coordinating checkpointing scheme, which is not the case in the former. For the sake of simplicity, in this paper we follow the description in [8]. Checkpoint coordination in any case is not necessary for the correct operation of the recovery process in a causal logging checkpoint/rollback scheme. In [6] it is essentially used to simplify the garbage collection of recovery information.

In particular: \(X\{^Y/_X\}\{^Z/_Y\} = Z\) and \(X\{^{Y,Z}/_{X,Y}\} = Y\).

For simplicity, we let this choice be non-deterministic, but we could easily extend the syntax of \(\text{ lr- }\pi {}\) to accommodate e.g. imperative rollback instructions as in [14].

Aggarwal, D., Kiehn, A.: Analyzing mutable checkpointing via invariants. In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 176–190. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24644-4_12CrossRef

Cao, G., Singhal, M.: Checkpointing with mutable checkpoints. Theor. Comput. Sci. 290(2), 1127–1148 (2003)MathSciNetCrossRef

Chothia, T., Duggan, D.: Abstractions for fault-tolerant global computing. Theor. Comput. Sci. 322(3), 567–613 (2004)MathSciNetCrossRef

Cristescu, I., Krivine, J., Varacca, D.: A compositional semantics for the reversible p-calculus. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society (2013)

Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 292–307. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_19CrossRef

Elnozahy, E.N.: Manetho: fault-tolerance in distributed systems using rollback-recovery and process replication. Ph.D. thesis, Rice University, TX, USA (1993)

Elnozahy, E.N., Alvisi, L., Wang, Y.M., Johnson, D.B.: A survey of rollback-recovery protocols in message-passing systems. ACM Comput. Surv. 34(3), 375–408 (2002)CrossRef

Elnozahy, E.N., Zwaenepoel, W.: Manetho: transparent rollback-recovery with low overhead, limited rollback and fast output commit. IEEE Trans. Comput. 41(5), 526–531 (1992)CrossRef

Field, J., Varela, C.A.: Transactors: a programming model for maintaining globally consistent distributed state in unreliable environments. In: 32nd ACM Symposium on the Principles of Programming Languages (POPL). ACM (2005)

10.

Giachino, E., Lanese, I., Mezzina, C.A., Tiezzi, F.: Causal-consistent rollback in a tuple-based language. J. Log. Algebr. Methods Program. 88, 99–120 (2017)MathSciNetCrossRef

11.

Hélary, J.M., Netzer, R.H.B., Raynal, M.: Consistency issues in distributed checkpoints. IEEE Trans. Softw. Eng. 25(2), 274–281 (1999)CrossRef

12.

Lanese, I., Lienhardt, M., Mezzina, C.A., Schmitt, A., Stefani, J.-B.: Concurrent flexible reversibility. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 370–390. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_21CrossRef

13.

Lanese, I., Mezzina, C.A., Stefani, J.-B.: Reversing higher-order pi. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 478–493. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15375-4_33CrossRef

14.

Lanese, I., Mezzina, C.A., Schmitt, A., Stefani, J.-B.: Controlling reversibility in higher-order pi. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 297–311. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23217-6_20CrossRef

15.

Lanese, I., Mezzina, C.A., Stefani, J.-B.: Reversibility in the higher-order \(\pi \)-calculus. Theor. Comput. Sci. 625, 25–84 (2016)MathSciNetCrossRef

16.

Leeman, G.B.: A formal approach to undo operations in programming languages. ACM Trans. Program. Lang. Syst. 8(1), 50–87 (1986)CrossRef

17.

Milner, R., Sangiorgi, D.: Barbed bisimulation. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 685–695. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55719-9_114CrossRef

18.

Nishida, N., Palacios, A., Vidal, G.: A reversible semantics for Erlang. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 259–274. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63139-4_15CrossRef

19.

Perumalla, K.S., Park, A.J.: Reverse computation for rollback-based fault tolerance in large parallel systems - evaluating the potential gains and systems effects. Cluster Comput. 17(2), 303–313 (2014)CrossRef

20.

Vassor, M., Stefani, J.B.: A comparison between stable causal log (Manetho) and a modified roll-pi calculus (2018). https://team.inria.fr/spades/long-version-checkpoint-vs-reversibility/

21.

Ziarek, L., Jagannathan, S.: Lightweight checkpointing for concurrent ML. J. Funct. Program. 20(2), 137–173 (2010)MathSciNetCrossRef

Titel: Checkpoint/Rollback vs Causally-Consistent Reversibility
verfasst von: Martin Vassor
Jean-Bernard Stefani
Verlag: Springer International Publishing
Buch: Reversible Computation
Print ISBN: 978-3-319-99497-0

Electronic ISBN: 978-3-319-99498-7

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-99498-7_20

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner