This repository contains the type checker, interpreter and compiler for language CLASS - a session-typed, higher-order, core language that supports concurrent computation with shared linear state, and which is described in detail in Safe Session-Based Concurrency with Shared Linear State.
The source code builds on the artifact of The Session Abstract Machine (Artifact). The compiler was developed by Ricardo Antunes for his thesis "Efficient Compilation for the Linear Language CLASS".
This work is licensed under a Creative Commons Attribution 4.0 International License.
CLASS code can be compiled through the ./compile.sh bash script. To pass flags to the CLASS compiler, the CLLS_FLAGS environment variable can be set. Flags can be passed to GCC through the C_FLAGS variable. To learn more about the script options, run ./compile.sh.
A full list of compiler options can be obtained by passing --help in CLLS_FLAGS.
To validate the compiler implementation, a suite of tests was built, which can be found at ./tests.
The tests can be run with ./test_compiler.sh. Extra flags can be passed through the C_FLAGS and CLLS_FLAGS environment variables.
The artifact consists of type checker and interpreter for language CLASS,
written in Java. It demonstrates the feasibility of our design and, pragmatically,
validates and guides the development of many complex programs:
we code inductive datatypes using either primitive recursion or using System-F style
encodings, linked data structures (e.g. linked lists, binary search trees),
shareable concurrent mutable ADTs (e.g. stacks, counters,
imperative queues and buffered channels), resource synchronisation methods
(e.g. fork-join barriers, dining philosophers, and Hoare-style monitors)
and several test suites.
In particular, all the examples presented in the paper are validated by the implementation. In the following list, we map all the examples in the paper to the corresponding files in the artifact:
- flag, presented in pp. 4, is in examples/state/flag.clls.
- toggle, presented in pp. 17-18, is in examples/state/toggle.clls.
- linked list, presented in pp. 18-19, is in examples/state/linked-lists.clls.
- buffered channel, presented in pp. 19-20 is in directory examples/state/buffered-channel. This directory contains three files, namely: server.clls, in which we define ADT operations on the server side; client.clls, in which we define the operations on the client side; and tests.clls, that defines a series of tests. This is the organisation used for the remaining shared mutable ADTs.
- dining philosophers, presented in pp.20-21, is in examples/state/dining-philosophers.clls.
- barrier, presented in pp. 21-22, is in examples/state/barrier.clls.
- Hoare-style monitor, presented in pp.22-23, is in examples/state/hoare-monitor.clls.
When presenting the examples in the paper we did some simplifications in the code for the purpose of presentation.
We will now present the commands to interact with the REPL and the concrete syntax of the implementation language. We conclude with some final remarks.
The REPL expects the following top-level commands:
1. type id(X1,...,Xn){ A };;
2. type rec id(X1,...,Xn){ A };;
3. type corec id(X1,...,Xn){ A };;
4. proc id<X1,..., Xn>(x1:A1, ... xm:Am ; y1:B1, ..., yk:Bk){ P };;
5. proc rec id<X1,..., Xn>(x1:A1, ... xm:Am ; y1:B1, ..., yk:Bk){ P };;
6. proc unsafe_rec id<X1,..., Xn>(x1:A1, ... xm:Am ; y1:B1, ..., yk:Bk){ P };;
7. P;;
8. trace P;;
9. include "filename";;
10. quit;;
Command (1): top level type definition.
Defines (if it kindchecks) the (possibly) parametric type A with name id and parameters X1, ... Xn ( n >= 0).
Example: when executing
type Fun(a,b) { recv ~ a; b };; we obtain
Type Fun: defined.
Command (2) and (3) are similar to (1) but allows inductive (mu X. A) and coinductive (nu A. A) type definitions, respectively.
For example,
type rec Nat{
choice of {
|#Z: close
|#S: Nat
}
};;
proc zero(n:Nat){
#Z n; close n
};;
defines the inductive session type of the natural numbers and
process zero(n) that encodes the natural zero on session n.
(4) Defines (if it typechecks) the (possibly) parametric process with name id with linear parameters x1:A1,..., xm:Am (m >0) and unrestricted (exponential) parameters y1:B1,..., yk:Bk (k>=0).
The process is typechecked as defined by the typing judgment
P |- x1:A1,..., xm:Am ; y1:B1,..., yk:Bk
Example: if we type in the REPL
proc id<a>(f:Fun(a,a))
{
recv f (x:~a);fwd x f
}
;;
we obtain
Process id: defined.
Command (5) is same as (4) but allows corecursive process definitions, e.g.:
proc rec double(n:~Nat, m:Nat)
{
case n of {
|#Z: wait n; zero(m)
|#S: cut{ double(n,k) |k:~Nat| #S m; #S m; fwd m k }
}
};;
defines a corecursive process that doubles natural n and outputs the answer on m.
The type checker ensures each that corecursive call is done in a
session that hereditarily descends from the corecursion parameter.
Command (6) allows to define an unsafe corecursion definition, in which the hereditary check of (5) is turned off.
Commands (7) and (8) type check process P in the current environment given by prior definitions and execute it, (8) with tracing enabled.
Example: if we input in the REPL
cut { id<lint>(f)
|f:~Fun(lint,lint)|
send f (10);
println "here is "+f;
()
};;
we obtain the log:
here is 10
Command (9) includes and processes all the commands included in the specified file. Filename are given as strings.
Example: include "examples/state/stack/tests.clls";;.
Command (10) quits the REPL.
By convention, we use the filename extension .clls for files written in the
implementation language.
Single-line comments are written as follows
//this is a single-line comment
whereas multiple-line comments are written as
/*
this is
a multiple-line
comment
*/
proc test0() {
println (2); ()
};;
proc test2() {
cut {
close n
| n : wait |
wait n; println ("done!"); ()
}
};;
proc test2() {
ccut {
send n (p. close p); close n
| n : recv wait; wait |
recv n(x:wait); wait x; wait n; ()
}
};;
The concrete syntax of types is given by::
A,B ::=
lint |
colint |
lbool |
colbool |
lstring |
colstring |
close |
wait |
send A; B | ( A (x) B )
recv A; B | ( A (p) B )
choice of {|#l1:A1 | ... |#ln: An} | ( (+){|#l1:A1 | ... |#ln: An} )
offer of {|#l1:A1 | ... | #ln:An} | ( &{|#l1:A1 | ... |#ln: An} )
!A |
?A |
sendty X; A | ( Exists X. A )
recvty X; A | ( Forall X. A )
affine A | (/\ A)
coaffine A| (\/ A)
state A | (Sf A)
usage A | (Uf A)
statel A | (Se A)
usagel A | (Ue A)
{ A } |
id<T1,...,Tk>(A1,...,An)
The correspondence to the types of the paper are written in parenthesis.
Except for the basic type constants, concrete types correspond to the types
described in the paper. We have basic type constants for linear integers
lint, linear booleans lbooland linear strings lstring, as well as their
dual colint, colbool and colstring. Unrestricted versions of
these types may be defined using ! and ? type constructors.
Choice label identifiers must start by a hash character#.
The concrete syntax of process terms is given by::
P, Q ::=
print M; P |
println M; P |
if M { P }{ Q } |
let x M |
let! x M |
id<A1, ... , An>(x1, ..., xm) |
() |
par {P || Q } |
share x { P || Q } |
fwd x y |
cut { P |x:A| Q } |
close x |
wait x; Q |
case x of {|#l1:P1 | ... | #ln:Pn} | #li;Pi |
send x(y:A. P); Q |
recv x(y:A);Q |
!x(y:A);P |
call x(y:A);P | ?x; P |
sendty x(A);P | recvty x(X);P |
send x(M);P |
affine x; P |
use x; P |
discard x |
take x(y:A);P |
put x(y:A. P); Q |
put x(M);P |
cell x(y:A. P) |
cell x(M) |
release x |
Construct id<A1,..., An>(x1,.. ; .,xm) spawns the
defined process id with type arguments "A1,..., An
and channel name arguments x1,..; .,xm. The ; in the
argument list separates the linear parameters from the unrestricted
parameters, according to the definition of id.
Except for the first five lines, which refer to expressions for basic datatypes, described in more detail below, all the constructs of the concrete process syntax are the fundamental ones introduced in our paper.
Access to affine (via use process construct) and exponential names (via why-not ? process construct) is inferred by our type checker, so it does not need to be explicitly indicated.
Process print M ; P prints message M and continues as P. Process
println M;P prints message M, starts a newline, and continues as P.
Process if M { P } { Q } evaluates boolean expression M. If the result
is true, it continues as P. Otherwise, the result is false and it
continues as Q. We support ML-style let-bindings. Construct let x M
binds expression M to channel x to be used linearly (type as either
lint, lbool or lstring). Construct let! x M binds expression M
to channel x to be used persistently (typed as either !lint, !lbool or
!lstring).
The concrete syntax of basic value expressions is given by::
M :: = n | true | false | str | x | (M) |
-M | M + M | M - M | M * M | M / M |
!M | M and M | M or M |
M == M | M != M | M < M | M > M
where n is any integer, true and false denote the boolean constants,
str is any string and x is an identifier. We support the usual arithmetic operations
of negation, addition, subtraction, multiplication and division. We support
the boolean constructs of logical negation !, logical and and logical or.
We can compare two expressions for value equality == and non-equality !=.
We can compare two integers with the usual relational operators "<" and ">".
The operator of addition + is overloaded: we can concatenate two string
expressions, obtaining a string. We can also concatenate a string with an
integer expression, in which case, the integer is first converted to a string.
We also provide support for expressions in the constructs send, cell and put:
send x(M);P cell x(M) put x(M);P
The elaboration phase of our interpreter expands this in the basic language before typechecking,.
For convenience, our concrete syntax supports multi-ary par and multi-ary cut (which are abbreviations of the expected associative composition of par and cut).
par {P1 || ... || Pn}
cut { P1 |x1:A1| ... |xn:An| Pn+1}
Multi-ary cut associates (conventionally) to the right.
In our concrete process syntax terms are written with bound names type-annotated, which from a pragmatic point of view guides the type checking algorithm and eases the task of writing programs. Currently, inference of annotations is provided, so that only parameters in process definitions and cut bound names need to be explicitly type annotated.
The supported language also includes pragmatic extensions (native basic datatypes int, boolean and string), that may be anyway encoded in our the fundamental linear logic based language using recursive/corecursive session types.
The type checker deals with the multiplicatives by lazy context splitting. The interpreter uses java.util.concurrent.* , using primitives such as fine-grained locks and condition variables to emulate the synchronous interactions of CLASS sessions and a cached thread pool to manage the life cycle of short-lived threads. Cell deallocation is implemented by reference counting, incremented on each share and decremented on each release. Forwarding redirects the clients of a shared cell through a chain of forwarding pointers.