On the expressive power of synchronization primitives in the -calculuscalculus Catuscia Palamidessi, INRIA Saclay, France 14 October 2009 BASICS'09, Shanghai 1 Focus on the -calculuscalculus Contents The -calculuscalculus with mixed choice () Expressive power of the -calculuscalculus and problems with its fully distributed implementation The asynchronous -calculuscalculus (a) The hierarchy Towards a randomized fully distributed implementation of The probabilistic asynchronous -calculuscalculus (pa) Encoding into pa using a generalized dining

cryptographers algorithm 14 October 2009 BASICS'09, Shanghai 2 The -calculuscalculus Proposed by [Milner, Parrow, Walker 92] as a formal language to reason about concurrent systems Concurrent: several processes running in parallel Asynchronous cooperation: every process proceeds at its own speed Synchronous communication: handshaking, input and output prefix Mixed guarded choice: input and output guards like in CSP and CCS. The implementation of guarded choice is aka the binary interaction problem Dynamic generation of communication channels Scope extrusion: a channel name can be communicated and its scope

extended to include the recipient Q z z x P 14 October 2009 y z R BASICS'09, Shanghai 3 : the -calculuscalculus with mixed choice Syntax gg::= ::= x(y) |x(y) x y | | x^yprefixes(input,output,silent) | prefixes (input, output, silent) P ::= P g .P ::= i

i choice | | | P|P (x)P i mixed guarded choice i gi . Pi mixed guarded parallel operator P | P parallel new name | (x) P new name | | recrec recursion AP P recursion A || A process name A procedure

name 14 October 2009 BASICS'09, Shanghai 4 Operational semantics Transition system Transition system P a -calculusa Q P Q Rules Rules Choice Choice i gi . Pi g .P i i gi

gi Pi P P -calculusx^y P xy ___________________ (y) P -calculusx^(y) P i Open Open 14 October 2009 P P x (y ) (y)P P BASICS'09, Shanghai xy 5 Operational semantics Rules (continued) Rules (continued) Com Com Q -calculusx^z Q x(y ) P -calculusx(y) P P ________________________ P Q x z Q P | Q P [z /Py]| |QQ-calculus P [z/y] | Q

P Close Close Par x(y ) P -calculusx(y) x (z)P Q -calculusx^(z) Q _________________________ P Q Q P | Q (z)( PP || QQ) -calculus (z) (P [z/y] g P -calculusg P P _________________ P g disjoint |Q P | Q P Q | P -calculusg Q | P Par

14 October 2009 | Q) f(Q), b(g) fn(Q) bn(g) = BASICS'09, Shanghai 6 Features which make very expressive -calculus and cause difficulty in its distributed implementation (Mixed) Guarded choice Symmetric solution to certain distributed problems involving distributed agreement Link mobility Network reconfiguration It allows expressing HO (e.g. calculus) in a natural way In combination with guarded choice, it allows solving more distributed problems than those solvable by guarded choice alone

14 October 2009 BASICS'09, Shanghai 7 The expressive power of Example of distributed agreement: The leader election problem in a symmetric network Two symmetric processes must elect one of them as the leader In a finite amount of time The two processes must agree y P Q x A symmetric and fully distributed solution using guarded choice x.Pwins + y^.Ploses | y.Qwins + x^.Qloses Pwins | Qlooses x.Pwins + y .Plooses | y.Qwins + x .Qlooses Ploses | Qwins Pwins | Qloses

Plooses | Qwins 14 October 2009 BASICS'09, Shanghai 8 Example of a network where the leader election problem cannot be solved by guarded choice alone For the following network there is no (fully distributed and symmetric) solution in CCS, or in CSP 14 October 2009 BASICS'09, Shanghai 9 A solution to the leader election problem in looser winner winner looser looser 14 October 2009 BASICS'09, Shanghai 10

Approaches to the implementation of guarded choice in literature [Parrow and Sjodin 92], [Knabe 93], [Tsai and Bagrodia 94]: asymmetric solution based on introducing an order on processes Other asymmetric solutions based on differentiating the initial state Plenty of centralized solutions [Joung and Smolka 98] proposed a randomized solution to the multiway interaction problem, but it works only under an assumption of partial synchrony among processes In this talk we propose an implementation fully distributed, symmetric, and using no synchronous hypotheses. 14 October 2009 BASICS'09, Shanghai 11 State of the art in

Formalisms able to express distributed agreement are difficult to implement in a distributed fashion For this reason, the field has evolved towards variants of which retain mobility, but have no guarded choice One example of such variant is the asynchronous calculus proposed by [Honda-calculusTokoro91, Boudol, 92] (Asynchronous = Asynchronous communication) 14 October 2009 BASICS'09, Shanghai 12 a : the Asynchonous Version of [Amadio, Castellani, Sangiorgi 97] Syntax Syntax g ::= x(y) | g ::=

prefixes (input,silent) x(y) | prefixes P P::= ::= choice gi .Pii input gi .guarded Pi input choice guarded i | xy output action | x^y output action | |P | Q P |parallel P parallel | | (x) new name (x)P P new name | recA P recursion | rec A P recursion

| A procedure name | 14 October 2009 A process identifier BASICS'09, Shanghai 13 Characteristics of a Asynchronous communication: we cant write a continuation after an output, i.e. no x^y.P, but only x^y | P so P will proceed without waiting for the actual delivery of the message Input-calculusguarded choice: only input prefixes are allowed in a choice. Note: the original asynchronous calculus did not contain a choice construct. However the version presented here was shown by [Nestmann and Pierce, 96] to be equivalent to the original asynchronous calculus

It can be implemented in a fully distributed fashion (see for instance Oderskys groups project PiLib) 14 October 2009 BASICS'09, Shanghai 14 The hierarchy We can relate the various sublanguages of by using encodings [ [ ] ] : L L Preserving certain observable properties of runs. Here we will consider as observable properties the presence/absence of certain actions. Existence of such encoding represented by 14 October 2009 L L BASICS'09, Shanghai 15 The hierarchy

mixed choice Value-calculuspassing CCS Internal mobility Separate choice Input guarded choice output prefix asynchronous 14 October 2009 BASICS'09, Shanghai 16 The hierarchy mixed choice Internal mobility Palamidessi Value-calculuspassing CCS Separate choice Input guarded choice Nestmann output prefix asynchronous 14 October 2009 BASICS'09, Shanghai

17 Separation result 1 It is not possible to encode mixed-calculus choice into separate-calculuschoice Homomorphically wrt [|: [ P | Q]] = [[ P ]] | [[Q]] Preserving 2 distinct observable actions This result is based on a sort of confluence property, which holds for the separate-calculuschoice and not for the separate-calculuschoice The proof proceeds by showing that the separate-calculuschoice cannot solve the leader election problem for 2 nodes 14 October 2009 BASICS'09, Shanghai 18 Separation result 2 It is not possible to encode mixed-calculus choice into value-calculuspassing ccs or with internal mobil.

[[ P | Q]] = [[ P ]] | [[Q]] Homomorphically wrt |: Without introducing extra channels Preserving 2 distinct observable actions The proof proceeds by showing that the separate-calculuschoice cannot solve the leader election problem for certain kinds of graphs 14 October 2009 BASICS'09, Shanghai 19 Towards a fully distributed implementation of The results of previous pages show that a fully distributed implementation of must necessarily be randomized A two-calculussteps approach: [[ ]]

probabilistic asynchronous << >> distributed machine 14 October 2009 BASICS'09, Shanghai Advantages: the correctness proof is easier since [[ ]] (which is the difficult part of the implementation ) is between two similar 20 pa: the Probabilistic Asynchonous Syntax | (input,silent) prefixes gg::= ::= x(y) | x(y) prefixes i pi gi input . Piguarded choice pr. inp. P ::=P ::= pi gi .Pi probabilistic pi = 1 i i guard.

choice i pi = 1 | xy output action | x^y output action | P |Q parallel | P |new P nameparallel | (x)P || P new recursion name rec (x) P A || recA AP recursion process identifier | 14 October 2009 A procedure name BASICS'09, Shanghai 21 The operational semantics of pa Based on the Probabilistic Automata of Segala and Lynch

Distinction between nondeterministic behavior (choice of the scheduler) and probabilistic behavior (choice of the process) 1/2 1/2 1/3 1/3 14 October 2009 1/3 1/3 Scheduling Policy: The scheduler chooses the group of transitions Execution: 2/3 BASICS'09, The process chooses probabilistically the transition within the

Shanghai group 22 The operational semantics of pa Representation of a group of transitions Representation of a group of gi transition P{ p P } i i i P { -calculus-calculusgi-calculus> pi Pi } i Rules Rules Choice ( pi gi .Pi ){ pi Pi }i

Choice gi i i pi gi . Pi {-calculus-calculusgi-calculus> pi Pi }i g P {-calculus-calculusgi-calculus> piPP{ i }i i p P } i i i Par Par ____________________ gi p P | Q} i i i Q |(PP | Q){ {-calculus-calculusg i-calculus > p Q | P } i i i 14 October 2009 BASICS'09, Shanghai

23 The operational semantics of pa Rules (continued) P {-calculus-calculusxi(yi)-calculus> Com P |x yQ{ {-calculus -calculus -calculus>1 Nil} piPi[z/yi] | Q }xi=x U Pi | Q }xi=/=x 1 Q }i { -calculus-calculusxi(yi)-calculus> P{ x i (y i ) pi Pi }i Q { x z 1 Q} (P | Q){ Pi [z / y i ] | Q}x i = x { x i (y i ) Pi | Q}x i x P {-calculus-calculusxi(yi)-calculus> Rst Q {-calculus-calculusx^z-calculus> xy pi Res Pi } i ____________________________________

Out Com pi pi Pi } i ___________________ x (y ) qi renormalized i)-calculus pi P (x) P P {{ -calculus -calculus xi(y >i } }xip=/=/ qii (x) Pq i = 14 October 2009 i i xi ( yi ) (x)P { qi Pi }i BASICS'09, Shanghai i

i p x j x j x 24 Implementation of pa Compilation in a DM Distributed << P | Q >> = >>.start(); Compositional << P op Q >> = op << >> : << P >>.start() | pa DM << Q << P >> jop << Q >> for all

Channels are buffers with test-calculusand-calculusset (synchronized) methods for input and output. The input-calculusguarded choice selects probabilistically one of the channels with available data 14 October 2009 BASICS'09, Shanghai 25 Encoding into pa [[ ]] : Fully distributed pa [[ P | Q ]] [[ P ]] | [[ Q ]] Preserves the communication structure [[ P ]] =

= [[ P ]] Compositional [[ P op Q ]] = Cop [ [[ P ]] , [[ Q ]] ] Correct wrt a notion of probabilistic testing semantics P must O 14 October 2009 iff [[ P ]] must [[ O ]] with prob 1 BASICS'09, Shanghai 26 Encoding into pa Idea (from an idea of Uwe Nestmann): Every mixed choice is translated into a parallel comp. of processes corresponding to the branches, plus a lock f The input processes compete for acquiring both its own lock and the lock of the partner The input process which succeeds first, establishes the communication. The other alternatives are discarded

f Pi P R f Ri Qi Ri Q S f Si f The problem is reduced to a dining philosophers problem: each lock is a fork, each input process is a philosopher, and enters a competition to get his adjacent forks. The winners of the competition can synchronize, which corresponds to eating in the DP. There can be more than one winner Generalized DP: each fork can be adjacent to more than two 14 October 2009 BASICS'09, Shanghai 27 Dining Philosophers: classic case Each fork is shared by exactly two philosophers 14 October 2009 BASICS'09, Shanghai 28 Dining Philosophers: generalized case Each fork can be shared by more than two philosophers

14 October 2009 BASICS'09, Shanghai 29 Intended properties of solution Deadlock freedom (aka progress): if there is a hungry philosopher, a philosopher will eventually eat Starvation freedom: every hungry philosopher will eventually eat (but we wont consider this property here) Robustness wrt a large class of schedulers: A scheduler decides who does the next move , not necessarily in cooperation with the program, maybe even against it Fully distributed: no centralized control or memory Symmetric: All philosophers run the same code and are in the same initial state

The same holds for the forks 14 October 2009 BASICS'09, Shanghai 30 The Dining Philosophers -calculus a brief history Problem proposed by Edsger Dijkstra in 1965 (actually the popular formulation is due to Tony Hoare) Many solutions had been proposed for the DP, but none of them satisfied all requirements In 1981, Lehmann and Rabin proved that There was no deterministic solution satisfying all requirements They proposed a randomized solution and proved that it satisfies all requirement. Progress is satisfied in the probabilistic sense, I.e. there is probability 1 that a philosopherwill eventually eat.

Meanwhile, Francez and Rodeh had come out in 1980 with solution to the DC written in CSP The controversy was solved by Lehmann and Rabin who proved that CSP (with guarded choice) is not implementable in a distributed fashion (deterministically). 14 October 2009 BASICS'09, Shanghai 31 The algorithm of Lehmann and Rabin 7) think; choose probabilistically first_fork in {left,right}; if not taken(first_fork) then take(first_fork) else goto 3; if not taken(second_fork) then take(second_fork); else { release(first_fork); goto 2 } eat; release(second_fork); release(first_fork); 8) goto 1 1) 2)

3) 4) 5) 6) 14 October 2009 BASICS'09, Shanghai 32 Problems Wrt to our encoding goal, the algorithm of Lehmann and Rabin has two problems: 1. It only works for the classical case (not for the generalized one) 2. It works only for fair schedulers 14 October 2009 BASICS'09, Shanghai 33 Conditions on the graph Theorem:

There are essentially three ways in which two cycles can be connected: The algorithm of Lehmann and Rabin is deadlock-calculusfree if and only if all cycles are pairwise disconnected 14 October 2009 BASICS'09, Shanghai 34 Proof of the theorem If part) Each cycle can be considered separately. On each of them the classic algorithm is deadlock-calculusfree. Some additional care must be taken for the arcs that are not part of the cycle. Only if part) By analysis of the three possible cases. Actually they are all similar. We illustrate the first case committed taken 14 October 2009 BASICS'09, Shanghai 35 Proof of the theorem

The initial situation has probability p > 0 The scheduler forces the processes to loop Hence the system has a deadlock (livelock) with probability p Note that this scheduler is not fair. However we can define even a fair scheduler which induces an infinite loop with probability > 0. The idea is to have a scheduler that gives up after n attempts when the process keep choosing the wrong fork, but that increases (by f) its stubborness at every round. With a suitable choice of n the probability of a loop is 14 October 2009 and f p/4 BASICS'09, Shanghai we have that 36 Solution for the Generalized DP

As we have seen, the algorithm of Lehmann and Rabin does not work on general graphs However, it is easy to modify the algorithm so that it works in general The idea is to reduce the problem to the pairwise disconnetted cycles case: Each fork is initially associated with one token. Each philosopher needs to acquire a token in order to participate to the competition. After this initial phase, the algorithm is the same as the Lehman & Rabins Theorem: The competing philosophers determine a graph in which all cycles are pairwise disconnected Proof: By case analysis. To have a situation with two connected cycles we would need a node with two tokens. 14 October 2009 BASICS'09, Shanghai 37 Generalized philosophers The other problem we had to face: the

solution of Lehmann and Rabin works only for fair schedulers, while pa does not provide any guarantee of fairness Fortunately, it turns out that the fairness is required only in order to avoid a busy-calculuswaiting livelock at instruction 3. If we replace busy-calculuswaiting with suspension, then the algorithm works for any scheduler This result was achieved independently also by [Duflot, Fribourg, Picarronny 02]. 14 October 2009 BASICS'09, Shanghai 38 Rabin The algorithm ofthe Lehmann Modified so to avoid need for and fairness Rabin 1) 2) 3) 3) 4) 4)

5) 6) 5) 6) 7) 8) think; (second_fork); choose probabilistically first_fork in release(first_fork); {left,right}; goto 1 think; if not taken(first_fork) take(first_fork) choose probabilistically then first_fork in else wait; {left,right}; if not then not taken(second_fork) taken(first_fork) then take(second_fork); elsegoto { release(first_fork); take(first_fork) else 3; goto 2 }taken(second_fork) then if not eat;

take(second_fork); else release(second_fork); { release(first_fork); goto 2 } release(first_fork); Eat; goto 1 release 14 October 2009 BASICS'09, Shanghai 39 The encoding [[ (x) P ]] = (x) [[ P ]] [[P | Q ]] = [[ P ]] | [[ Q ]] [[ gi.Pi ]] = the translation we have just seen Theorem: For every P, [[P]] and P are testing-calculus equivalent. Namely for every test T, inf (Prob (succ, [[ P ]] (Prob (succ , P | T)) |

[[T ]] ) = inf sup (Prob (succ, [[ P ]] (Prob (succ , P | T)) | [[T ]] ) = sup 14 October 2009 BASICS'09, Shanghai 40 Conclusion We have provided an encoding of the calculus into a probabilistic version of its asynchronous fragment fully distributed compositional correct wrt a notion of testing

semantics Advantages: high-calculuslevel solutions to distributed algorithms Easier to prove correct (no reasoning about randomization required) 14 October 2009 BASICS'09, Shanghai 41