Notice: Function _load_textdomain_just_in_time was called incorrectly. Translation loading for the popup-by-supsystic domain was triggered too early. This is usually an indicator for some code in the plugin or theme running too early. Translations should be loaded at the init action or later. Please see Debugging in WordPress for more information. (This message was added in version 6.7.0.) in /dati/html/wordpress/pros/wp-includes/functions.php on line 6121
Cherry-pi – PROS

Cherry-pi

DOCUMENTS
Rollback Recovery in Session-based Programming

Submitted Manuscript 
Maude sources

For our MAUDE implementation of the cherry-pi type semantics we have used the version 2.7.1 of MAUDE for Mac OS X.

DESCRIPTION

To react to unforeseen circumstances or amend abnormal situations in communication-centric systems, programmers are in charge of “undoing” the interactions which led to an undesired state. To assist this task, session-based languages can be endowed with reversibility mechanisms. In this paper we propose a language enriched with programming facilities to commit session interactions, to roll back the computation to a previous commit point, and to abort the session. Rollbacks in our language always bring the system to previous visited states and that a rollback cannot bring the system back to a point prior to the last commit. Programmers are relieved from the burden of ensuring that a rollback never restores a checkpoint imposed by a session participant different from the rollback requester. Such undesired situations are prevented at design-time (statically) by relying on a decidable compliance check at the type level, implemented in MAUDE. We show that the language satisfies error-freedom and progress of a session.