Assignment 5: Concurrency
15-312: Principles of Programming Languages (Spring 2023)
This assignment studies concurrency through the lens of a concurrent programming language known as Concurrent Algol (CA).
Effectful computations (involving side-effects) distinguish themselves from “pure” computation by involving some sort of interaction. Think IO effects (user interaction) or reference cells (state/mem- ory interaction). We seek to make this more explicit by introducing interaction as a primitive notion.
To this end, CA augments our existing expression/command modal separation with two new sorts accomodating interaction: processes and actions. The formulation of CA as presented in this assignment is derived from that of Chapter 40 of PFPLand relevant supplements posted on the course website.
CA is conceptually similar to the concurrent programming language Go.
1 Syntax and Semantics
First, we will introduce the user language of CA.
cmd( τ ) chan( τ )
cmd[τ ](m) chref⟨a⟩
ret(e) bnd(e;x.m) spawn( e ) emitref( e1 ; e2 ) sync( e ) newchan⟨τ⟩(a.m)
τ cmd τ chan
… cmd m &a
ret e bndx←e;m spawn( e ) emitref( e1 ; e2 ) sync( e ) newchan⟨τ⟩(a.m)
other types command channel
other expressions encapsulation channel reference
spawn process
send message on channel receive message on channel new channel
You may think of other types and other expressions as common features discussed earlier in the semester, such as products, sums, and natural numbers.
Definition 1.1 (Synchronicity). We say that an operation runs synchronously if it must complete before further operations can begin. Conversely, we say that an operation runs asynchronously if
it immediately returns, running concurrently and thus not blocking further operations. We informally describe the behavior of each command as follows:
• ret( e ): An “interface” between the expression and command sorts, including all expressions as trivial commands.
• bnd( e;x.m ): Sequencing of computation, synchronously running the suspended computation e and then binding its result to x and running m. Note that e is an expression, allowing the programmer to compute a command to run.
• spawn(e): Creation of a new concurrent process, where e is the (encapsulated) command that will be asynchronously executed by the process. return type of the command as usual. Returns a “return channel” channel reference, which the spawned process uses to send the value returned by the command.
• emitref( e1 ; e2 ): Sends the value e2 along channel reference e1 asynchronously , returning immediately regardless of whether the message has been received yet.
• sync( e ): Waits for a value to be transmitted along channel reference e synchronously , blocking until a value is received. Upon seeing a transmission, returns the value.
• newchan⟨τ ⟩( a . m ): Creates a new channel for use within the command m.
1.1 Statics
The statics of the language are defined with three judgments. As usual, Γ ⊢Σ e : τ is the typing rule for expressions, here including a channel context Σ = a1 ~ τ1, . . . , an ~ τn describing the names and associated types of channels that are available for use. The rules for the new forms are given below.
Γ ⊢Σ e : τ
Γ ⊢ m ∼· τ
Γ ⊢Σ cmd[τ ](m) : cmd(τ )
(SE2) Γ ⊢Σ,a~τ chref⟨a⟩ : chan(τ )
m ∼· τ formalizes the typing for commands. ·
The judgment Γ ⊢ Σ
Γ ⊢ m ∼· τ
Γ⊢ spawn(e)∼· chan(τ) Γ⊢ emitref(e ;e )∼· unit Σ·Σ12·
Running this command given a channel a ~ nat would behave as follows:
1. Send 312 on channel a asynchronously, continuing immediately while the message 312 is
available on channel a.
2. Synchonize on channel a, receiving the message 312 immediately because it is already available
on channel a.
3. Return 312 as the result.
Example 1.3. Consider the following command:
bnd( cmd( sync( chref⟨a⟩ ) ) ; u . emitref( chref⟨a⟩ ; 312 ) )
Running this command given a channel a ~ nat would behave as follows:
1. Synchonize on channel a, but getting “blocked”/stuck forever because no messages are avail- able on channel a.
Γ⊢ e:cmd(τ) Σ
Γ,x:τ⊢ m∼·τ′
Γ⊢Σ e:cmd(τ) (SM3) Γ⊢Σ e1 :chan(τ) Γ⊢Σ e2 :τ(SM4)
Γ⊢ ret(e)∼· τ
Γ⊢ bnd(e;x.m)∼· τ′
Γ⊢ e:chan(τ) Σ
Γ⊢ ~ m∼·τ′ Σ,a τ ·
(SM5) Σ·Σ·
Γ⊢ sync(e)∼· τ
Γ⊢ newchan⟨τ⟩(a.m)∼· τ′ Using the informal description of the dynamics, we consider some simple examples.
Example 1.2. Consider the following command:
bnd( cmd( emitref( chref⟨a⟩ ; 312 ) ) ; u . sync( chref⟨a⟩ ) )
1.2 Examples
Example 1.4. Consider the following command:
bnd( cmd( emitref( chref⟨a⟩ ; 312 ) ) ; u . bnd( cmd( sync( chref⟨a⟩ ) ) ; x . sync( chref⟨a⟩ ) ) )
Running this command given a channel a ~ nat would behave as follows:
1. Send 312 on channel a asynchronously, continuing immediately while the message 312 is
available on channel a.
2. Synchonize on channel a, receiving the message 312 immediately because it is already available
on channel a.
3. Synchonize on channel a, but getting “blocked”/stuck forever because no messages are avail-
able on channel a.
Task 1.1 (5 pts). Let f : τ → τ and Σ = a ~ τ , b ~ τ . Write a command ⊢ m ∼· unit that
reads a value x from channel a and sends f(x) over channel b.
Henceforth, we abbreviate bnd( e ; x . ret( x ) ) as do( e ). Example 1.5 (Producer). Let:
memit =bnd(cmd(emitref(chref⟨a⟩;n));x.do(f(n′)))
mproduce =do(ap(fun[nat;cmd(unit)](f.n.ifz(n;cmd(ret(triv));n′ .cmd(memit)));10))
Running this command given a channel a ~ nat spawns 10 asynchronous processes, each of which emits a number 1 ≤ n ≤ 10 on channel a and immediately exits. Notice that we use a recursive function to compute a “large” command.
Task 1.2 (15 pts). Write a “consumer” mconsume that reads 10 natural numbers over channel a and returns their sum. You may use e1 + e2 to sum two natural numbers.
Running bnd( mproduce ; u . mconsume ) should evaluate to 55. Hint. You may wish to model your solution on mproduce.
Remark. The producer-consumer pattern is common in concurrent programming.
2 Processes
Underlying CA is a sort of procesess, which concurrently communicate. Processes send and receive messages over channels, which we will denote a.
Proc p ::=
stop 1 conc(p1 ;p2 ) p1 ⊗p2 newch[τ](a.p) νa~τ.p
nullary concurrent composition binary concurrent composition newchannel
send on channel a receive on channel a
silent send receive
Action α ::= ε snd⟨a⟩(e)
rcv⟨a⟩( e )
run⟨a⟩( m ) send⟨a⟩(e) recv⟨a⟩(x.p)
run⟨a⟩( m ) !a(e) ?a(x.p)
Atomic Processes Atomic processes run⟨a⟩(m) contain commands m, which will be user- written programs; we will introduce commands in Section 1. It will be arranged in the dynamics that the channel a of an atomic process eventually receives the result of the command m; you may observe that channel a serves as a unique “process ID” for a given atomic process.
Remark. Processes and actions are not user-level constructs, like stacks k and states s in KPCF. Programmers will write commands m, not processes p.
2.1 Statics
The statics for processes are given in Appendix B.3.1.
Processes p are identified up to structural congruence, described in Appendix B.3.2. Of note, structural congruence states that:
• Concurrent composition operators 1 and − ⊗ − form a commutative monoid, allowing us to reorder concurrent composition of processes.
• Newchannelsνa~τ.pcanbehoistedtothetopofaprocess. For example, we have:
(νa1 ~τ1 .p1)⊗1⊗(?b(x.νa2 ~τ2 .p2))≡νa1 ~τ1 .νa2 ~τ2 .p1 ⊗?b(x.p2) 2.2 Dynamics
The dynamics of processes are given via actions α; the judgment p 7→ p states that process p steps
to p′ with action α. The key rules are given below; we provide the rules for atomic processes in Appendix C.3.
α ′ p17→p1
a!e ′ p1 7→ p1
p2 7→ p2 p 7→ p ⊢Σαaction
Σ,a~τ (P2) Σ,a~τ
Σ,a~τ α′ε′′α′
Σ (P1) p1 ⊗p2 7→p1 ⊗p2
p1 ⊗p2 (P4)
νa~τ .p7→νa~τ .p Σ
a!e !a(e) 7→ 1
?a(x.p) 7→ {e/x}p
Task 2.1 (5 pts). Let Σ = a ~ nat,b ~ nat,c ~ nat. Provide a process p with ⊢Σ p proc such that
if p receives a natural number n along channel a, it will send n along channels b and c.
Task 2.2 (10 pts). Consider the following process p: !a(1)⊗!a(2)⊗?a(x.!b(x))
We have ⊢Σ p proc, where Σ = a ~ nat, b ~ nat. Provide two processes, p′1 and p′2, such that ε′ε′ ′′
p7→Σ p1 andp7→Σ p2 butitisnot thecasethatp1 ≡p2. Thisshowsthatthedynamicsof CAare nondeterministic!
2.3 Safety
Like the other languages we have considered in this course, CA satisfies progress and preservation theorems. Here, we will consider the progress theorem.
One might imagine that the progress theorem might say the following:
Theorem 2.1 (Faulty Progress). If ⊢Σ p proc, then either p ≡ 1 or p 7→ p for some p .
This theorem holds for some processes p. For example: !a(312)⊗?a(x.1) 7→ 1
However, in general, this theorem is false!
Task 2.3 (10 pts). Provide a process p that is a counterexample to Theorem 2.1. Briefly (one sentence) justify why your choice of p is a counterexample. You should not use atomic processes run⟨a⟩( m ) in your counterexample.
Hint. Note the ε action in Theorem 2.1.
Hint. Your counterexample can be very simple!
The true progress theorem involves non-ε actions: 6
CS Help, Email: tutorcs@163.com
′ ′ ′ α ′′ Theorem 2.2 (Progress). If ⊢Σ p proc, then either p ≡ 1 or p ≡ νΣ{p} such that p 7→′ p for
some p′′ and some ⊢Σ,Σ′ α action.
Recall the following statics rule from Appendix B.3.1:
and the structural congruence rules in Appendix B.3.2.
(SP1) Γ ⊢Σ p1 proc Γ ⊢Σ p2 proc(SP2) Γ ⊢Σ,a~τ e : τ (SP5) Γ⊢Σ p1 ⊗p2 proc Γ⊢Σ,a~τ !a(e)proc
Task 2.4 (15 pts). Prove Theorem 2.2 for these three statics rules, using the dynamics given above
3 Implementing the Dynamics
In this section, you will implement parts of the dynamics for CA.
In order to work up to structural congruence of processes, we will use an “execution context” data structure to maintain a canonical form for processes, thus mediating communication. You should read lang-ca/execution-context.sig to understand how this data structure will behave.
Remark. You may attempt the following tasks in either order.
3.1 Dynamics
Task 3.1 (30 pts). Implement the remaining cases of progress in lang-ca/dynamics-ca.fun .
progress (a, m) transitions an atomic processes run⟨a⟩(m) to an execution context (i.e., a collection of atomic processes). In particular, progress will be based directly on rules R1-R7 from Appendix C.3, so it will not be recursive. The output in each case will be built via the operations provided by structure EC , where:
Testing To test your implementation, move the reference solution heap image into lang-ca/ and include your dynamics file and the updated top-level structure:
This will make use of the reference implementation of EC . You should see the following out- put:
structure EC : EXECUTION_CONTEXT where type chan = CA.Chan.t and type msg = CA.Exp.t
smlnj @SMLload lang -ca
– use “dynamics -ca.fun”; use “dynamics -ca.sml”; use “interpreter -ca.sml”;
– InterpreterCA.evalFile “tests.lam”;
fib 10 = 55
b (* nondeterministic, could be c *) abc
You can also run:
– InterpreterCA.repl (); -> load “tests.lam”;
for a more verbose output, including printing the execution context. You may find it useful to change (or comment out parts of) tests/tests.lam when debugging.1
3.2 Execution Context
A process can be put into a canonical form containing:
• For each channel a, either a collection of surplus messages (of the form ! a( e )) or a collection of identifiers for waiting processes. There will never be both a surplus and a deficit simulta- neously: if a message and a waiter would be present on a channel, the waiter should be given the message and marked as ready.
• A map from waiter identifiers to true waiters (of the form x . p).
• A collection of ready processes, each of the form run⟨a⟩( m ).
We will call such a canonical form an execution context and represent all processes in this form. In this subsection, we will implement this data structure, using rules P1-P5 (transitions for non- atomic processes) from Section 2.2 and rules E1-E13 (structural congruence) from Appendix B.3.2 to convert a process to normal form.
The signature in lang-ca/execution-context.sig details which operations should be supported by an execution context. The type parameter ’a represents an abstract atomic process type; in
the dynamics, it will be instantiated at CA.Chan.t * CA.Cmd.t .
All new channel identifiers ν τ ~ a . p can be hoisted to the top via rules E12 and E13. Therefore, in the code, we do not include an operation on execution contexts to bind a new channel; this is handled by Chan.new , and we may assume capture is never incurred.
Task 3.2 (40 pts). Implement in
according to the specification in . Comments in the file describe
how you should understand the types.
Observe that functor ExecutionContext is parameterized on arbitrary channel and message
types. Thus, your implementation will not involve any CA-specific constructs.
Additionally, it is parameterized on a queue data structure, which you should use internally to queue messages, waiters, and ready processes. To simulate nondeterminism, the provided implementation may be randomized.
Testing To test your execution context independently, you can run TestHarness.testEC . By default, TestHarness introduces random dequeueing, so you may notice that tests fail only some- times. If you wish to test deterministically, you can use structure Queue (val random = false) in . In the same file, you can read the test cases to aid with debugging (using
for verbose test output).
1In , the function evalCmd builds the initial processes. In , the function run contains the entry point for the dynamics.
tests/tests.sml
functor ExecutionContext
lang-ca/execution-context.fun
lang-ca/execution-context.sig
TestHarness.testEC true
lang-ca/interpreter-ca.fun
lang-ca/process-executor.sml
You should now be able to run the aforementioned CA test cases using your execution context, as well, by loading sources.cm .
4 References
Next, we will implement free assignable references in Concurrent Algol.
4.1 Reference Cells
Task 4.1 (35 pts). In tests/refs.lam , implement the signature of three functions that define ref cells of natural numbers, a type named ref :
newref , when given an initial value, should return a ref containing that value.
deref , when given a ref cell, should return the contents of the cell, such that the cell may
be read again to obtain the same value in the future until the cell is reset.
set , when given a ref cell and a new value, should update the contents of the cell such that future dereferences return the new value until the cell is reset again.
You are given the test file tests/refs-test.lam to verify your implementation. Feel free to write more tests of your own.
To help you get started, first take a look at tests/tests.lam and tests/tests2.lam , which give some examples of using the CA concrete syntax. If you would like a complete, formal presentation of the concrete syntax, be sure to look at Section A.
Next, please check out tests/prng.lam and tests/prng-test.lam . This is an implementation of a pseudorandom number generator (PRNG), specifically one called Blum Blum Shub. It defines a type named prng with two functions:
• newprng , when given a modulus and seed value (both natural numbers), should return a prng initialized with those values
• next , when given a prng, should output the value stored within the prng as the next pseu- dorandom number, then update the prng’s value to be the square of the previous value mod the modulus
The key takeaways from the PRNG example are:
• how it simulates “memory” or “state” using the server process
• how next communicates back and forth with the server process using channel-passing
Do familiarize yourself with the PRNG example, as your ref implementation will likely use similar strategies and code constructs.
4.2 Atomic References
The mutable references we implemented work well if we agree to be careful with concurrent reads and writes. If we try to do many reads and writes concurrently, though, we can encounter race conditions!
For example, consider incrementing a reference cell. Normally, it requires a read from the cell, then a write of the incremented value back to the cell. If there is only one thread performing the
浙大学霸代写 加微信 cstutorcs
increment operation, everything will proceed as planned.
However, what if multiple threads try to increment a reference simultaneously? The first thread may read from the cell, followed immediately by the second thread. Then, both threads write back the value they saw plus one—the same value for both threads. One of the increments got lost, and we have a race condition, meaning the increment operation is not thread-safe.
Your next task is to make the references thread-safe by providing atomic operations that cannot be interrupted in such ways.
Task 4.2 (35 pts). In tests/atomic.lam , implement three operations on a new type atomic_ref :
new_atomic_ref , when given a reference, wraps it to make it atomic.
incr , which performs an atomic increment of the cell: no two threads performing a concur-
rent incr operation may interfere with each other.
cmpxchg , which performs an atomic compare-and-exchange: given a ref cell, a value expected ,
and a value new , if the cell currently has the value expected , update it to have value new and return true. Otherwise, make no change to the contents and return false. The entire operation must happen atomically.
In particular, incr and cmpxchg must be atomic with respect to each other, meaning that con- current invocations of either function must not interfere; the result should always look as if the threads had performed their actions sequentially instead.
Hint. You may find the notion of a lock useful, though it is not required. A lock is an “object” that only one process may “have” at a time; it can be used to guarantee that even given multiple concurrent threads, only one thread will perform some sensitive operation at a time (such as accessing a ref cell).
It does so through two operations:
• acquire which is called to request the lock and stall the thread until it is safe to proceed, and • release which is called afterward, allowing another thread to now proceed.
Hint. A lock may be implemented easily using the features of Concurrent Algol. Think about how you might use a channel to hold an “object” that only one process can have at a time.
To test your code, you may run the test file tests/atomic-test.lam .
Here, we outline the concrete syntax of CA.
Abstract Syntax
nat sum(τ1;τ2) prod(τ1;τ2) arr(τ1;τ2) cmd(τ) chan( τ )
in⟨l⟩[ τ1 ; τ2 ]( e )
in⟨r⟩[ τ1 ; τ2 ]( e ) case(e;x1 .e1 ;x2 .e2 ) pair( e1 ; e2 )
split( e ; x1, x2 . e′ )
λ[ x ]( τ . e )
fun[τ1 ;τ2](f.x.e) if( e ; e1 ; e2 ) ifz[τ](e;e1 ;x.e2) let(e;x.e1 )
cmd[ τ ]( m )
ret(e) bnd(e;x.m) spawn( e ) emitref( e1 ; e2 ) sync( e ) newchan⟨τ ⟩( a . m )
Concrete Syntax
Description
bool type natural number sum type product type function type command channel
left injection
right injection case expression pair/tuple
lambda expression function conditional
encapsulation channel reference
spawn process
send message on channel receive message on channel new channel
tau1 + tau2
tau1 * tau2
tau1 -> tau2
inl[tau1 + tau2] e
inr[tau1 + tau2] e
case e of {x1 => e1 | x2 => e2}
split e is x1, x2 in e’
fn (x : tau)=> e
fun f (x : tau1): tau2 = e
if e then e1 else e2
ifz e then e1 else x => e2
let val x = e in e1 end
val x = e in m
emit(e1, e2)
newchan x ~ tau in c
We also provide various constant forms, such as true, false, zero, succ e .
Also take note of various pieces of (very helpful) syntactic sugar for writing commands:
• emit[c](e) is sugar for emit(chan[c], e) • sync[c] is sugar for sync(chan[c])
• do e issugarfor val x = e in ret(x)
• {c1,…,cn} is sugar for val _ = cmd(c1)in … in cn
directive ::= type t = tau | fun f (x1 : tau1) … (xn : taun) : tau = term
| val x = term | m | c | load f
decl d ::= fun f (x1 : tau1) … (xn : taun) : tau = term | val x = term
type tau ::= t | tau1 + tau2 | tau1 * tau2 | tau1 -> tau2 | rec(t.tau)
| unit | void | nat | bool | cmd[tau] | chan[tau]
cmd c ::= ret(e) | val x = e in c | spawn(e) | emit(e1,e2) | emit[k](e)
| sync(e) | sync[k] | newchan x ~ tau in c | print e | do e | {c1,…,cn}
atom a ::= (e) | n | ’…’ | true | false | zero | x | () | (e1,e2)
| case e of {x1 => e1 | x2 => e2} | let d1…dn in e end
tree s ::= a1 … an | s1 + s2 | s1 – s2 | s1 * s2 | s1 / s2 | s1 = s2
| s1 != s2 | s1 < s2 | s1 <= s2 | s1 > s2 | s1 >= s2 | s1 && s2 | s1 || s2
term e ::= s
| fn x : tau => e | fn(x : tau) => e | split e is x1, x2 in e’ | inl[tau]e | inr[tau]e
| fold[tau] e | unfold e | if e then e1 else e2
| succ e | ifz e then e1 else x => e2 | abort[tau] e | cmd c | !e
The parser will delineate directives by “;”. See tests/tests.lam for some examples.
B.1 Expressions
Γ ⊢Σ e : τ
Γ ⊢ m ∼· τ Σ ·
Γ ⊢Σ cmd[τ ](m) : cmd(τ ) B.2 Commands
Γ ⊢ m ∼· τ
Γ⊢ spawn(e)∼· chan(τ) Γ⊢ emitref(e ;e )∼· unit Σ·Σ12·
Γ ⊢Σ,a~τ chref⟨a⟩ : chan(τ )
Γ⊢ e:cmd(τ) Σ
Γ,x:τ⊢ m∼·τ′
Γ⊢ bnd(e;x.m)∼· τ′
Γ⊢Σ e:cmd(τ) (SM3) Γ⊢Σ e1 :chan(τ) Γ⊢Σ e2 :τ(SM4)
Γ⊢ ret(e)∼· τ
Γ⊢ e:chan(τ) Σ
Γ⊢ ~ m∼·τ′ Σ,a τ ·
(SM5) Σ·Σ·
Γ⊢ sync(e)∼· τ
Γ⊢ newchan⟨τ⟩(a.m)∼· τ′
B.3 Processes
B.3.1 Typing
The judgment Γ ⊢Σ p proc describes the valid processes relative to the signature Σ and context Γ. Processes have to be typed under a specific context due to the existence of accepting processes.
Γ ⊢Σ p proc Γ⊢Σ 1proc
Γ⊢ ~ m∼·τ Σ,a τ ·
Γ⊢Σ,a~τ run⟨a⟩(m)proc
Γ ⊢Σ p1 proc Γ ⊢Σ p2 proc(SP2) Γ⊢Σ p1 ⊗p2 proc
Γ ⊢Σ,a~τ p proc (SP3) Γ⊢Σ νa~τ .pproc
Γ,x:τ⊢ ~ pproc
Σ,a τ (SP6)
Γ⊢Σ,a~τ ?a(x.p)proc
Γ⊢ ~ e:τ Σ,a τ
Γ⊢Σ,a~τ !a(e)proc
B.3.2 Structural Congruence
Processes are identified up to structural congruence, an equivalence relation written p1 ≡ p2. p1 ≡ p2
First, we state that p1 ≡ p2 is an equivalence relation (reflexive, symmetric, and transitive): p1 =α p2(E1) p2 ≡ p1(E2) p1 ≡ p2 p2 ≡ p3(E3)
p1 ≡ p2 p1 ≡ p2
Then, we state that p1 ≡ p2 is a congruence:
p 1 ≡ p ′1 p 2 ≡ p ′2 p ≡ p ′
p ⊗p ≡p′ ⊗p′ (E4) νa~τ.p≡νa~τ.p′(E5) 1212
We guarantee that 1 and − ⊗ − form a commutative monoid: p ⊗(p ⊗p )≡(p ⊗p )⊗p (E7) p⊗1≡p(E8)
p ≡ p ′ ?a(x.p)≡?a(x.p′)(E6)
p ⊗p ≡p ⊗p (E9) 123123 1221
We allow new channels to be reordered, removed if unused, and hoisted to the top level provided they do not incur capture. Rule E12 is called scope extrusion, since it allows the scope of a to be extruded out of the concurrent composition.
νa1 ~τ1 .νa2 ~τ2 .p≡νa2 ~τ2 .νa1 ~τ1 .p
a ∈/ p (E11) νa~τ .p≡p
a ∈/ p2 (E12) (νa~τ.p1)⊗p2 ≡νa~τ.(p1⊗p2)
B.4 Actions
Actions also admit a statics, given by the judgment ⊢Σ α action. ⊢Σ α action
?a2(x.νa1 ~τ.p)≡νa1 ~τ.?a2(x.p)
⊢Σ ε action
(A1) ⊢Σ,a~τ e : τ (A2) ⊢Σ,a~τ a ! e action
⊢Σ,a~τ e : τ (A3) ⊢Σ,a~τ a ? e action
C Dynamics C.1 Expressions
chref⟨a⟩ val ~ Σ,a τ
C.2 Commands
cmd[ τ ]( m ) val Σ
e 7−→ e′ Σ
bnd(e;x.m)⇒bnd(e′ ;x.m) e1 7−→ e′1
C.3 Processes
ret(e)⇒ret(e′) ΣΣ
e 7−→ e′ Σ
emitref(e1 ;e2)⇒Σ emitref(e′1 ;e2)
spawn(e)⇒Σ spawn(e′)
e1 valΣ e2 7−→ e′2
emitref(e1 ;e2)⇒Σ emitref(e1 ;e′2)
sync(e)⇒Σ sync(e′)
In this formulation of Concurrent Algol, there is no command level transitions for the effects. It does not follow that our language is free of effects, instead all effects have been lifted into process level and carried out at process level. The rules for transitioning processes that does not involve lifting effects from commands are given in Section 2.2.
Rule P1, together with congruence, allows for independent transition of both concurrent sub- processes. P2 enables communications between concurrent processes.
Finally, we may now consider the actions and effects of the commands:
p 7→ p , continued
ε ′ (R1) run⟨a⟩(m) 7→ run⟨a⟩(m )
′ε′ (R3) run⟨a⟩(bnd(cmd[τ ](m1);x.m2)) 7→ νb~τ .run⟨b⟩(m1)⊗?b(x.run⟨a⟩(m2))
run⟨a⟩(ret(e))
ε (R2) 7→ !a(e)
7→ ν b ~ τ . run⟨b⟩( m ) ⊗ run⟨a⟩( ret( chref⟨b⟩ ) )
ε Σ,a~chan( τ )
run⟨a⟩( spawn( cmd[ τ ]( m ) ) )
(R5 ) run⟨a⟩(emitref(chref⟨b⟩;e)) 7→ !b(e)⊗run⟨a⟩(ret(⟨⟩))
e valΣ,a~unit,b~τ
ε Σ,a~unit,b~τ
(R6 ) run⟨a⟩(sync(chref⟨b⟩)) 7→ ?b(x.run⟨a⟩(ret(x)))
ε Σ,a~τ,b~τ
run⟨a⟩(newchan⟨τ⟩(b.m)) 7→ νb~τ.run⟨a⟩(m) Σ,a~τ
In our setup, all command level effects have been elevated to the process level. In particular, a sequence of two commands is achieved by spawning a process for each of the commands, and have the second process wait for the result from the first one on a secret channel. Type annotation makes it possible to figure out the type τ and τ′ in R4 and R3 respectively. Notice that the emit com- mands generates new processes. This should remind you that we are implementing asynchronous sends.
Code Help