Previous Contents Next

Chapter 1   Concurrent programming

This part of the manual is a tutorial introduction to the join-calculus. This chapter presents small, local, examples. Chapter 2 deals with the distributed features.

1.1   Conventions

Examples are given as join-calculus source, followed by the output of the compiler when enabled to print types. For instance, here is the definition of a simple top-level value binding:
# let x = 1
# ;;
val x : int
An example may span over several programs chunks. Here is another binding:
# let y = x+1
# ;;
val y : int
In the end, the output generated by the execution of the example is shown:
# spawn echo(y)
# ;;
-> 2
Therefore, to execute the example above, it suffices to concatenate the three source chunks above in some file a.j (erasing the ``#'' characters), then to compile a.j by the command jcc -i a.j, and finally to run the produced code by the command ./a.out. (Option -i enables the output of inferred types).

1.2   Basics

Join-calculus programs are made of processes and expressions. Roughly, processes are executed asynchronously and produce no result, whereas expressions are evaluated synchronously and their evaluation produces values. Processes communicate by sending messages on channels or port names. Messages carried by channels are made of zero or more values and channels are values themselves. By contrast with other process calculi (such as the pi-calculus and its derived programming language Pict), channels and the processes that listen on them are defined by a single language construct. This feature allows considering (and implementing) channels as functions, when channels are used as functions.

Join-calculus programs are first organized as a list of top-level statements. A Top-level statements is a binding (such as let x = 1 ;;), a process spawnings or an expression execution (see below).

1.2.1   Processes

Processes are the core syntactic class in the join-calculus. The most simple process sends a message on a channel. For instance, the standard library provides the channel echo, sending an integer i on echo prints i on the console. At top-level, processes are introduced by the keyword ``spawn''. Top-level phrases are terminated by an optional ;;.
# spawn echo(1)
# ;;
# 
# spawn echo(2)
# ;;
-> 12
Processes introduced by ``spawn'' are executed concurrently. The program above may either echo 1 then 2, or echo 2 then 1. Thus, the output above may be 12 or 21, depending on the implementation.

Concurrent execution also occurs inside processes, using the parallel composition operator ``|''. This provides a more concise, semantically equivalent, alternative to the previous example:
# spawn echo(1) | echo(2)
# ;;
-> 21
Composite processes also include conditionals (if's) and local binding (let...in's). Process grouping is done by using curly braces ``{'' and ``}''.
# spawn
#   let x = 1 in
#   {let y = x+1 in echo(y) | echo(y+1)} | echo(x)
# ;;
-> 231
Once again, the program above may echo the integers 1, 2 and 3 in any order.

1.2.2   Expressions

The other important syntactic class of the join-calculus is the class of expressions. By contrast with processes, expressions evaluate to some results.

At top-level, expressions are introduced by the keyword ``do''. Expressions also occur in the right-hand side of value bindings or as arguments to message sending. Apart from variables and constants, such as integers, the most simple expression sends some values on a synchronous channel. Synchronous channels return an answer, which is made of zero or more results. For instance, the standard library provides the synchronous channel print. When given a message consisting of one integer i, print outputs i on the console and returns an empty result, consisting of zero values, to its sender.
# let x = 1
# ;;
# do print(x)
# ;;
# do print(x+1)
# ;;
val x : int
-> 12
In the program above 1, x and x+1 are expressions whose evaluation returns a single value (here an integer). The expressions print(x) and print(x+1) return empty results. This makes sense with respect to synchronization: as top-level phrases are evaluated by following textual ordering, the program above first outputs 1 and then outputs 2.

Composite expressions are made of conditionals, value bindings and sequence. Thus one may write:
# do
#   let x = 1 in
#   print(x) ; print(x+1)
# ;;
-> 12
Sequences may also occur inside processes. The general form of a sequence inside a process is expression ;   process , where expression must return an empty result. As expression can itself be a sequence, composite sequences appear inside processes naturally. Thus, one may write:
# spawn
#   print(1) ; print(2) ; echo(3)
# ;;
-> 123
A sequence may terminate with the empty process that does nothing and is denoted by ``'', the empty sequence of characters. Thus, an alternative to the previous example is as follows:
# spawn
#   print(1) ; print(2) ; print(3) ;
# ;;
-> 123
Concrete syntax for processes and expressions are purposely similar, when not the same. A noticeable exception is grouping, which is expressed by curly braces ``{'' and ``}'' in the case of processes and by ordinary parenthesis ``('' and ``)'' in the case of expressions. Due to parser limitations, grouping is mandatory in the branches of an if process, i.e., one must write if expression then {   process 1 } else {   process 2 }.

1.2.3   Channels

Channels or port names are the main values of the join-calculus. The standard library already provides many port names, such as echo and print.

There are two important categories of port names: asynchronous and synchronous port names. Synchronous names (such as print) return values, whereas asynchronous channels (such as echo) do not. Therefore, message sending on synchronous channels occur inside expressions, whereas the message sending on asynchronous channels occur inside processes. The type-checker flags an error whenever a channel is used in the wrong context.
# do echo(1)
# ;;
File "ex11.j", line 1, characters 3-10:
Type error: This is not an expression with an empty result

jcc: Compilation failed for ex11.j
Users can create new channels with a new kind of let binding, which is not to be confused with ordinary value binding. The right hand-side of the definition of a channel a is a process that will be spawned whenever some message is sent on a. Additionally the message contents are bound to formal parameters. For instance, here is the definition of a stuttering echo channel:
# let echo_twice(x) = echo(x) | echo(x)
# ;;
val echo_twice : <int>
The new channel echo_twice has type <int>, this means that it accepts messages made of one integer. Sending an integer i on echo_twice fires an instance of the guarded process echo(x) | echo(x), where x is replaced by i. Such message sending is asynchronous in the sense that it is not possible to know when console output actually takes place.

The definition of a stuttering print is as follows:
# let print_twice(x) = print(x) ; print(x) ; reply
# ;;
val print_twice : <int> -> <>
As exposed by its type, print_twice is a synchronous port name that takes one integer as argument and returns an empty result. The type checker infers that print_twice is synchronous, thanks to the new reply construct whose semantics is to send back some (here zero) values as result. Message sending on print_twice is synchronous, in the sense that one knows that console output has occurred at the time when print_twice answers.
# spawn echo_twice(1)
# ;;
# 
# do print_twice(2)
# ;;
# 
# spawn echo_twice(3)
# ;;
-> 221133
Observe that, since processes execute concurrently, 221331 would also be a perfectly valid output. Printing both 2's before any 3 is the only constraint here, by the synchronous character of print_twice.

Channels are polyadic with respect to both arguments and results (when they exist). For instance, print accepts one argument and returns an empty result. Another example is the standard library channel +, that accepts two arguments and returns one result. The following channel f has arity two, both for argument and result, as shown by its type.
# let f(x,y) = reply x+y,y-x
# ;;
val f : <int * int> -> <int * int>
The type for f clearly shows its arities. Polyadic results are exploited by using polyadic value bindings. For instance the following program should print 3 on the console:
# let x,y = f(1,2)
# ;;
# 
# do print(x)
# ;;
val x : int
val y : int
-> 3
Synchronous names can be used to support a functional programming style. A traditional example is the Fibonacci function.
# let fib(n) =
#   if n <= 1 then {reply 1}
#   else {reply fib(n-1) + fib(n-2)}
# ;;
# 
# do print(fib(10))
# ;;
val fib : <int> -> <int>
-> 89
Note that, by contrast with value bindings, channel definitions are always potentially recursive.

Port names are first-class values in the join-calculus. They can be sent as messages on other port names and returned as results. As a result, higher order ``functions'' can be written.
# let twice(f) =
#   let r(x) = reply f(f(x)) in
#   reply r
# ;;
val twice : <<'a> -> <'a>> -> <<'a> -> <'a>>
The type for twice is polymorphic: it includes a type variable 'a that can be replaced by any type. Thus twice is a synchronous channel that takes a synchronous channel of type <'a> -> <'a> as argument and returns one result of the same type.

For instance, 'a can be the type of integers or the type of strings (^ is string concatenation):
# let succ(x) = reply x+1
# ;;
# 
# let double(s) = reply s^s
# ;;
# 
# do
#   let f = twice(succ)
#   and g = twice(double) in
#   print(f(0)) ; print_string(g("X"))
# ;;
val succ : <int> -> <int>

val double : <string> -> <string>
-> 2XXXX

1.2.4   Threads

Threads are not part of the join-calculus language, but they are part of the implementation. Threads are some kind of execution units at the implementation level. Threads are created, may suspend then resume, and finally die. Threads match the intuition of a ``direct'' causality. For instance, all the printing actions in a sequence are to be executed one after another and clearly belong to an unique thread. By contrast, the parallel composition operator ``|'' separates two threads that execute independently.

More precisely, the following program creates three threads:
# spawn
#   {print(1) ; print(2) ; print(3) ;} |
#   {{print(4) ;} |
#     print(5) ; print(6) ;}
# ;;
-> 561234
The output of the program is a mix of the output of its three threads: 123, 4 and 56. An output such as 12, then 4, then 356 would reveal that the thread printing 1, 2 and 3 has been preempted before printing 3.

Sending messages on channels ultimately fires a new process and should thus create a new thread. However, a new thread is not always created. For instance, compare the following definitions that create infinitely many threads and one, never dying, thread:
# let rabbit() = print_string("+") ; rabbit() | rabbit ()
# ;;
# 
# let forever() = print_string("-") ; forever() ; forever() ; reply
# ;;
val rabbit : <>

val forever : <> -> <>
Sending a message on asynchronous rabbit, fires a small thread that terminates spawning two new instances of rabbit, thus creating two other thread. By contrast, sending a message on synchronous forever blocks the sender thread until the thread fired by the message completes. The implementation takes advantage of this: it does not fire a new thread and executes the process guarded by forever() on the sender thread. Here, message sending results in an ordinary function call.

This implementation behavior is exposed by the following program:
# spawn
#   {rabbit()} |
#   {print_newline () ; failwith("over !!!")} |
#   {forever() ;}
# ;;
-> -------------------
-> jcrun a.out: failwith over !!! (from runtime.ml)
The program concurrently starts three threads: first, a failwith(...) thread that flushes pending output and kills the system; then, two crazy threads, rabbit() and forever().

Considering processes only, the program may terminate after an unspecified number of -'s and +'s has been printed. Considering threads, more -'s than +'s should appear on the console, since all -'s are printed by the same thread, whereas +'s are printed by different threads. All these printing threads compete for scheduling with the lethal thread and the forever() thread has to be preempted to stop outputting.

As a conclusion, informal reasoning about threads helps predicting program output, taking the implementation into account. What is predicted is likely output and not correct output.

1.3   Modules

The current implementation of the join-calculus supports a simple module system. This provides a clean access to library routines. Additionally, users may structure their programs in several modules, which can be written and compiled separately.

1.3.1   Names from the library

The standard library provides a lot of pre-defined names. The library is made of modules. Inside programs the name x from the module mod is accessed as a qualified name mod.x. For instance, the library module ml gives access to basic operations from the implementation, including operations on floating point numbers (such as conversion, output functions and the exponentiation exp).
# let one = ml.float_of_string("1.0")
# ;;
# 
# do ml.print_float(ml.exp(one))
# ;;
val one : ml.float
-> 2.71828182846
An alternative to qualifying names from modules is ``opening'' modules. Opened modules are searched by the compiler when it discovers a name that is not bound locally.
# open ml
# ;;
# 
# let one = float_of_string("1.0")
# ;;
# 
# do print_float(exp(one))
# ;;
val one : ml.float
-> 2.71828182846
The compiler starts with module sys opened, so that the primitives print, print_string, +, ...are in fact sys.print, sys.print_string, sys.+, ...

Primitives can be seen as (synchronous) port names in one important aspect: users send messages to them and get results from them. However, there is one important difference: primitives are not first class values. As such, primitives cannot be used on their own, they must be applied to their arguments.
# let duplicate_arg(f,x) = reply f(x,x)
# ;;
# 
# do print(duplicate_arg(+,2))
# ;;
File "ex25.j", line 4, characters 23-24:
this is an external primitive: sys.+
jcc: Compilation failed for ex25.j
Primitive are not first class values, mainly for implementation reasons : the execution of primitive is compiled as an instruction and there is no port name here. A simple workaround is to create a port name that simply calls the primitive.
# let duplicate_arg(f,x) = reply f(x,x)
# ;;
# 
# let plus(x,y) = reply x+y
# ;;
# 
# do print(duplicate_arg(plus,2))
# ;;
val duplicate_arg : <<'a * 'a> -> <'b> * 'a> -> <'b>

val plus : <int * int> -> <int>
-> 4

1.3.2   User defined modules

Modules are not restricted to the standard library. Users can create their own modules, compile them separately and link them together into an executable program. For instance, users may write a module stutter, that exports two channels echo and print. Ideally, users first specify the names exported by module stutter and their types, by writing an interface file stutter.ji.
# val echo : <int>
# val print : <int> -> <>
The interface stutter.ji is compiled by issuing the command jcc stutter.ji. This produces an object interface file stutter.jio.

Then, the implementation file stutter.j contains the actual definitions for stutter.echo and stutter.print.
# let echo(x) = async.echo(x) | async.echo(x)
# 
# let print(x) = sys.print(x) ; sys.print(x) ; reply
The implementation file stutter.j is compiled by issuing the command jcc -c stutter.j (-c is the compile-only, do-not-link option). This produces an object implementation file stutter.jo.

Now that the module stutter is properly compiled, some other implementation file user.j can use it.
# do stutter.print(1)
# ;;
# 
# spawn stutter.echo(2) | stutter.echo(3)
# ;;
The implementation file user.j can be compiled into user.jo by issuing the command jcc -c user.j. An executable a.out is produced by the command jcc stutter.jo user.jo that links the modules stutter and user together. Alternatively, a.out can be produced in one step by the command jcc stutter.jo user.j.

Running a.out may produce the following output:
-> 112233
See sections 3.9 and 7.3 for a more thorough description of modules.

1.4   Join-patterns

Join patterns significantly extend port name definitions. A join-pattern defines several ports simultaneously and specifies a synchronization pattern between these co-defined ports. For instance, the following source fragment defines two synchronizing port names fruit and cake:
# let fruit(f) | cake(c) =
#   {print_string(f^" "^c) ; print_newline() ; }
# ;;
val fruit : <string>
val cake : <string>
To trigger the guarded process {print_string(f^" "^c) ; print_newline() ;}, messages must be sent on both fruit and cake.
# spawn fruit("apple") | cake("pie")
# ;;
-> apple pie
The parallel composition operator ``|'' appears both in join-patterns and in processes. This highlights the kind of synchronization that the pattern matches.

Join-definitions, such as the one for fruit and cake, provide a simple mean to express non-determinism.
# spawn fruit("apple") | fruit("raspberry") | cake("pie") | cake("crumble")
# ;;
-> raspberry pie
-> apple crumble
Two cake names must appear on the console and both possible combinations of different fruits and cake types are correct.

Composite join-definitions specify several synchronization patterns.
# let apple() | pie() = print_string("apple pie") ;
# and raspberry() | pie() = print_string("raspberry pie") ;
val apple : <>
val raspberry : <>
val pie : <>
Observe that only three names apple, raspberry and pie are defined. Thus, pie potentially takes part in two synchronizations.

Again, internal choice is performed when only one invocation of pie is present:
# spawn apple() | raspberry() | pie()
# ;;
-> apple pie
Join-patterns are the key programming paradigm in the join-calculus. They allow the encoding of many data structures, which can be used concurrently. For instance, the following source fragment defines a counter:
# let count(n) | inc() = count(n+1) | reply to inc
# and count(n) | get() = count(n) | reply n to get
# ;;
# 
# spawn count(0)
# ;;
val inc : <> -> <>
val count : <int>
val get : <> -> <int>
This definition calls for two remarks. First, when a join-pattern defines several names, some of which are synchronous, the reply construct must now specify the name to which it replies. Hence the new reply ... to name construct.

Second, the usage of the name count above is a typical way of ensuring mutual exclusion. For the moment, assume that there is at most one active invocation on count . When one invocation is active, count holds the counter value as a message and the counter is ready to be incremented or examined. Otherwise, some operation is being performed on the counter and pending operations are postponed until the operation being performed has left the counter in a consistent state. As a consequence, the counter may be used consistently by several threads.
# spawn {inc () ; inc () ;} | {inc() ;}
# ;;
# 
# let wait() =
#   let x = get() in
#   if x < 3 then {wait()} else {
#     print_string("three is enough !!!") ; print_newline() ;
#   }
# ;;
# 
# spawn wait()
# ;;
val wait : <>
-> three is enough !!!
Ensuring the correct counter behavior in the example above requires some programming discipline: only one initial invocation on count has to be made. If there are more than one simultaneous invocations on count, then mutual exclusion is lost. If there is no initial invocation on count, then the counter will not work at all. This can be avoided by making the count, inc and get names local to a create_counter definition and then by exporting inc and get while hiding count, taking advantage of lexical scoping rules.
# let create_counter() =
#   let count(n) | inc0() = count(n+1) | reply to inc0
#   and count(n) | get0() = count(n) | reply n to get0 in
#   count(0) | reply inc0,get0
# ;;
# 
# let inc,get = create_counter()
# ;;
val create_counter : <> -> <<> -> <> * <> -> <int>>

val inc : <> -> <>
val get : <> -> <int>
This programming style is reminiscent of ``object-oriented'' programming: a counter is a thing called an object, it has some internal state (count and its argument) and exports some methods to the external world (here, inc and get). The constructor create_counter creates a new object, initializes its internal state and returns the exported methods. As a consequence, several counters may now coexist.

1.5   Control structures

Join-pattern synchronization expresses many programming paradigms, either concurrent or sequential.

1.5.1   Control structures for concurrency

Locks

Join-pattern synchronization can be used to emulate simple locks.
# let new_lock() =
#   let free() | lock() = reply to lock
#   and unlock() = free() | reply to unlock in
#   free() | reply lock,unlock
# ;;
val new_lock : <> -> <<> -> <> * <> -> <>>
Threads try to acquire the lock by performing a synchronous call on channel lock. Due to the definition of lock(), this consumes the name free and only one thread can get a response at a time. Another thread that attempts to acquire the lock is blocked, until the thread that got the lock releases it by the synchronous call unlock that fires another invocation of free.

To give an example of lock usage, we introduce channels that output their string arguments several times:
# 
# let double(p) =
#   let r(s) = p(s) ; p(s) ; reply in
#   reply r
# ;;
# 
# let print_port(s) = print_string(s) ; reply
# ;;
# 
# let print16 = double(double(double(double(print_port))))
# ;;
val double : <<'a> -> <>> -> <<'a> -> <>>

val print_port : <string> -> <>

val print16 : <string> -> <>
Now consider two threads, one printing -'s, the other printing +'s.
# spawn {print16("-") ;} | {print16("+") ;}
-> ++++++----------------++++++++++
As threads execute concurrently, their outputs may mix, depending upon scheduling.

Using a lock to delimit a critical section, -'s and +'s do not mix anymore.
# let lock,unlock = new_lock()
# ;;
# 
# spawn
#   {lock() ; print16("-") ; unlock() ;} |
#   {lock() ; print16("+") ; unlock() ;} 
# ;;
# 
val lock : <> -> <>
val unlock : <> -> <>
-> ++++++++++++++++----------------

Barriers

A barrier is another synchronization mechanism. Basically, barriers define synchronization points in the execution of concurrent threads. Here is a simple barrier that synchronizes two threads only:
# let join1() | join2() = reply to join1 | reply to join2
# ;;
val join1 : <> -> <>
val join2 : <> -> <>
Note that the definition above includes two reply constructs.

The following two threads print ba or ab between matching parenthesis:
# spawn
#   {print_string("(") ; join1() ; print_string("a") ; join1() ;
#    print_string(")") ;} |
# 
#   {join2() ; print_string("b") ; join2() ;}
# ;;
-> (ba)

Bi-directional channels

Bi-directional channels are found in many process calculi, such as the pi-calculus for instance. In the pi-calculus, given a channel c, a value v can be sent asynchronously on c (written c![v]) or received from c and bound to some variable x in some guarded process P (written c?x.P). All processes can both send and receive on the channels they know. By contrast, join-calculus processes that know a channel can only send messages on it. The receiver process is defined at the same time as the channel and is therefore unique. Finally, the scope of a pi-calculus channel name c is defined by the new c in P operator. Such an operator does not exist in the join-calculus, since join-definitions are binding constructs.

Bi-directional channels can be defined in the join calculus as follows:
# let new_pi_channel() =
#   let send(x) | receive() = reply x to receive in
#   reply send,receive
# ;;
val new_pi_channel : <> -> <<'a> * <> -> <'a>>
A pi-calculus channel is implemented by a join definition with two port names. The port name send is asynchronous and is used to send messages on the channel. One of these messages is received by making a synchronous call to the other port name receive. Now let us ``translate'' the following pi-calculus process:
new c,d in c![1] | c![2] | c?x.d![x+x] | d?y. print(y))

We get:
# spawn
#   let sc,rc = new_pi_channel()
#   and sd,rd = new_pi_channel() in
#   sc(1) |  sc(2) |  {let x = rc() in sd(x+x)} |
#   {let y = rd() in print(y) ;}
# ;;
-> 4
Observe that, by contrast with the join-calculus semantics of receptors, the process that performs x+x runs only once.

Synchronous pi-calculus channels are encoded just as easily as asynchronous ones: it suffices to make send synchronous:
# let new_pi_synch_channel() =
#   let send(x) | receive() = reply x to receive | reply to send in
#   reply send,receive
# ;;
val new_pi_synch_channel : <> -> <<'a> -> <> * <> -> <'a>>

1.5.2   Loops

Join-patterns are also useful for expressing various programming control structures. A simple control structure is iteration on some integer interval.

Simple loops

Asynchronous loops can be used when the execution order of iterated actions is irrelevant.
# let loop(a,x) = if x > 0 then {a() | loop(a,x-1)}
# ;;
# 
# let echo_star() = print_string("*") ;
# ;;
# 
# spawn loop(echo_star,5)
# ;;
val loop : <<> * int>

val echo_star : <>
-> *****
When execution order matters, asynchronous loops do not work. Since iterated actions are performed concurrently. Here, a synchronous loop is preferred.
# let loop(a,x) = if x > 0 then {a(x) ; loop(a,x-1) ; reply} else {reply}
# ;;
# 
# let print_int(x) = print(x) ; print_string(" ") ; reply
# ;;
# 
# do loop(print_int,5)
# ;;
val loop : <<int> -> <> * int> -> <>

val print_int : <int> -> <>
-> 5 4 3 2 1 
When a synchronous loop produces a result, this result can be computed inside reply constructs and returned. The following example computes the sum of the squares of the integer between 1 and 32:
# let sum(i0,f) =
#   let iter(i) =
#     if i > 0 then {reply f(i)+iter(i-1)} else {reply 0} in
#   reply iter(i0)
# ;;
# 
# let square(x) = reply x*x
# ;;
val sum : <int * <int> -> <int>> -> <int>

val square : <int> -> <int>
# do print(sum(32,square))
# ;;
-> 11440
Port name definitions such as the one for iter above belong to a functional programming style. In particular, the various iterations of the loop body (computing f(i) here) never execute concurrently, since iterations are performed one after the other.

However, since integer addition is associative and commutative, the summing order of the various f(i) does not matters. Thus, asynchronous iteration can be used here. Then, we get a program with much more opportunities for concurrent execution:
# let sum(i0,f) = 
# 
#   let add(dr) | total(r,i) =
#     let r' = r+dr in
#     if i > 1 then {reply total(r',i-1) to total}
#     else  {reply r' to total} in
# 
#   let loop(i) = if i > 0 then {add(f(i)) | loop(i-1)} in
#   loop(i0) | reply total(0,i0)
# ;;
# 
# do print(sum(32,square))
# ;;
val sum : <int * <int> -> <int>> -> <int>
-> 11440
Observe how loop result is accumulated using the synchronous name total. The argument to the reply to sum consists in one call to total. This trick enables the synchronous sum to return its result when the asynchronous loop is over. In fact, replying directly to sum from inside the sub-definition for add(dr) | total(r,i) is rejected by the compiler:
# let sum(i0,f) = 
# 
#   let add(dr) | total(r,i) =
#     let r' = r+dr in
#     if i > 1 then {total(r',i-1)}
#     else  {reply r' to sum} in
# 
#   let loop(i) = if i > 0 then {add(f(i)) | loop(i-1)} in
#   loop(i0)
# ;;
# 
File "ex49.j", line 6, characters 23-26:
continuation outside of its scope: sum
jcc: Compilation failed for ex49.j
The current compiler enforces strong restriction on where to place reply constructs, see section 7.4.

Distributed loops

Sharing a loop between several ``agents'' requires more work. Let us informally define an agent as some computing unit. In this section, an agent is represented by a synchronous channel. In a more realistic setting, different agents would reside on different computers. The agent paradigm then serves to allocate computing resources (see section 2.3.3 in the next chapter).

For instance, here are two agents square1 and square2. The agent square1 modelizes a fast machine, whereas square2 modelizes a slow machine by computing squares in a uneficient way. Additionally, square1 and square2 differ marginally by their console output: square1 outputs a +, while square2 outputs a * when it starts and a - just before answering.
# let square1(i) = print_string("+") ; reply i*i
# ;;
# 
# let square2(i) =
#    print_string("*") ;
#    let total(r) | wait() = reply r to wait in
#    let mult(r,j) =
#      if j <= 0 then {total(r)} else {mult(r+i,j-1)} in
#    mult(0,i) |
#    let r =  wait() in
#    print_string("-") ; reply r
# ;;
val square1 : <int> -> <int>

val square2 : <int> -> <int>
Sharing a loop between several agents is allocating the iterations to be performed to them. The following channel make_sum, returns a register channel and a wait channel. An agent registers by sending its computing channel on register. The final loop result is returned on wait.
# let make_sum(i0) = 
# 
#   let add(dr) | total(i) =
#     if i > 1 then {reply dr+total(i-1) to total}
#     else  {reply dr to total}
#   and  wait() = reply total(i0) to wait in
# 
#   let loop(i) | register(f) =
#     if i > 0 then {add(f(i)) | loop(i-1) | register(f)} in
# 
#   loop(i0) | reply register,wait
# ;;
val make_sum : <int> -> <<<int> -> <int>> * <> -> <int>>
The only difference with the asynchronous sum loop from the previous section resides in the replacement of the definition let loop(i) = ... by the join-pattern definition let loop(i) | register(f) = .... As a consequence, the agents square1 and square2 may now compete for loop iterations, provided two invocations register(square1) and register(square2) are active.
# let register,wait = make_sum(32)
# ;;
# 
# spawn register(square1) | register(square2)
# ;;
# 
# do print(wait())
# ;;
val register : <<int> -> <int>>
val wait : <> -> <int>
-> +*+*+*+*+*+*+*+*+*+*+*+*++**+*+*----------------11440
The distributed loop above is not satisfactory, since it does not take the relative computing speed of square1 and square2 into account while allocating iterations. The add(f(i)) jobs are spawned asynchronously, so that the different iterations performed by a given agent are executed concurrently. As a result, the iteration space is partitioned evenly between square1 and square2, as illustrated by the output above. This leads to a poor load balance, since the fast square1 stands idle at the end of the loop, while the slow square2 is overwhelmed.

A better solution is for an an agent to execute its share of work in sequence rather than concurrently. This is achieved by the slightly modified definition for loop(i) | register(f) below:
# let make_sum(i0) =
# 
#   let add(dr) | total(i) =
#     if i > 1 then {reply dr+total(i-1) to total}
#     else  {reply dr to total} in
# 
#   let  wait() = reply total(i0) in
# 
#   let loop(i) | register(f) =
#     if i > 0 then
#       {loop(i-1) |
#       let r = f(i) in
#       add(r) | register(f)} in
# 
#   loop(i0) | reply register,wait
# ;;
val make_sum : <int> -> <<<int> -> <int>> * <> -> <int>>
In the new definitions, register(f) is launched again only once f(i) is computed. By contrast, loop(i-1) is launched immediately, for another agent to grab the next iteration as soon as possible.
# let register,wait = make_sum(32)
# ;;
# 
# spawn register(square1) | register(square2)
# ;;
# 
# do print(wait())
# ;;
val register : <<int> -> <int>>
val wait : <> -> <int>
-> +*++++++++++++++++++++++++++++++-11440

1.6   Data structures in the join-calculus

1.6.1   Simple data structures

Polymorphic pairs can be encoded quite easily in the join-calculus by taking advantage of port name arity.
# let create(x,y) =
#   let get() = reply x,y in
#   reply get
# ;;
val create : <'a * 'b> -> <<> -> <'a * 'b>>
As exposed by the type above, a pair is a synchronous port name that takes zero arguments and returns two values. The synchronous name create returns such a name when given the values to store in the pair.

The content of a pair can be retrieved by sending a message of arity zero on it:
# let fst(p) = let x,y = p() in reply x
# and snd(p) = let x,y = p() in reply y
# ;;
val fst : <<> -> <'a * 'b>> -> <'a>
val snd : <<> -> <'a * 'b>> -> <'b>
Pairs can now be used in an ``abstract'' fashion, by considering only the constructor create and the two destructors, fst and snd:
# let p = create(1,"coucou")
# ;;
# let x = fst(p) and s = snd(p)
# ;;
# do print(x+string.length(s))
# ;;
val p : <> -> <int * string>

val x : int
val s : string
-> 7
An alternative to encoding data structures in the join-calculus is using data structures from Objective Caml. For instance, the standard library provides a module pair:
# open pair
# ;;
# 
# let p =  create(1,"coucou")
# ;;
# let x = fst(p) and s = snd(p)
# ;;
# do print(x+string.length(s))
# ;;
val p : (int, string) ml.pair

val x : int
val s : string
-> 7
The type of pairs is now ('a,'b) ml.pair, emphasizing the abstract character of pairs. Nothing is known about the concrete structure of pairs, implementation details for pairs being local to the implementation of the standard library module pair. This is in sharp contrast with the type of encoded pairs: <> -> <'a * b'>, which unveils much of the encoding.

1.6.2   Data structure encoding by object-oriented style

A convenient programming style for expressing data structures in the join-calculus is the so-called object-oriented style. An object has an internal, hidden, state and exports some methods, (here some synchronous names) that operate on its internal state. Consider for instance the following encoding for lists:
# let cons (h,t) =
#   let head () = reply h
#   and tail () = reply t
#   and self () = reply false,head,tail in
#   reply self
# and nil () =
#   let  head () = reply failwith ("head of nil")
#   and  tail () = reply failwith ("tail of nil")
#   and self () = reply true,head,tail in
#   reply self
# ;;
val cons : <'a * 'b> -> <<> -> <bool * <> -> <'a> * <> -> <'b>>>
val nil : <> -> <<> -> <bool * <> -> <'a> * <> -> <'b>>>
The internal state of a list cell is an emptiness status (true or false), plus, when appropriate, two subcomponents (h and t). The emptiness status is exposed directly to the external world. The two methods head and tail give access to the subcomponents of a non-empty list cell or fail. Observe how the name self is introduced to pack methods together in the reply to cons and nil. Finally, the types for the results of nil and cons are the same. Hence, both kinds of list cells are values of the same type.

List can now be used by directly retrieving methods:
# let list_concat(l) =
#   let n,h,t = l() in
#   if n then {reply ""}
#   else {
#     reply h()^list_concat(t())
#   }
# ;;
val list_concat :
  <'a> -> <string> where 'a = <> -> <bool * <> -> <string> * <> -> <'a>>
The above type is recursive. This reflects the fact that lists are recursive data structures. More precisely, the type of the cons-cell creator cons was not recursive. However, the recursive type for lists of strings appears naturally when writing a function that traverses lists.

Finally, the following source fragment shows how to create and use string lists:
# let replicate(elem,n) =
#   if n <= 0 then {reply nil()}
#   else {
#    reply cons(elem,replicate(elem,n-1))
#   }
# ;;
# 
# do print_string(list_concat(replicate("X",16)))
# ;;
val replicate :
  <'a * int> -> <'b> where 'b = <> -> <bool * <> -> <'a> * <> -> <'b>>
-> XXXXXXXXXXXXXXXX

1.6.3   Mutable data structures

Object states, represented as join-patterns, can be altered by invoking the appropriate methods. Here is a definition for a reference cell. One method (get) examines the content of the cell, while another (put) alters it.
# let create_ref(y0) =
#   let state(y) | get() = state(y) | reply y to get
#   and state(y) | put(new_y) = state(new_y) | reply to put in
#   state(y0) | reply get,put
# ;;
val create_ref : <'a> -> <<> -> <'a> * <'a> -> <>>
Here, the internal state of a cell is its content, its is stored as a message y on the channel state. Lexical scoping is used to keep the state internal to a given cell.

# let gi,pi = create_ref(0)
# and gs,ps = create_ref("")
# 
val gi : <> -> <int>
val pi : <int> -> <>
val gs : <> -> <string>
val ps : <string> -> <>

1.6.4   Elaborate data structure: a concurrent fifo

We are now ready for a more sophisticated example of data structure encoding in the join-calculus. First we define a new kind of list cells. Such a cell always holds an element (x below). When created, it stands in the first position of a list, and a name (see first below) reflecting that status is activated. Then, when another element is cons-ed is front of the list, a cell additionally holds a pointer to this previous element (see the pattern first() | set_prev(prev) below). In the end, a cell can be destroyed (see kill below), it then returns both its content, a pointer to the previous cell (when it exists), and a boolean, which is set to true, when the destroyed cell is the only one in the list.
# let new_cell (x) =
#   let first() | set_prev(prev) = inside(prev) | reply to set_prev
#   and inside(prev) | kill () = reply x,prev,false to kill
#   and first()      | kill () = reply x,self,true to kill
#   and self() = reply set_prev,kill in
#   first() | reply self to new_cell
# ;;      
val new_cell :
  <'a> -> <'b> where 'b = <> -> <<'b> -> <> * <> -> <'a * 'b * bool>>
A fifo is a data structure that provides two methods put and get. The method put stores its argument in the fifo, while the method get retrieves one element from the fifo. The internal state of the fifo is either empty (and then the name Empty is activated), or it contains some elements (internally, non-empty fifos have the name state activated). The name state holds two arguments: fst is a pointer to the first cell of the element list, while lst is a pointer to the last cell of the element list. Thus, elements stored in the fifo are cons-ed in front of fst (see put below), while retrieved elements are taken from the end of the element list (see get below). There is no Empty() | get() pattern below. As a consequence, an attempt to retrieve an element from an empty fifo is not an error: answering to get is simply postponed until the fifo fills in.

# let fifo() =
#   let Empty() | put(x) =
#     let fst = new_cell(x) in
#     state(fst,fst) | reply to put
#   and state(fst,lst) | put(x) =
#      let new_fst = new_cell(x) in
#      let set,rem = fst() in
#      set(new_fst) ;
#      state(new_fst,lst) |
#      reply to put
#   and state(fst,lst) | get () =
#      let set,rem = lst() in
#      let x,prev,last_cell = rem () in
#      if last_cell then {Empty()} else {state(fst,prev)} |
#      reply x to get in
#   Empty() | reply put,get to fifo
# ;;   
val fifo : <> -> <<'a> -> <> * <> -> <'a>>
From the fifo point of view, elements are retrieved in the order they are stored. In a concurrent setting this means that when a thread performs several get in a row, the retrieved elements come in an order that is compatible with the order in which another thread feeds the fifo.
# spawn
#   let put,get = fifo() in
#  {print(get()) ; print(get()) ; print_newline() ;} |
#  {let x = get () and y = get () in } |
#  {put(1) ; put(2) ; put(3) ; put(4);}
# ;;
-> 34
Therefore, the program above prints two integers from the set {1, 2, 3, 4} in increasing order.

1.7   A word on typing

The join-calculus type system is derived from the ML type system and it should be no surprise to ML programmers. The key point in typing la ML is parametric polymorphism. For instance, here is a polymorphic identity function:
# let id(x) = reply x
# ;;
val id : <'a> -> <'a>
The type for id contains a type variable ``'a'' that can be instantiated to any type each time id is actually used. Such a type variable is a generalized type variable.

For instance, in the following program, variable ``'a'' is instantiated successively to int and string:
# let i = id(1) and s = id("coucou")
# ;;
# 
# do print(i) ; print_string(s)
# ;;
val i : int
val s : string
-> 1coucou
In other words, the first occurrence of id above has type <int> -> <int>, while the second has the type <string> -> <string>.

Experienced ML programmers may wonder how the join-calculus type system achieves mixing parametric polymorphism and mutable data structures. There is no miracle here. Consider, again, the join-calculus encoding of a reference cell:
# let state(x) | get() = state(x) | reply x to get
# and state(x) | set(new_x) = state(new_x) | reply to set
val get : <> -> <'_a>
val state : <'_a>
val set : <'_a> -> <>
The type variable ``'_a'' that appears inside the types for state, get and set is prefixed by an underscore ``_''. Such type variables are non-generalized type variables that are instantiated only once. That is, all the occurrences of state must have the same type. Moreover, once ``'_a'' is instantiated with some type, this type replaces ``'_a'' in all the types where ``'_a'' appears (here, the types for get and set). This wide-scope instantiation guarantees that the various port names whose type contains ``'_a'' (state, get and set here) are used consistently.

More specifically, if ``'_a'' is instantiated to some type int, by sending the message 0 on state. Then, the type for get is <> -> <int> in the rest of the program, as shown by the type for x below. As a consequence, the following program does not type-check and a runtime type-error (printing an integer, while believing it is a string) is avoided:
# let state(x) | get() = state(x) | reply x to get
# and state(x) | set(new_x) = state(new_x) | reply to set
# ;;
# 
# spawn state(0)
# ;;
# 
# let x = get()
# ;;
# 
# do print_string(x)
# ;;
val get : <> -> <'_a>
val state : <'_a>
val set : <'_a> -> <>

val x : int

File "ex70.j", line 12, characters 3-15:
Type error (Call): this expression has type
<string> -> <>
but is used with type
<int> -> '_b

jcc: Compilation failed for ex70.j
Non generalized type variables appear when the type of several co-defined port names share a type variable. Such a type variable is not generalized.
# let port(p) | arg(x) = p(x)
val port : <<'_a>>
val arg : <'_a>
A workaround is to encapsulate the faulty names into another port name definition that defines only one name. This restores polymorphism.
# let make_it() =
#   let port(p) | arg(x) = p(x) in reply port,arg
# ;;
val make_it : <> -> <<<'a>> * <'a>>
Non-generalized type variables also appear in the types of the identifiers defined by a value binding.
# let p1,a1 = make_it()
# ;;
# 
# let p2,a2 = make_it()
# ;;
# 
# spawn p1(echo) | p2(echo_string) | a1(1) | a2("coucou")
# ;;
val p1 : <<'_a>>
val a1 : <'_a>

val p2 : <<'_b>>
val a2 : <'_b>
-> 1coucou
It is interesting to notice that invoking make_it() twice produces two different sets of port and arg port names, whose types contain different type variables. Thereby, programmers make explicit the different type instantiations that are performed silently by the compiler in the case of generalized type variables.

Non-generalized type variable sometimes are a source of nuisance, when the compiler unexpectedly rejects programs, see section 7.4 for details.
Previous Contents Next