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.
https://go.dev/
1 Syntax and Semantics
First, we will introduce the user language of CA.
Typ τ ::= . . . . . . other types
cmd( τ ) τ cmd command
chan( τ ) τ chan channel
Exp e ::= . . . . . . other expressions
cmd[ τ ](m ) cmdm encapsulation
chref⟨a⟩ & a channel reference
Cmd m ::= ret( e ) ret e return
bnd( e ; x . m ) bndx← e ;m sequence
spawn( e ) spawn( e ) spawn process
emitref( e1 ; e2 ) emitref( e1 ; e2 ) send message on channel
sync( e ) sync( e ) receive message on channel
newchan⟨τ⟩( a . m ) newchan⟨τ⟩( a . m ) 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
Γ ⊢Σ e : τ
Γ ⊢Σ m ∼·· τ
Γ ⊢Σ cmd[ τ ](m ) : cmd( τ )
Γ ⊢Σ,a~τ chref⟨a⟩ : chan( τ )
The judgment Γ ⊢Σ m ∼·· τ formalizes the typing for commands.
Γ ⊢Σ m ∼·· τ
Γ ⊢Σ e : τ
Γ ⊢Σ ret( e ) ∼·· τ
Γ ⊢Σ e : cmd( τ ) Γ, x : τ ⊢Σ m ∼·· τ ′
Γ ⊢Σ bnd( e ; x . m ) ∼·· τ ′
Γ ⊢Σ e : cmd( τ )
Γ ⊢Σ spawn( e ) ∼·· chan( τ )
Γ ⊢Σ e1 : chan( τ ) Γ ⊢Σ e2 : τ
Γ ⊢Σ emitref( e1 ; e2 ) ∼·· unit
Γ ⊢Σ e : chan( τ )
Γ ⊢Σ sync( e ) ∼·· τ
Γ ⊢Σ,a~τ m ∼·· τ ′
Γ ⊢Σ newchan⟨τ⟩( a . m ) ∼·· τ ′
1.2 Examples
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⟩ ) )
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.
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 : τ1 → τ2 and Σ = a ~ τ1, b ~ τ2. 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.
https://en.wikipedia.org/wiki/Producer%E2%80%93consumer_problem
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 nullary concurrent composition
conc( p1 ; p2 ) p1 ⊗ p2 binary concurrent composition
newch[ τ ]( a . p ) ν a ~ τ . p new channel
run⟨a⟩(m ) run⟨a⟩(m ) atomic
send⟨a⟩( e ) ! a( e ) send on channel a
recv⟨a⟩(x . p ) ? a(x . p ) receive on channel a
Action α ::= ε ε silent
snd⟨a⟩( e ) a ! e send
rcv⟨a⟩( e ) a ? e receive
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.
• New channels ν a ~ τ . p can be hoisted to the top of a process.
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
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.
p′ ⊢Σ α action
ν a ~ τ . p α7→
ν a ~ τ . p′
? a(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
p′2 but it is not the case that p
2. This shows that the dynamics of CA are
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
p′ for some p′.
This theorem holds for some processes p. For example:
! a( 312 )⊗ ? a(x . 1 ) ε7→
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:
Theorem 2.2 (Progress). If ⊢Σ p proc, then either p ≡ 1 or p ≡ ν Σ′{p′} such that p′
some p′′ and some ⊢Σ,Σ′ α action.
Recall the following statics rule from Appendix B.3.1:
Γ ⊢Σ 1 proc
Γ ⊢Σ p1 proc Γ ⊢Σ p2 proc
Γ ⊢Σ p1 ⊗ p2 proc
Γ ⊢Σ,a~τ e : τ
Γ ⊢Σ,a~τ ! a( e ) proc
Task 2.4 (15 pts). Prove Theorem 2.2 for these three statics rules, using the dynamics given above
and the structural congruence rules in Appendix B.3.2.
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:
structure EC : EXECUTION_CONTEXT where type chan = CA.Chan.t
and type msg = CA.Exp.t
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:
smlnj @SMLload lang -ca
– use “dynamics -ca.fun”; use “dynamics -ca.sml”; use
“interpreter -ca.sml”;
– InterpreterCA.evalFile “tests.lam”;
This will make use of the reference implementation of EC . You should see the following out-
fib 10 = 55
b (* nondeterministic , could be c *)
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 functor ExecutionContext in lang-ca/execution-context.fun
according to the specification in lang-ca/execution-context.sig . 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 tests/tests.sml . In the same file, you can read the test cases to aid with debugging (using
TestHarness.testEC true for verbose test output).
1In lang-ca/interpreter-ca.fun , the function evalCmd builds the initial processes. In
lang-ca/process-executor.sml , the function run contains the entry point for the dynamics.
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
https://en.wikipedia.org/wiki/Blum_Blum_Shub
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.
Sort Abstract Syntax Concrete Syntax Description
Typ τ ::= unit unit unit type
void void void type
bool bool bool type
nat nat natural number
sum( τ1 ; τ2 ) tau1 + tau2 sum type
prod( τ1 ; τ2 ) tau1 * tau2 product type
arr( τ1 ; τ2 ) tau1 -> tau2 function type
cmd( τ ) cmd[tau] command
chan( τ ) chan[tau] channel
Exp e ::= triv () unit
in⟨l⟩[ τ1 ; τ2 ]( e ) inl[tau1 + tau2] e left injection
in⟨r⟩[ τ1 ; τ2 ]( e ) inr[tau1 + tau2] e right injection
case( e ; x1 . e1 ; x2 . e2 ) case e of {x1 => e1 | x2 => e2} case expression
pair( e1 ; e2 ) (e1, e2) pair/tuple
split( e ; x1, x2 . e
′ ) split e is x1, x2 in e’ split
λ[x ]( τ . e ) fn (x : tau)=> e lambda expression
fun[ τ1 ; τ2 ]( f . x . e ) fun f (x : tau1): tau2 = e function
if( e ; e1 ; e2 ) if e then e1 else e2 conditional
ifz[ τ ]( e ; e1 ; x . e2 ) ifz e then e1 else x => e2 ifz
let( e ; x . e1 ) let val x = e in e1 end let
cmd[ τ ](m ) cmd m encapsulation
chref⟨a⟩ chan[a] channel reference
Cmd m ::= ret( e ) ret(e) return
bnd( e ; x . m ) val x = e in m sequence
spawn( e ) spawn(e) spawn process
emitref( e1 ; e2 ) emit(e1, e2) send message on channel
sync( e ) sync(e) receive message on channel
newchan⟨τ⟩( a . m ) newchan x ~ tau in c new channel
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 is sugar for 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( τ )
Γ ⊢Σ,a~τ chref⟨a⟩ : chan( τ )
B.2 Commands
Γ ⊢Σ m ∼·· τ
Γ ⊢Σ e : τ
Γ ⊢Σ ret( e ) ∼·· τ
Γ ⊢Σ e : cmd( τ ) Γ, x : τ ⊢Σ m ∼·· τ ′
Γ ⊢Σ bnd( e ; x . m ) ∼·· τ ′
Γ ⊢Σ e : cmd( τ )
Γ ⊢Σ spawn( e ) ∼·· chan( τ )
Γ ⊢Σ e1 : chan( τ ) Γ ⊢Σ e2 : τ
Γ ⊢Σ emitref( e1 ; e2 ) ∼·· unit
Γ ⊢Σ e : chan( τ )
Γ ⊢Σ sync( e ) ∼·· τ
Γ ⊢Σ,a~τ m ∼·· τ ′
Γ ⊢Σ 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
Γ ⊢Σ 1 proc
Γ ⊢Σ p1 proc Γ ⊢Σ p2 proc
Γ ⊢Σ p1 ⊗ p2 proc
Γ ⊢Σ,a~τ p proc
Γ ⊢Σ ν a ~ τ . p proc
Γ ⊢Σ,a~τ m ∼·· τ
Γ ⊢Σ,a~τ run⟨a⟩(m ) proc
Γ ⊢Σ,a~τ e : τ
Γ ⊢Σ,a~τ ! a( e ) proc
Γ, x : τ ⊢Σ,a~τ p proc
Γ ⊢Σ,a~τ ? a(x . p ) proc
B.3.2 Structural Congruence
Processes are identified up to structural congruence, an equivalence relation written p1 ≡ p2.
First, we state that p1 ≡ p2 is an equivalence relation (reflexive, symmetric, and transitive):
p1 ≡ p2 p2 ≡ p3
Then, we state that p1 ≡ p2 is a congruence:
p1 ≡ p′1 p2 ≡ p
p1 ⊗ p2 ≡ p′1 ⊗ p
ν a ~ τ . p ≡ ν a ~ τ . p′
? a(x . p ) ≡ ? a(x . p′ )
We guarantee that 1 and −⊗− form a commutative monoid:
p1 ⊗ (p2 ⊗ p3) ≡ (p1 ⊗ p2)⊗ p3
p1 ⊗ p2 ≡ p2 ⊗ p1
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 ≡ p
(ν a ~ τ . p1)⊗ p2 ≡ ν a ~ τ . (p1 ⊗ p2)
? a2(x . ν a1 ~ τ . p ) ≡ ν a1 ~ τ . ? a2(x . p )
B.4 Actions
Actions also admit a statics, given by the judgment ⊢Σ α action.
⊢Σ α action
⊢Σ ε action
⊢Σ,a~τ e : τ
⊢Σ,a~τ a ! e action
⊢Σ,a~τ e : τ
⊢Σ,a~τ a ? e action
C Dynamics
C.1 Expressions
chref⟨a⟩ valΣ,a~τ
cmd[ τ ](m ) valΣ
C.2 Commands
bnd( e ; x . m )⇒
bnd( e′ ; x . m )
spawn( e )⇒
spawn( e′ )
emitref( e1 ; e2 )⇒
emitref( e′1 ; e2 )
e1 valΣ e2 7−−→
emitref( e1 ; e2 )⇒
emitref( e1 ; e
sync( e )⇒
sync( e′ )
C.3 Processes
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′, continued
run⟨a⟩(m ) ε7→
run⟨a⟩(m′ )
e valΣ,a~τ
run⟨a⟩( ret( e ) ) ε7→
run⟨a⟩( bnd( cmd[ τ ′ ](m1 ) ; x . m2 ) )
ν b ~ τ ′ . run⟨b⟩(m1 )⊗ ? b(x . run⟨a⟩(m2 ) )
run⟨a⟩( spawn( cmd[ τ ](m ) ) ) ε7→
Σ,a~chan( τ )
ν b ~ τ . run⟨b⟩(m )⊗ run⟨a⟩( ret( chref⟨b⟩ ) )
e valΣ,a~unit,b~τ
run⟨a⟩( emitref( chref⟨b⟩ ; e ) ) ε7→
Σ,a~unit,b~τ
! b( e )⊗ run⟨a⟩( ret( ⟨⟩ ) )
run⟨a⟩( sync( chref⟨b⟩ ) ) ε7→
? b(x . run⟨a⟩( ret(x ) ) )
run⟨a⟩( newchan⟨τ⟩( b . m ) ) ε7→
ν b ~ τ . run⟨a⟩(m )
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
Syntax and Semantics
Implementing the Dynamics
Execution Context
References
Reference Cells
Atomic References
Expressions
Structural Congruence
Expressions