In recent years, reversibility in concurrent settings has attracted interest thanks to its diverse applications in areas such as error recovery, debugging, and biological modeling. Also, it has been studied in many formalisms, including Petri nets, process algebras, and programming languages like Erlang. However, most attempts made so far suffer from the same limitation: they define the reversible semantics in an ad-hoc fashion. To address this limit, Lanese et al. have recently proposed a novel general method to derive a concurrent reversible semantics from a non-reversible one. However, in most interesting instances the method relies on infinite sets of reductions, making doubtful its practical applicability. We bridge the gap between theory and practice by implementing the above method in Maude. The key insight is that infinite sets of reductions can be captured by a small number of schemas in many relevant cases. This happens indeed for our application: the functional and concurrent fragment of Erlang. We extend the framework with a general rollback operator, allowing one to undo an action far in the past, including all and only its consequences. We can thus use our tool, e.g., as an oracle against which to test the reversible debugger CauDEr for Erlang, or as an executable specification for new reversible debuggers.
Generation of a Reversible Semantics for Erlang in Maude / Fabbretti G.; Lanese I.; Stefani J.-B.. - STAMPA. - 13478:(2022), pp. 106-122. (Intervento presentato al convegno 23rd International Conference on Formal Engineering Methods, ICFEM 2022 tenutosi a esp nel 2022) [10.1007/978-3-031-17244-1_7].
Generation of a Reversible Semantics for Erlang in Maude
Lanese I.;
2022
Abstract
In recent years, reversibility in concurrent settings has attracted interest thanks to its diverse applications in areas such as error recovery, debugging, and biological modeling. Also, it has been studied in many formalisms, including Petri nets, process algebras, and programming languages like Erlang. However, most attempts made so far suffer from the same limitation: they define the reversible semantics in an ad-hoc fashion. To address this limit, Lanese et al. have recently proposed a novel general method to derive a concurrent reversible semantics from a non-reversible one. However, in most interesting instances the method relies on infinite sets of reductions, making doubtful its practical applicability. We bridge the gap between theory and practice by implementing the above method in Maude. The key insight is that infinite sets of reductions can be captured by a small number of schemas in many relevant cases. This happens indeed for our application: the functional and concurrent fragment of Erlang. We extend the framework with a general rollback operator, allowing one to undo an action far in the past, including all and only its consequences. We can thus use our tool, e.g., as an oracle against which to test the reversible debugger CauDEr for Erlang, or as an executable specification for new reversible debuggers.File | Dimensione | Formato | |
---|---|---|---|
icfem.pdf
Open Access dal 11/10/2023
Tipo:
Postprint
Licenza:
Licenza per accesso libero gratuito
Dimensione
511.88 kB
Formato
Adobe PDF
|
511.88 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.