DOC PREVIEW
CMU CS 15312 - The pi-Calculus and Concurrent ML

This preview shows page 1-2-3-4 out of 13 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 13 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 13 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 13 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 13 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 13 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Lecture Notes onThe π-Calculus and Concurrent ML15-312: Foundations of Programming LanguagesFrank PfenningLecture 26December 7, 2004In this lecture we first generalize the calculus of concurrent processes sothat values can be transmitted during communication. But our languagehas no primitive values, so this just reduces to transmitting names alongchannels that are themselves represented as names. This means that a sys-tem of processes can dynamically change its communication structure be-cause connections to processes can be passed as first class values. This iswhy the resulting language, the π-calculus, is called a calculus of mobile andconcurrent communicating processes. In the second part of the lecture weshow how concurrency primitives along the lines of the π-calculus can beembedded in ML, leading to Concurrent ML (CML).We generalize actions and differentiate them more explicitly into inputactions and output actions, since one side of a synchronized communica-tion act has to send and the other to receive a name. We also replace prim-itive process identifiers and defining equations by process replication !Pexplained below.Action prefixes π : : = a(y) receive y along a| ahbi send b along a| τ unobservable actionProcess exps P : : = N | (P1| P2) | new x.P | !PSums N : : = 0 | N1+ N2| π.PIn examples π.0 is often abbreviated by π. Note that in a summanda(y).P, y is a bound variable with scope P that stands for the value receivedalong a. On the other hand, ahbi.P does not bind any variables. EvenLECTURE NOTES DECEMBER 7, 2004L26.2 The π-Calculus and Concurrent MLthough the syntax does not formally distinguish, we use x for binding oc-currences of names (subject to renaming), and a and b for non-binding oc-currences.The structural congruence remains the same as before, except that inaddition we have !P ≡ P | !P , that is, a process !P can spawn arbitrarilymany copies of itself. For references, we repeat the laws here.1. Renaming of bound variables (α-conversion)2. Reordering of terms in a summation3. P | 0 ≡ P , P | Q ≡ Q | P, P | (Q | R) = (P | Q) | R4. new x.(P | Q) ≡ P | new x.Q if x 6∈ fn(P )new x.0 ≡ 0, new x.new y.P ≡ new y.new x.P5. !P ≡ P | !PBefore presenting the transition semantics, we consider the followingexample.P = ((xhy i.0 + z(w).whyi.0) | x(u).uhvi.0 | xhzi.0)The middle process can synchronize and communicate with either the firstor the last one. Reaction with the first leads toP1= (0 | yhvi.0 | xhzi.0) ≡ (yhvi.0 | xhzi.0)which cannot transition further. Reaction with the seconds leads toP01= ((xhyi.0 + z(w).whyi.0) | zhvi.0 | 0)which can step further toP02= (vhyi.0 | 0 | 0)Next we show the reaction rules in a form which does not make anexternally observable action explicit, and exploits structural congruence.LECTURE NOTES DECEMBER 7, 2004The π-Calculus and Concurrent ML L26.3τ.P + N −→ PTau(a(x).P + M) | (ahbi.Q + N) −→ ({b/x}P ) | QReactP −→ P0P | Q −→ P0| QParP −→ P0new x.P −→ new x.P0ResQ ≡ P P −→ P0P0≡ Q0Q −→ Q0StructAs a simple example we will model a storage cell that can hold a valueand service get and put requests to read and write the cell contents. We firstshow it using definitions for process identifiers and then rewrite it usingprocess replication.C(x, get, put)def= gethxi.Chx, get, puti+ put(y).Chy, get, putiWe express this in the π-calculus by turning C itself into a name, left-hand side into an input action and occurrences on the right-hand side intoan output action.! c(x, get, put).(gethxi.chx, get, puti.0 + put(y).chy, get, puti.0)We abbreviate this process expression by !C. In order to be in the cal-culus we must be able to receive and send multiple names at once. It isstraightforward to add this capability. As an example, consider how to cre-ate cell with initial contents 3, write 4 to it, read the cell and then print thecontents some output device. Printing a is represented by an output actionprinthai.0. We also consider 3 and 4 just as names here.!C | new g.new p.ch3, g, pi.ph4i.g(x).printhxi.0Note that c and print are the only free names in this expression. Notealso that we are creating new names g and p to stand for the channel toget or put a names into the storage cell C. We leave it to the reader as aninstructive exercise to simulate the behavior of this expression. It should beclear, however, that we need to use structural equivalence initially to obtainLECTURE NOTES DECEMBER 7, 2004L26.4 The π-Calculus and Concurrent MLa copy of C with which we can react after moving the quantifiers of g andp outside.As a more involved example, consider the following specification of thesieve of Eratosthenes. We start with a stream to produce integers, assumingwe have a primitive successor operation on integer names.1The idea is tohave a channel which sends successive numbers.!count(n, out).outhni.counthn + 1, outiSecond we show a process to filter all multiples of a given prime num-ber from its input stream while producing the output stream. We assumean oracle (x mod p = 0) and its negation.!filter(p, in, out).in(x).((x mod p = 0)().filterhp, in, outi.0+ (x mod p 6= 0)().out(x).filterhp, in, outi.0)Finally, we come to the process that generates a sequence of prime num-bers, starting from the first item of the input channel which should be prime(by invariant).!primes(in, out).in(p).outhpi.new mid.(filterhp, in, midi.0 | primeshmid, outi.0)primes establishes a new filtering process for each prime and threads theinput stream in into the filter. The first element of the filtered result streamis guaranteed to be prime, so we can invoke the primes process recursively.At the top level, we start the process with the stream of numbers count-ing up from 2, the smallest prime. This will generate communication re-quests outhpi for each successive prime.new nats.counth2, natsi | primeshnats, outiIn this implementation, communication is fully synchronous, that is,both sender and receiver can only move on once the message has been ex-changed. Here, this means that the prime numbers are guaranteed to beread in their natural order. If we don’t care about the order, we can rewritethe process so that it generates the primes asynchronously. For this we usethe general transformation ofahbi.P =⇒ τ.(ahbi.0 | P )1This can also be coded in the π-calculus, but we prefer to avoid this complication here.LECTURE NOTES DECEMBER 7, 2004The π-Calculus and Concurrent ML L26.5which means the computation of P


View Full Document

CMU CS 15312 - The pi-Calculus and Concurrent ML

Download The pi-Calculus and Concurrent ML
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view The pi-Calculus and Concurrent ML and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view The pi-Calculus and Concurrent ML 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?