×

Causal-consistent rollback in a tuple-based language. (English) Zbl 1362.68213

Summary: Rollback is a fundamental technique for ensuring reliability of systems, allowing one, in case of troubles, to recover a past system state. However, the definition of rollback in a concurrent/distributed scenario is quite tricky. We propose an approach based on the notion of causal-consistent reversibility: any given past action can be undone, provided that all the actions caused by it are undone as well. Given that, we define a rollback as the minimal causal-consistent sequence of backward steps able to undo a given action. We define the semantics of such a rollback operator, and show that it satisfies the above specification. The approach that we present is quite general, but we instantiate it in the case of \(\mu\)Klaim, a formal coordination language based on distributed tuple spaces. We remark that this is the first definition of causal-consistent rollback in a shared-memory setting. We illustrate the use of rollback in \(\mu\)Klaim on a simple, but realistic, application scenario.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Elnozahy, E. N.M.; 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)
[2] Apple, Time Machine (OS X)
[3] Bernstein, P. A.; Hadzilacos, V.; Goodman, N., Concurrency Control and Recovery in Database Systems (1987), Addison-Wesley
[4] Randell, B., System structure for software fault tolerance, IEEE Trans. Softw. Eng., 1, 2, 220-232 (1975)
[5] Danos, V.; Krivine, J., Reversible communicating systems, (Gardner, P.; Yoshida, N., CONCUR 2004. CONCUR 2004, Lecture Notes in Computer Science, vol. 3170 (2004), Springer), 292-307 · Zbl 1099.68066
[6] Gorla, D.; Pugliese, R., Resource access and mobility control with dynamic privileges acquisition, (Baeten, J. C.M.; Lenstra, J. K.; Parrow, J.; Woeginger, G. J., ICALP. ICALP, Lecture Notes in Computer Science, vol. 2719 (2003), Springer), 119-132 · Zbl 1039.68542
[7] Giachino, E.; Lanese, I.; Mezzina, C. A.; Tiezzi, F., Causal-consistent reversibility in a tuple-based language, (Daneshtalab, M.; Aldinucci, M.; Leppänen, V.; Lilius, J.; Brorsson, M., PDP (2015), IEEE), 467-475
[8] De Nicola, R.; Ferrari, G.; Pugliese, R., KLAIM: a kernel language for agents interaction and mobility, IEEE Trans. Softw. Eng., 24, 5, 315-330 (1998)
[9] Gelernter, D., Generative communication in Linda, ACM Trans. Program. Lang. Syst., 7, 1, 80-112 (1985) · Zbl 0559.68030
[10] Bettini, L.; Bono, V.; De Nicola, R.; Ferrari, G. L.; Gorla, D.; Loreti, M.; Moggi, E.; Pugliese, R.; Tuosto, E.; Venneri, B., The KLAIM project: theory and practice, (Priami, C., Global Computing. Global Computing, Lecture Notes in Computer Science, vol. 2874 (2003), Springer), 88-150 · Zbl 1179.68027
[11] Lanese, I.; Mezzina, C. A.; Stefani, J.-B., Reversing higher-order pi, (Gastin, P.; Laroussinie, F., CONCUR 2010. CONCUR 2010, Lecture Notes in Computer Science, vol. 6269 (2010), Springer), 478-493 · Zbl 1287.68137
[12] Phillips, I.; Ulidowski, I., Reversing algebraic process calculi, J. Log. Algebraic Program., 73, 1-2, 70-96 (2007) · Zbl 1123.68065
[13] Cristescu, I. D.; Krivine, J.; Varacca, D., A compositional semantics for the reversible pi-calculus, (LICS (2013), IEEE Press), 388-397 · Zbl 1366.68201
[14] Lienhardt, M.; Lanese, I.; Mezzina, C. A.; Stefani, J.-B., A reversible abstract machine and its space overhead, (Giese, H.; Rosu, G., FMOODS/FORTE. FMOODS/FORTE, Lecture Notes in Computer Science, vol. 7273 (2012), Springer), 1-17
[15] Lanese, I.; Mezzina, C. A.; Stefani, J.-B., Reversibility in the higher-order \(π\)-calculus, Theor. Comput. Sci., 625, 25-84 (2016) · Zbl 1338.68078
[16] Prabhu, P.; Ramalingam, G.; Vaswani, K., Safe programmable speculative parallelism, (Zorn, B. G.; Aiken, A., PLDI (2010), ACM), 50-61
[17] Barnes, P. D.; Carothers, C. D.; Jefferson, D. R.; LaPre, J. M., Warp speed: executing time warp on 1,966,080 cores, (Loper, M. L.; Wainer, G. A., SIGSIM-PADS (2013), ACM), 327-336
[18] Lanese, I.; Lienhardt, M.; Mezzina, C. A.; Schmitt, A.; Stefani, J.-B., Concurrent flexible reversibility, (Felleisen, M.; Gardner, P., ESOP. ESOP, Lecture Notes in Computer Science, vol. 7792 (2013), Springer), 370-390 · Zbl 1381.68210
[19] Lanese, I.; Mezzina, C. A.; Schmitt, A.; Stefani, J.-B., Controlling reversibility in higher-order pi, (Katoen, J.; König, B., CONCUR 2011. CONCUR 2011, Lecture Notes in Computer Science, vol. 6901 (2011), Springer), 297-311 · Zbl 1344.68168
[20] Avizienis, A.; Laprie, J.-C.; Randell, B.; Landwehr, C. E., Basic concepts and taxonomy of dependable and secure computing, IEEE Trans. Dependable Secure Comput., 1, 1, 11-33 (2004)
[21] Chothia, T.; Duggan, D., Abstractions for fault-tolerant global computing, Theor. Comput. Sci., 322, 3, 567-613 (2004) · Zbl 1071.68010
[22] Field, J.; Varela, C. A., Transactors: a programming model for maintaining globally consistent distributed state in unreliable environments, (Palsberg, J.; Abadi, M., POPL (2005), ACM), 195-208 · Zbl 1369.68134
[23] Ziarek, L.; Jagannathan, S., Lightweight checkpointing for concurrent ML, J. Funct. Program., 20, 2, 137-173 (2010) · Zbl 1214.68122
[24] Leeman, G., A formal approach to undo operations in programming languages, ACM Trans. Program. Lang. Syst., 8, 1, 50-87 (1986) · Zbl 0592.68015
[25] Danos, V.; Regnier, L., Reversible, irreversible and optimal lambda-machines, Theor. Comput. Sci., 227, 1-2, 79-97 (1999) · Zbl 0952.03008
[26] Bishop, P. G., Using reversible computing to achieve fail-safety, (ISSRE (1997), IEEE Computer Society), 182-191
[27] Danos, V.; Krivine, J., Transactions in RCCS, (Abadi, M.; de Alfaro, L., CONCUR 2005. CONCUR 2005, Lecture Notes in Computer Science, vol. 3653 (2005), Springer), 398-412 · Zbl 1134.68432
[28] Bacci, G.; Danos, V.; Kammar, O., On the statistical thermodynamics of reversible communicating processes, (Corradini, A.; Klin, B.; Cîrstea, C., CALCO 2011. CALCO 2011, Lecture Notes in Computer Science, vol. 6859 (2011), Springer), 1-18 · Zbl 1344.68160
[29] Phillips, I.; Ulidowski, I.; Yuen, S., A reversible process calculus and the modelling of the ERK signalling pathway, (Glück, R.; Yokoyama, T., Reversible Computation. Reversible Computation, Lecture Notes in Computer Science, vol. 7581 (2012), Springer), 218-232 · Zbl 1451.68124
[30] Kuhn, S.; Ulidowski, I., Towards modelling of local reversibility, (Krivine, J.; Stefani, J.-B., Reversible Computation. Reversible Computation, Lecture Notes in Computer Science, vol. 9138 (2015), Springer), 279-284 · Zbl 1464.68113
[31] Lanese, I.; Mezzina, C. A.; Tiezzi, F., Causal-consistent reversibility, Bull. Eur. Assoc. Theor. Comput. Sci., 114, 121-139 (2014) · Zbl 1409.68117
[32] Bettini, L.; De Nicola, R.; Pugliese, R., Klava: a Java package for distributed and mobile applications, Softw. Pract. Exp., 32, 14, 1365-1394 (2002) · Zbl 1009.68933
[33] Engblom, J., A review of reverse debugging, (System, Software, SoC and Silicon Debug (2012), IEEE), 1-6
[34] Giachino, E.; Lanese, I.; Mezzina, C. A., Causal-consistent reversible debugging, (Gnesi, S.; Rensink, A., FASE. FASE, Lecture Notes in Computer Science, vol. 8411 (2014), Springer), 370-384
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.