Towards parametric causal semantics in π-calculus ? Doriana Medić and Claudio Antares Mezzina IMT School for Advanced Studies Lucca, Italy Abstract. In a concurrent setting, causally-consistent reversibility re- lates causality and reversibility. In this note we overview three causal semantics for π-calculus: two classical and a recent one used for a re- versible variant of π-calculus. We show the differences between them via examples, and discuss how to revise the classical one in order to be used as the underlying machinery for a reversible calculus. We propose a rein- terpretation of such notions in particular when it comes to silent actions and names extrusion. Our ultimate goal is to devise a general reversible framework parametric into the underlying notion of causality. 1 Introduction A reversible system is capable of executing both in the forward (normal) direction and in the backward one. In a sequential setting, executing backwards is quite straightforward since there exists only one execution order. In a concurrent sys- tem, things are more complex as there exist no clear notion of last action: indeed, several independent processes may execute concurrently. Causally-consistent re- versibility [7] relates causality and reversibility of a concurrent system in the following way: an action can be reverted provided all its consequences have been reverted. In Milner’s CCS, there exists just one notion of causality: the so-called struc- tural which is imposed by the prefixing ‘.’ operator and by synchronizations. An evidence of this is that the two reversible variants of CCS, RCCS [4] and CCSK [9] are shown to be equivalent [8]. When moving to more expressive cal- culi with name creation and passing like π-calculus things are more complex, since there exist different notions of causality as witnessed by the plethora of causal semantics for π-calculus [2, 5, 1] (just to cite a few of them). In π-calculus, structural causality is determined by the nesting of the prefixes; for example, in process ba.ce the output on channel c structurally depends on the output on b. Extruding (or opening) a name generates an object dependency; for example, in process νa (ba | a(z)) the input action on a depends on the output on b. Sending a bound name to the context will make all the successive actions using that name dependent on the extruder. There exist different interpretations on how the first extrusion of a name causes the processes using it. In this short note we ? Partially supported by EU COST IC1405 (Reversible Computation - Extending Horizons of Computing). will consider the causal semantics introduced by Boreale and Sangiorgi [1], by Degano and Priami [5] and by Cristescu, Krivine and Varacca [2]; and we will dis- cuss on how these notions generate different interpretations of backward moves especially when considering silent actions. Our goal is to devise a reversible cal- culus parametric with respect the underlying causal semantics, in order to better compare them. 2 Causal semantics by example Processes in π-calculus are derived from the following syntax: P, Q ::= 0 | π.P | P | Q | νa(P ) π ::= bc | b(a) | τ A process can be inactive 0, a prefixed process π.P , the parallel composition P | Q and the restriction of a name νa(P ) meaning that the channel name a is only known in process P . A prefix π denotes the output, input and the silent action, respectively. The semantics of π-calculus is expressed via an LTS and the generated actions/labels are µ ::= bc | b(a) | bhνai | τ , where bhνai represents sending of a bound name a. Let us consider the π process P = νa (ba | ca | a(z)), ba ca a(∗) where the actions are executed in following order: P −→−→−−→ P 0 and ∗ stands for either y or z depending on whether the considered semantics is a late (∗ = z) or an early (∗ = y) one. We now show how the different causal semantics behave. Boreale et al. Causal information is added to the syntax and semantics of π- calculus in order to track down subject dependencies. Causal processes are of the form K :: P , where the cause-set K contains all the causes of the process P . Every visible action is associated with a unique cause k. The τ actions are not observable and do not exhibit causes. The set of the previous causes is noted by K and in our example it is ∅. Object dependencies can be observed in the labels of the transitions, by looking at the process trace/run. In our example: bhνai ca a(y) P −−−→ k1 :: 0 | ca | a(z) − −−→ k1 :: 0 | k2 :: 0 | a(z) −−−→ k1 :: 0 | k2 :: 0 | k3 :: 0 ∅;k1 ∅;k2 ∅;k3 According to [1], the extrusion (the first action) causes every following action in which a is a free name. This implies that both of the actions ca and a(y) are caused by bhνai. Hence bhνai cannot be undone unless ca and a(y) are undone. To be able to capture this behaviour we need to be sure that action bhνai is the last one to be undone, the other two can be undone in any order. Degano et al. The authors keep track of the structural dependence by specifying which component of the process is performing a move. To uniquely identify the actions, they use labels of the form ϑµ and ϑhk0 ϑ0 µ0 , k1 ϑ1 µ1 i where ϑ ∈ {k0 , k1 }∗ represents the position of the (sub-)process making the action, and µ0 = b(x) iff µ1 is either ba or bhνai, or vice versa. The tag k0 (k1 ) is used to record that the left (right) component in the process is moving. The object (link) dependency can be observed by looking at the process run. In our example: k0 k0 bhνai k0 k1 ca k1 a(z) P −−−−−−→ 0 | ca | a(z) −−−−→ 0 | 0 | a(z) −−−−→ 0 | 0 | 0 The extrusion bhνai causes every following action that has the name a in the subject position. In this way, the input a(z) is caused by the first action. The output ca is neither object dependent on the extrusion, nor concurrent with it. To order these kind of actions, the authors introduced the notion of temporal precedence (structural and object). In this way, action bhνai has object prece- dence over action ca even if they are not causally dependent. From the reversible point of view this notion of causality is similar to [1]. Cristescu et al. A compositional semantics for the reversible π-calculus is in- troduced in [2]. The information about the past actions are kept into a memory added to every process. A term of the form m . P represents the reversible pro- cess, where memory m is a stack of events and P is process. A memory1 event hi, k, αi contains the identifier i, the contextual cause k and executed action α, respectively. If the action does not have a cause, it is noted with ∗. The indexed restriction νaΓ behaves as the classical restriction when Γ = ∅, otherwise it is used to keep track of the past scope of the variable. The process that we get from P after the execution of the first two actions is: νai,h (hi, ∗, bai . 0 | hh, ∗, cai . 0 | a(z)) The outputs ba and ca are associated with the identifiers i and h, respectively. Since these two actions were sending the bound name a to the context, their identifiers are recorded into the process νai,h . According to the semantics, these two actions are meant to be executed concurrently and both of them can be seen as the extrusion of the name a. Hence, the input action a(z) can choose its cause between i and h, according to the context. For example, by choosing h, we will get the process: νai,h (hi, ∗, bai . 0 | hh, ∗, cai . 0 | hl, h, a[∗/z]i . 0) Since in the memory hl, h, a[∗/z]i, h is saved as a cause of the action l, that force us to undo the action a(z) before the extrusion ca. The other extrusion (ba) can be reversed at any time. 2.1 Causalities and silent actions The semantics introduced in [1, 5] lose information about object dependence when it comes to consider silent actions. Let us consider the process P = νa (ba | ca | a(z)) with a context b(x).xy | c(w) and see what happens. Boreale et al. By adding a context to the example, all the executed actions will become silent. Since after a synchronization the causes of the two synchronizing processes are merged, and no new causes are created, in order to keep track of them we need to give to processes initial and unique causes. We have: τ νa (k1 :: ba | k2 :: ca | k3 :: a(z)) | k4 :: b(x).xy | k5 :: c(w) − → τ νa ({k1 , k4 } :: 0 | k2 :: ca | k3 :: a(z) | {k1 , k4 } :: ay) | k5 :: c(w) − → τ νa ({k1 , k4 } :: 0 | {k2 , k5 } :: 0 | k3 :: a(z) | {k1 , k4 } :: ay | {k2 , k5 } :: 0) − → νa ({k1 , k4 } :: 0 | {k2 , k5 } :: 0 | {k3 , k1 , k4 } :: 0 | {k1 , k4 , k3 } :: 0 | {k2 , k5 } :: 0)) 1 For the sake of simplicity we are simplifying the information contained into the memory m. We refer to [2] for more details on memories. We can notice that the (silent) actions are no longer object-dependent (as the example of the previous section). The third τ action is structurally dependent on the first one and we can detect it in the set of the causes {k1 , k4 , k3 }. If instead of imposing unique causes ki to the initial processes, we were to use ∅ (as prescribed by the silent actions) we were unable to observe this fact. In [6], authors proved that the causal information used to support reversibility in ρπ is consistent with this notion of causality, if a reduction semantics is considered. Degano et al. The object dependence after the communication is not needed because through the rule Close the object is localised to the rest of the com- municating processes via νa. Hence these three silent actions are not object dependent. The computation with a context will look like: hk0 k0 k0 bhνai,k1 k0 b(a)i hk0 k0 k1 chνai,k1 k1 c(a)i P | b(x).xy | c(w) −−−−−−−−−−−−−−−→ νa (0 | ca | a(z) | ay) | c(w) −−−−−−−−−−−−−−−→ hk0 k1 a(z),k1 k0 ayi νa (0 | 0 | a(z) | ay | 0) −−−−−−−−−−−−→ νa (0 | 0 | 0 | 0 | 0) From the structural point of view the third action is depending on the first one and we can notice it in the labels. Output k1 k0 ay has a prefix in the first label. Cristescu et al. After the two synchronizations on the channel b and c, we will get the process: νa∅ (νah (νai,h (hi, ∗, bai . 0 | hh, ∗, cai . 0 | a(z)) | hi, ∗, b[a/x]i . xy) | hh, ∗, c[a/w]i . 0) According to the authors, processes a(z) and hi, ∗, b[a/x]i.xy can communicate2 only if the instantiator of the action xy is equal to the cause of the action a(z). Since action i instantiates the name x with the name a, the cause of the input action on the channel a is k = i. Considering the silent actions, the causal order does not change, as one property of their causal semantics is that object causality correspond to the subject one. 2.2 Silently regaining information From these examples we can notice the change in the dependences between the visible actions and the silent ones. When considering just τ actions in [1, 5], there is no object dependency among actions; they are considered as concurrent events. Moreover, information on extruders is lost. To be able to use these causal semantics for a reversible calculus we need to keep track of which process did the extrusion and to record where the binder was before. Moreover, also silent actions have to bring the same causal information as their visible counterpart. But when considering these modified semantics we will have that in the struc- turally equivalent processes, the same actions have different causal order. If we consider our example we will have that Q = νa (ba | ca | a(z)) | b(x).xy | c(w), Q0 = νa( (ba | ca | a(z)) | b(x).xy | c(w)) with Q ≡ Q0 , we will have that if τ b τc Q −→ −→ executes the synchronization on b and then on c these two silent actions τb τc will be object dependent, while in Q0 −→ −→ the two actions are concurrent. This 2 Memory m is used as a variables store, hence variable x is evaluated into a. is not the case of [2] since this semantics enjoys some correctness criteria [3] (one of which is that causality is preserved via structural congruence) that the other two semantics do not. 3 Conclusions and future work We reviewed three notions of causality for π-calculus, two non reversible [1, 5] and one reversible [2], and we showed the differences among them. From the reversible perspective we pointed out the difficulties while using semantics [1, 5] and proposed a reinterpretation of them in particular when it comes to con- sider silent actions. More in details, information about the extruder have to be maintained, in order to bring back the binder while reverting a bound action. It seems that different data structures can be used to maintain such information; indeed, [2] uses a set while in [1, 5] since the first extruder causes the other an in- dexed set should be the ideal data structure. Different data structures will induce a different notion of causality. Currently we are working on developing a general framework for reversible π-calculi parametric with respect to the data structure used to save extruders information. Then, depending on the underlying data structure used to instantiate the framework, we could obtain different causal semantics. In this way, once we are able to capture the two known reversible variants of π-calculus [6, 2], it will be simpler to compare them. Acknowledgments We are grateful to Daniele Varacca for his useful remarks and suggestions which led to substantial improvements. Furthermore, we thanks Jorge A. Pérez for his comments on a preliminary version of this document. References 1. M. Boreale and D. Sangiorgi. A fully abstract semantics for causality in the π- calculus. Acta Inf., 35(5):353–400, 1998. 2. I. Cristescu, J. Krivine, and D. Varacca. A compositional semantics for the reversible π-calculus. In LICS 2013, pages 388–397, 2013. 3. I. D. Cristescu, J. Krivine, and D. Varacca. Rigid families for CCS and the π- calculus. In ICTAC 2015, volume 9399 of LNCS, pages 223–240. Springer, 2015. 4. V. Danos and J. Krivine. Reversible communicating systems. In CONCUR 2004, volume 3170 of LNCS, pages 292–307. Springer, 2004. 5. P. Degano and C. Priami. Non-interleaving semantics for mobile processes. Theor. Comput. Sci., 216(1-2):237–270, 1999. 6. I. Lanese, C. A. Mezzina, and J. Stefani. Reversibility in the higher-order π-calculus. Theor. Comput. Sci., 625:25–84, 2016. 7. I. Lanese, C. A. Mezzina, and F. Tiezzi. Causal-consistent reversibility. Bulletin of the EATCS, 114, 2014. 8. D. Medic and C. A. Mezzina. Static VS dynamic reversibility in CCS. In RC 2016, pages 36–51, 2016. 9. I. C. C. Phillips and I. Ulidowski. Reversing algebraic process calculi. J. Log. Algebr. Program., 73(1-2):70–96, 2007.