Message passing lies at the heart of SePi. This section introduces the notions of channels, types for channels, sending and receiving messages, and selecting and offering choices. We concentrate on linear channels.
All that SePi does is to exchange messages. Messages are exchanged on
channels. If c denotes a channel, then to send integer 3 on c,
we write c!3; the exclamation mark, !, denotes output. SePi
counts with a few primitive channels, allowing to interact with the
console. Channel printInteger is used to write integer values on the
console. Try this:
printInteger!3
To print two integer values, one may send two messages to the console,
that is, we printInteger!3 and then we printInteger!7. The
sequencing operator is ., at the left of which we find one message
send, and on the right the 'rest of the program'.
printInteger!3.
printInteger!7
The console should read 37. If somehow you want to distinguish the
values coming from different messages, you are faced with different
choices. Channel printIntegerLn behaves as printInteger only that
it inserts a newline after printing the value. Try:
printIntegerLn!3.
printInteger!7
Alternatively, one may compose the two integer values in a single
string and print it. The ++ operator concatenates two strings, after
converting its arguments to strings. To print a string we use primitive
channel printString or printStringLn. Try:
printString!("first: " ++ 3 ++ ", second: " ++ 7)
SePi is equipped with six builtin channels on which we can only write.
printBooleanprintBooleanLnprintIntegerprintIntegerLnprintStringprintStringLnValues comprise the boolean values literals (false and true), the integer literals (..., -1, 0, 1, ...), and the string literals (sequences of characters enclosed in quotes; the usual escape sequences are available, including \n and \t).
The primitive operators in reverse binding order are the following.
orand==, /=<, <=, >=, >+++, -*, /, %-, notParenthesis may be used in expressions to circumvent the operator precedence above. Parenthesis are not mandatory when the argument to a message is an expression, but they help reading the code. One can write
printInteger!7+3
or
printInteger(7+3)
both will parse.
Exercise. Write a process that prints the truth table for the boolean conjunction. Use boolean operators and the and operator; use \t to align the entries. Try a solution with one (long) message only, and a solution with four separate messages. You should obtain a table of the following form:
false false false
false true false
false false false
true true true
In order to receive messages, one needs a channel on which one may read. Since there is no primitive channel from which one may read from (in SePi one cannot read from stdin), we must create a channel for the effect. We start by creating a channel on which a string must be exchanged. SePi channels are synchronous, bi-directional, and defined by their two end points.
By synchronous we mean that SePi is equipped with a non-buffered, rendez-vous, operational semantics: both the read and the write operations are blocking; once a reader and a writer are available, a value is transmitted, and both processes advance.
Bi-directional implies that channels may be used in both directions, that is, to write and to read messages (for the same channel end, and in turn).
Finally, defined by its two end points mean that there are separate identifiers for each of the channel ends.
Here's how we declare a new channel:
new readerEnd writerEnd: ?string.end
Identifier readerEnd denotes the channel end on which processes may
read; identifier writerEnd is the channel end on which processes may
write. Whatever one process writes on writerEnd may be read by
another process on clientEnd. Channel end readerEnd is of type
?string.end, a type that allows a string to be read and then allows
no further interaction. The exclamation mark, ?, denotes input;
type end denotes a channel on which messages cannot be exchanged.
Conversely, writerEnd is of type !string.end, a type that allows a
string to be written (question mark, !, denotes output) and then
allows no further interaction on the channel end.
We may then setup the writer process. The writer is a process that must write a string on channel writerEnd, and then terminate.
writerEnd!"Hello world!"
We then setup the reader process. The reader is a process that reads a
string from channel readerEnd and then prints it on the console.
readerEnd?x. printString!x
Finally, the parallel composition operator, denoted by the vertical
bar |, lets two processes run in parallel. Here is the whole code
together, so that you may run it:
new readerEnd writerEnd: ?string.end
writerEnd!"Hello world!" |
readerEnd?x. printString!x
You may have noticed that the question mark means input, both at the
type level, as in ?string, and at process level, as
inreaderEnd?x. Likewise, the exclamation mark means output both at
the type level (!integer) and at the process level
(printInteger!3). Finally, the dot denotes sequencing both at the
type level and at the process level. This is no coincidence. Types and
programs must be always aligned.
Exercise. Write a program that exchanges an integer value of your choice. The receiver then prints true if the value is positive, and false otherwise.
Suppose now that the two strings, Hello and world!, are to be
exchanged on separate, but consecutive, messages on the same channel.
The writer process is as follows.
writerEnd!"Hello". writerEnd!"world!"
Notice that the two messages are joined by a dot, denoting that the
Hello message is to be delivered before world!. The writer process
collects the two strings and prints them together, using the string
concatenation operator, ++.
readerEnd?x. readerEnd?y. printString!(x++" "++y)
What is the type for the writerEnd-readerEnd channel? In this case
we need a channel able to exchange two messages, both of type
string, after which no further interaction is possible. The type of
this channel will look different if seen from side of the writer or
that of the reader. The type of the channel, as it is presented to the
writer, is !string.!string.end. Its dual, that is, the type of the
channel as presented to the reader is ?string.?string.end.
Putting everything together we get the following program.
new writerEnd readerEnd: !string.!string.end
writerEnd!"Hello". writerEnd!"world!" |
readerEnd?x. readerEnd?y. printString!(x++" "++y)
Exercise. Write a program that exchanges two integer values on a channel. The reader then prints the sum on the console.
Exercise. Write a program that exchanges two boolean values. The reader prints in the console the conjunction and the disjunction of the two values.
We have seen that channel declaration takes the form new x y: T,
where x and y are two identifiers denoting the two ends of the
newly created channel and T is a type. So we have two identifiers
and one type. Is T the type of x, that of y, or of both?
Identifiers x and y have different types, for a channel will
present different behaviours depending on which end it is observed
from. If one end allows for an input operation (?), the other
expects an output (!), and vice versa. If the type of x is
?string.end, then that of y is !string.end. In SePi, a
declaration
new x y: ?string.end
is equivalent to
new y x: !string.end
so that the answer to the above question is: T is the type of x,
the first identifier in the declaration. In general, a declaration
new x y: T is equivalent to new y x: U, where U is a type dual
to T. We will revisit duality in Section More on Types.
SePi is equipped with a conventional if-then-else process. For example, a process that receives two integer values and prints the maximum of these on the console can be written as follows
reader?x. reader?y.
if x > y
then printInteger!x
else printInteger!y
The whole program, so that you can run it, is as follows. ```sepi|load new writer reader: !integer.!integer.end
writer!4. writer!9 | reader?x. reader?y. if x > y then printInteger!x else printInteger!y ```
Exercise. Adapt the program above so that it prints the maximum of three integer values.
The channels we have met so far only operate in one direction. This
need not be the case. Imagine a process that accepts two integer
values and returns the minimum and the maximum of them. A client to this process writes two consecutive integers, and then reads
another two integers, that is, the client is of type
!integer.!integer.?integer.?integer.end. The channel declaration is as
follows.
new client server: !integer.!integer.?integer.?integer.end
The code for the client outputs two integer values, say 5 and 7,
inputs two integer values (on variables x and y), and then prints
both.
client!5. client!7.
client?x. client?y.
printString!("min: " ++ ", max: " ++ y)
Conversely, the code for the server, inputs two integer values (on variables u and v), and writes another two integer values.
server?u. server?v.
if u > v
then server!u. server!v
else server!v. server!u
Putting everything together, so that you may run it, yields the below code.
new client server: !integer.!integer.?integer.?integer.end
client!5. client!7.
client?x. client?y.
printString!("min: " ++ x ++ ", max: " ++ y)
|
server?u. server?v.
if u > v
then server!u. server!v
else server!v. server!u
We can do more than input followed by output or output followed by
input. In fact, input and output can be freely mixed. And we may mix
messages of different kinds, say, integer and boolean. Suppose
that after output min-max, the server accepts a further integer value
and then outputs true if the new integer (strictly) lies between the
two other, that is, given x, y, and z, the server outputs the
truth value of expression x<z and z<y. In this case the type of the
channel, as seen from the side of the client, is
!integer.!integer.?integer.?integer.!integer.?boolean.end. The code
for the client may extend that introduced above:
client!5. client!7.
client?x. client?y.
printString!("min: " ++ x ++ ", min: " ++ y).
client!3.
client?b.
printString!(", lies between: " ++ b)
The code for server can also be adapted as follows.
server?u. server?v.
if u > v
then
server!u. server!v.
server?w.
server!(u<w and w<u)
else
server!v. server!u.
server?w.
server!(u<w and w<v)
Putting everything together we get the following running program.
new client server:
!integer.!integer.?integer.?integer.!integer.?boolean.end
client!5. client!7.
client?x. client?y.
printString!("min: " ++ x ++ ", min: " ++ y).
client!3.
client?b.
printString!(", lies between: " ++ b)
|
server?u. server?v.
if u > v
then
server!u. server!v.
server?w.
server!(u<w and w<u)
else
server!v. server!u.
server?w.
server!(u<w and w<v)
Exchanging one value at a time may lead to rather lengthy code. Rather
than sending 5 and 7 in two separate messages, one may send the
pair (5,7) in a single message. In turn, the reader may read two
values in a go, using the pattern (x,y). The type of the channel
must be adapted in order to accommodate the change; we now need a
channel of type !(integer,integer)?(integer,integer).end. The
min-max program may be more concisely written as follows.
new client server: !(integer,integer).?(integer,integer).end
client!(5,7).
client?(x,y).
printString!("min: " ++ x ++ ", max: " ++ y)
|
server?(x,y).
if x > y
then server!(x,y)
else server!(y,x)
Exercise. Write a program whose server reads two boolean values, and replies its conjunction and disjunction. Try minimising the number of messages exchanged.
Exercise. Write a program that reads two integer values and returns its product and whether this is positive (a boolean value). Try minimising the number of messages exchanged.
Suppose that we are interested in computing a few math operations. For
example, the maximum of two integer values, and testing for zero. Surely that we could setup two different
servers at two different channels, one for the max, the other for
the isZero operation. But we do want a single server to serve all
our math operations.
The types for each operation are easy to write. One is of the form
!integer.!integer.?integer.end, the other !integer.?boolean.end,
both as seen from the client's point of view. To compose them we write
+{max: !integer.!integer.?integer.end, isZero:
!integer.?boolean.end}. The + type constructor denotes a choice as
exerted by the client. A process interacting on a channel governed
by such a type must first select option max or isZero. If option
max is selected, then twointeger values must be sent, and an
integer received. If, on the other hand, option isZero is
selected, then an integer must be sent and a boolean value
received.
First we declare the channel:
new client server :
+{max: !integer.!integer.?integer.end,
isZero: !integer.?boolean.end}
Then we setup a client. To select an option on a channel, we use the
select process constructor:
client select isZero.
client!5.
client?b.
printBooleanLn!b
Each client selects exactly one option. The server, on the other hand,
must offer both. The & type constructor denotes a choice
as offered by the server. If a server accepts the max option, then
it must receive two integer values, and return an integer value. If,
on the other hand, the server receives the isZero option, the it
must accept an integer and output a boolean value. The type of the
server is thus &{max: ?integer.?integer.!integer.end, isZero:
?integer.!boolean.end}, obtained by dualising each type operator: !
becomes ? and vice-versa, + becomes & and vice-versa, and end remains as is. The above
channel declaration could have been equivalently written as follows (notice that we have exchanged the order of the identifiers server and client).
new server client :
&{max: ?integer.?integer.!integer.end,
isZero: ?integer.!boolean.end}
Now for the server. We have seen it must offer two choices; we use the
case-of process constructor for the effect.
case server of
max ->
server?x. server?y.
if x>y then server!x else server!y
isZero ->
server?x.
server!(x==0)
Putting everything together so that you may run it:
new client server :
+{max: !integer.!integer.?integer.end,
isZero: !integer.?boolean.end}
client select isZero.
client!5.
client?b.
printBooleanLn!b
|
case server of
max ->
server?x. server?y.
if x>y then server!x else server!y
isZero ->
server?x.
server!(x==0)
Exercise. Write a client that tests whether -5 is greater or equal than 3 using the math server.
Exercise. Add an abs operation to the math server.
The above client is given the choice of calling a max or an isZero
operation; then it terminates. Wouldn't it be nice to allow clients to
call as many operations as they wish, in a single session? We want a client that, after completing one operation (max or
isZero), is given the choice of selecting another (or the same)
operation. For this we require a recursive type, so that we can go
back to the beginning. We take the chance to introduce a third option,
quit, which we use to abandon the interaction. The type of the
channel, as seen from the client point of view, becomes rec a.
+{max: !integer.!integer.?integer.a, isZero: !integer.?boolean.a,
quit: end}.
Recursive types tend to be quite long. Type declarations may turn the code a little more readable. Rather then writing:
new client server:
rec a. +{max: !integer.!integer.?integer.a,
isZero: !integer.?boolean.a,
quit: end}
we may give a name to the type of the math server and then use it to declare our channels.
type mathClient = +{
max: !integer.!integer.?integer. mathClient,
isZero: !integer.?boolean. mathClient,
quit: end}
new client server : mathClient
Clients can now interact multiple times with the math server. The last
selection must always be quit, leaving the channel at type end.
// First try the isZero operation
client select isZero. client!5. client?b.
printStringLn!"Got "++b++"!".
// Then the max operation
client select max. client!-5. client!3. client?n.
printStringLn!"This time got "++n+"!".
// Invoke the isZero operation again
client select isZero. client!-3. client?b.
printStringLn!"And now "++b++"!".
// And finally quit the interaction
client select quit
Exercise. Write a client that tests whether the max of two numbers is zero, using a math client channel. For the time being you will only be able to write the client part of the code (and thus the program will not compile).
The math server, when governed by a recursive type above, needs to
continuously offer the max and the isZero options. Such behaviour
cannot be achieved with a finite composition of the primitives we have
seen so far. We need some form of unbounded behaviour, which SePi
provides in the form a def process.
We start by writing the math server type as seen from the server side; contrast with the mathClient type defined above.
type mathServer = &{
max: ?integer.?integer.!integer. mathServer,
isZero: ?integer.!boolean. mathServer,
quit: end}
The serverLoop process definition below is a form of input (?) that survives interaction, that is, after receiving a message (containing a math server channel end) executes its body, while providing a copy of itself to answer subsequent messages.
Because process definitions are (persistent or replicated) inputs, they are invoked with the exact same syntax used for message sending (for example, serverLoop!server). Message serverLoop!s in the body of a definition constitutes a recursive call. To launch the server we need a message from the "main" program that starts the loop. This is achieved with a message serverLoop!server after the definition.
def serverLoop s: mathServer =
case s of
max ->
s?x. s?y.
if x>y then s!x else s!y.
serverLoop!s
isZero ->
s?x.
s!(x==0).
serverLoop!s
quit ->
printStringLn!"Done!"
serverLoop!server
Putting everything together so that you may run it:
type mathServer = &{
max: ?integer.?integer.!integer. mathServer,
isZero: ?integer.!boolean. mathServer,
quit: end}
// The client-server channel
new server client: mathServer
// The client
client select isZero. client!5. client?b.
printStringLn!"Got "++b++"!".
client select max. client!-5. client!3. client?n.
printStringLn!"This time got "++n++"!".
client select isZero. client!-3. client?b.
printStringLn!"And now "++b++"!".
client select quit |
// The server definition
def serverLoop s: mathServer =
case s of
max ->
s?x. s?y.
if x>y then s!x else s!y.
serverLoop!s
isZero ->
s?x.
s!(x==0).
serverLoop!s
quit ->
printStringLn!"
// Launch the server
serverLoop!server
Notice that a process definition is supposed to be followed by the "rest of the program".
Exercise. Write a client that invokes the server an unbounded
number of times. Hint: try the technique we used for the server, for
example alternating between invoking the max and the isZero
operations (but never selecting quit). To see such a code running
use the Eclipse IDE or the command line, not the web server (see Section Processes That
Run Forever).
dualof type operatorIt should be clear by now that the 'client' and the 'server' notions exist only in the head of the programmer. Because of the continuous interaction session types provide us with, freely mixing input and output, what is now a client soon becomes a server.
Yet, when we declare a channel, we must decide on a type T for the
new x y : T declaration. Shall we pick that of the server or that of
the client? (or perhaps better, that of the process that starts as a
client or the one that starts as a server?). Either is valid in SePi
(cf. Section Two Channel Ends, One Type Declaration). It
is perhaps a good idea to be consistent. I usually choose the client
side, the one that starts with an output or selection.
Unfortunately, in the example in Section Servers That Serve More Than One Request, i forgo the discipline. Suppose than that we want to start our code as follows.
type mathClient = +{
max: !integer.!integer.?integer. mathClient,
isZero: !integer.?boolean. mathClient,
quit: end}
When it comes to declare that channel, we first write the client side:
new client server: mathClient
But the process definition serverLoop requires a math-server type,
and we do not have this type anymore, because we decided to declare instead the type of the client. Certainly, we could write the mathServer type by dualising all the operators in the mathClient type (as in
Section Servers That Serve More Than One Request), but this is
a tedious and error prone task. Fortunately, the type of the server
can be easily obtained from that of the client: the dualof type
operator does just that. Using this operator, the signature of the
server loop becomes def serverLoop s: dualof mathClient.
Here's the whole code, rewritten using the dualof operator, so that you
may try it.
type mathClient = +{
max: !integer.!integer.?integer. mathClient,
isZero: !integer.?boolean. mathClient,
quit: end}
new client server: mathClient
client select isZero. client!5. client?b.
printStringLn!"Got "++b++"!".
client select max. client!-5. client!3. client?n.
printStringLn!"This time got "++n++"!".
client select isZero. client!-3. client?b.
printStringLn!"And now "++b++"!".
client select quit
|
def serverLoop s: dualof mathClient =
case s of
max ->
s?x. s?y.
if x>y then s!x else s!y.
serverLoop!s
isZero ->
s?x.
s!(x==0).
serverLoop!s
quit ->
printStringLn!"Done!"
serverLoop!server
Types must be taken very seriously. If the type of some channel promises "output an integer; then input a string; then end", the code must fulfil the promise. In particular,
There must be code that, sequentially, outputs an integer, then inputs a string, and then uses the channel no more, and
There must be code that, sequentially, inputs an integer, then outputs a string, and then uses the channel no more.
The following piece of syntax does not fulfil the server's (y)
promise, and is thus not accepted as SePi code.
new x y : !integer.?boolean.end
x!1.x?b | y?z.y!5
The problem in this case is a simple type mismatch: y promised to send a boolean value (after receiving an integer), but instead sends an integer value.
The below code presents a problem of a different nature: y "forgot" to send the final boolean value. This leads to a deadlocked situation where thread x will forever be waiting for the promised boolean value.
new x y : !integer.?boolean.end
x!1.x?b | y?z
Similarly, the following syntax does not fulfil the client's (x)
promise; it leaves thread y indefinitely trying to send a boolean value.
new x y : !integer.?boolean.end
x!1 | y?z.y!true
Sometimes (more often than not), we want servers to serve multiple clients. The servers we have seen so far can only serve a single client. Conversely, the clients above can only be served by a single server. This section shows how to circumvent this problem.
SePi does not accept as valid the following code.
new c s : !integer.end
c!1 | c!2 | s?x
Similarly, the following code using multiple readers is not allowed in SePi.
new c s : !integer.end
c!1 | s?x | s?y
Why is this so? One the one hand it would introduce a race condition leading to non-determinism:
output c!1 could interact with either input s?x or s?y. More
important is perhaps the fact that allowing such behaviour may lead to
erroneous situations. In order to understand the problem we need a
more complex example. Consider the following piece of syntax,
new c s : !integer.!boolean.end
c!1.c!true | c!2.c!false | s?x.s?y.printBoolean!y
and suppose that c!1 goes first. After one reduction step, we get:
new c s : !integer.!boolean.end
c!true | c!2.c!false | s?y.printBoolean!y
Now two things can happen: either c!true or c!2 goes
forward. Suppose the second happens. We obtain something that is not
supposed to happen: writing a integer value on the printBoolean
channel:
new c s : !integer.!boolean.end
c!true | c!false | printBoolean!2
So the problem seems to lie in channels that mix messages of two
different sorts, integer and boolean in this case. What if channels
always exchange messages of the same kind? Consider the following
piece of syntax.
new c s : !integer.!integer.end
c!1.c!5 | c!2.c!6 | s?x.s?y.printInteger!x+y
In this case nothing goes wrong, except perhaps for the fact that two of the four messages will not be served. And we do not want this: all messages on linear channels should be delivered and all servers on linear channels should be invoked (cf. Section Servers and clients that do not fulfil their obligations).
The bottom line is that channels in SePi are linear by default. In
fact, a type !integer.!boolean.end abbreviates
lin!integer.lin!boolean.end. We have made the lin qualifier
optional, for it is the most common case. A linear channel type must
have exactly one writer and one reader. The end type is always shared.
Contrary to linear channels, shared channels must exhibit the same behaviour, always. In order to
describe the type of a shared (or unrestricted) channel, we use the un qualifier (un
for un restricted). Unlike lin, which is optional, un is
obligatory (it could not be otherwise).
Shared channels are meant to be used by multiple (that is, zero or more) clients and multiple servers. In the previous section we have seen that, in order to avoid type mismatches problems, shared channels must always exhibit the "same" protocol: output an integer once, output an integer forever. This means that, after an un!integer, there must be another un!integer, followed by an un!integer, followed by ...
Fortunately we have recursive types.
Let us play a little with unrestricted channels. Try this code:
type ForeverUnOutInt = un!integer.ForeverUnOutInt
new client server : ForeverUnOutInt
{}
The {} is a block of zero processes running in parallel. The code compiles. When run it produces no behaviour. All a shared channel requires is that there is zero or more processes reading on the channel and zero or more writers writing on the channel, which is the case.
We can have two clients and one server:
type ForeverUnOutInt = un!integer.ForeverUnOutInt
new client server : ForeverUnOutInt
client!5 |
client!7 |
server?x. printStringLn!"Got " ++ x
In this case one client will not be served. And we can have two servers and one client:
type ForeverUnOutInt = un!integer.ForeverUnOutInt
new client server : ForeverUnOutInt
client!5 |
server?x. printStringLn!"Server 1 got " ++ x |
server?y. printStringLn!"Server 2 got " ++ y
In this case one client will not be invoked. We can also have as many servers as clients.
type ForeverUnOutInt = un!integer.ForeverUnOutInt
new client server : ForeverUnOutInt
client!5 |
client!7 |
server?x. printStringLn!"Server 1 got " ++ x |
server?y. printStringLn!"Server 2 got " ++ y
Exercise. What are the possible outcomes when running the code above?
Interaction on shared channels may be issued from parallel threads, as in the code above, or sequentially, as in:
type ForeverUnOutInt = un!integer.ForeverUnOutInt
new client server : ForeverUnOutInt
client!5.
client!7 |
server?x. printStringLn!"Server 1 got " ++ x.
server?y. printStringLn!"Server 2 got " ++ y
Exercise. What are the possible outcomes in this case? Compare to the situation with parallel threads above.
Unrestricted types are always equivalent to types of the form rec a.un!T.a or to
rec a.un?T.a (where a does not occur in T). For example, the type ForeverUnOutInt we have been using is an abbreviation for rec a.un!integer.a. The pattern is so
common that SePi provides two powerful abbreviations: *!T and *?T. For example, the type ForeverUnOutInt could be simply written *!integer.
What if we need to exchange, on a shared channel, not one but two (or
more) values of different types? We know that rec
a.un!integer.!un.boolean.a is not a valid type, because two messages
of different types are sent separately. But we can send them together,
atomically, in a pair, as in the following code. No interference in this case.
new c s : *!(integer,boolean)
c!(1,false) |
c!(2,true) |
s?(n,b). printString!"("++n++","++b++")"
We have seen that the lin qualifier is optional. On the other hand, most of the needs for shared channels can be written with the * syntax. We thus see that we seldom need to explicit mention qualifiers lin and un.
Exercise. What are the possible outcomes of the below code? Is 52 a possible output?
new c s : *!integer
c!1. c!5 |
c!2. c!6 |
s?x. printInteger!x. s?y. printInteger!y
In the previous section we played with a fixed number of clients and servers. Suppose that we want to write a server that repeatedly receives two integers and prints their sum. We have seen that the two integers must be sent in pair. We have also seen that, in order to write processes with an unbounded behaviour we must use process definitions, def. So here is a server that servers zero or more clients, together with two clients.
def sumLoop c : *?(integer, integer) =
c?(x,y). printIntegerLn!x+y. sumLoop!c
new client server : *!(integer, integer)
client!(5,7) |
client!(3,1) |
sumLoop!server
Suppose now that we want to adapt the above code in such a way that the server, rather than printing, replies back the sum of the two integers received. We would like to write a type:
type SumServer = un?(integer,integer). !integer. SumServer
but this is not a valid SePi type. Processes using such types may end up in erroneous situations, for example using channel printBoolean to write an integer value (cf. Section Linear channels).
Let us pause for a moment and think of a related problem. We have seen that, in order to send two values on a shared channel, we have to send them in pairs, as in *!(integer,boolean), that is as un!(integer,boolean).un!(integer,boolean)..., and not as un!integer.un!boolean.un!integer.un!boolean....
What if SePi did not allow to transmit pairs? How do we send a pair of values on a shared channel in such a way that we interference is avoided? Specifically we want to make sure that two values, sent on separate messages, reach the same server (in the order they were sent), and conversely, that servers get two values (on separate messages) from the same client. And, of course, there may be many clients and many servers competing for the same (shared) channel.
Towards this end, we take advantage of two features, both available on SePi:
Essentially, we create a new linear channel (with a "pair" protocol in this case) that we send on the shared channel. We need:
type OutPair = lin!integer.lin!integer.end
type PairClient = *!OutPair
new client server : PairClient
Then, the session initiation procedure works as follows. The server creates a new (linear) channel:
new writer reader : OutPair
and sends the reader end on the shared channel:
new writer reader : OutPair
server!writer...
The client, on the other hand, reads the linear channel:
client?c...
At this point the client and the server possess a linear channel on which two integer values may be sent, without fear of interaction. Then the server reads two integer values:
...reader?x. reader?y. printInteger!x+y
and the client sends two integer values on the channel just received
...c!5.c!7
The whole code looks as follows.
type OutPair = lin!integer.lin!integer.end
type PairServer = *!OutPair
new server client : PairServer
// Server
new writer reader : OutPair
server!writer. reader?x. reader?y. printInteger!x+y |
// Client
client?c. c!5. c!7
Session initiation is only interesting in the presence of more than one client or more than one server. Here is an example with three servers and two clients.
type OutPair = lin!integer.lin!integer.end
type PairServer = *!OutPair
new server client : PairServer
// Servers
{new writer reader : OutPair
server!writer. reader?x. reader?y. printInteger!x+y} |
{new writer reader : OutPair
server!writer. reader?x. reader?y. printInteger!x+y} |
{new writer reader : OutPair
server!writer. reader?x. reader?y. printInteger!x+y} |
// Clients
client?c. c!5. c!7 |
client?c. c!3. c!9
In this example not all servers will be invoked, but what is important
is that the various messages (5, 7, 3, 9) do not get mixed
up. If, say, the second server manages to receive 3, then both the
3 and the 9 will be received by the second server (in this order). It is not possible for a server to receive, say 3 and 5.
Also notice the usage of braces to delimit the scope of the various writer-reader channels, so that we may cut&paste to replicate servers. A more appropriate approach would have been to use a def for code reuse.
This technique is fundamental in bridging the linear and the shared world, and goes by the name of session initiation.
Exercise.
Rewrite the above example with three servers using a process definition, def.
Exercise. Session initiation does not need to be started at the server side. Rewrite the above program in such a way that clients start the process.
Now we can go back to the problem we left open at the end of the previous section. We leave it as an exercise.
Exercise. Write a shared server that receives a pair of integers and replies its sum.
Session initiation is so common that SePi provides a special syntax for it.
The server of the previous section looks line this:
new writer reader : OutPair
server!writer.// use the reader end; do not touch the server end again
After sending the reader end the server cannot use it anymore; linearity obliges. We then may hide the writer identifier by "creating" the channel directly on the output message:
server!(new reader : dualof OutPair).// use the reader end
Notice that the type of the reader end of the newly created channel
is lin?integer.lin?integer.end, that is, the dual of OutPair. Here's the whole code, so that you may run it.
type OutPair = lin!integer.lin!integer.end
type PairServer = *!OutPair
new server client : PairServer
// Server
server!(new reader : dualof OutPair).
reader?x. reader?y. printInteger!x+y |
// Clients
client?c. c!5. c!7 |
client?c. c!3. c!9 |
client?c. c!7. c!1
Let us now apply the idea of session initiation to write a math server able to handle multiple (that is, zero or more clients.
So, how can a math server serve multiple clients? It must be located on a shared channel. But shared channels do not allow the rich interaction required for the service. As before, we use the ability to create new channels to generate new linear channels that we transmit on the shared channel. We need:
type MathSession =
+{max: !integer.!integer.?integer.end,
isZero: !integer.?boolean.end}
un channel end that clients (and servers)
share:type MathServer = *?MathSession
new client server : MathServer
Using session initiation, the code for the client
is easy to set up. For example a client interested in the isZero
operation interacts with the server as follows.
// client is a shared channel end
client?c. // c is a linear channel end
// There will be no interference on channel c
c select isZero. c!-7. c?b. printBooleanLn!b
The server code is a little more complex. Basically, it creates a new channel, sends one end (that of the client) on the shared channel and then interacts on the server's end. We take advantage of the special syntax for session initiation, in order to write more compact code:
server!(new s : dualof MathSession).
case s of
max -> s?x. s?y. if x>y then s!x else s!y
isZero -> s?x. s!x==0
We can now place in parallel as many servers and clients as we may wish. Here's a version with two servers and three clients, where we use a process definition for code reuse. One of the clients will not be served, necessarily. But this is acceptable since clients wait on shared channels, and there is no service guarantee on shared channels.
type MathSession =
+{max: !integer.!integer.?integer.end,
isZero: !integer.?boolean.end}
type MathServer = *?MathSession
new client server : MathServer
def serverProc () =
server!(new s : dualof MathSession).
case s of
max -> s?x. s?y. if x>y then s!x else s!y
isZero -> s?x. s!x==0
serverProc!() |
serverProc!() |
client?c. c select isZero. c!-7. c?b. printBooleanLn!b |
client?c. c select max. c!3. c!9. c?n. printIntegerLn!n |
client?c. c select isZero. c!0. c?b. printBooleanLn!b
What if we want to make sure that all clients will eventually be
served? One possibility is to turn process definition serverProc
into a loop, similarly to what we did in Section
Servers that serve more than one request. The code looks as
follows. In this case all three clients get served.
type MathSession =
+{max: !integer.!integer.?integer.end,
isZero: !integer.?boolean.end}
type MathServer = *?MathSession
new client server : MathServer
def serverProc () =
server!(new s : dualof MathSession).{
serverProc!() | // and only then recur
case s of
max -> s?x. s?y. if x>y then s!x else s!y
isZero -> s?x. s!x==0
}
// Launch the server
serverProc!() |
// and the three clients
client?c. c select isZero. c!-7. c?b. printBooleanLn!b |
client?c. c select max. c!3. c!9. c?n. printIntegerLn!n |
client?c. c select isZero. c!0. c?b. printBooleanLn!b
Exercise. Discuss the need for braces in the body of the
serverProc process definition.
Exercise. Enrich the example above to allow clients to perform more than one operation per session. That is, use the recursive session type introduced in Section Servers that serve more than one request. You will need a second process definition for the server loop, again as in Section Servers that serve more than one request. The two definitions (the server process and the server loop) maybe nested or placed one after the other. Try both approaches.
The point where the recursive call is inserted is quite important. In
the serverProc example we have chosen to recur only after session
initiation, that is, after the acceptance of message server!c by the
client. In this way we guarantee that the program terminates once all
clients are served.
A common mistake is to perform the recursive call right at the beginning of the process definition, as in
def serverProc () =
serverProc!().
server!(new s : dualof MathSession).
case s of
...
or in the beginning but in parallel with other operations, as for example:
def serverProc () = {
serverProc!() |
server!(new s : dualof MathSession).
case s of
...
}
In this case clients will still be served but the server itself will never terminate, creating more and more copies of itself, getting ready for clients that will never come.
If you are using the web service, you'll experience a "Connection timeout" and no output. If you are using Eclipse or the command line you'll see the output but the interpreter does not halt. In Eclipse, press the red (stop) button at the console; if the interpreter is running from the command line, type Control-c.
Here is a summary of the situations we have addressed.
Races. Not possible with linear channels (violations detected by the type system). Possible (and often welcome) with shared channels.
Deadlocks. For linear channels, some situations are avoided by the typing system, but not all. Code using shared channels can easily "deadlock" even though one would not use the word deadlock in this case, for such situations are expected in the shared world.
Here is an example from Section Servers and clients that do not fulfil their obligations), where the second thread would be deadlocked waiting for a reader to which send the true message. The code does not compile.
new x y : !integer.?boolean.end
x!1 | y?z.y!true
There are nevertheless some deadlocked situations that are beyond the reach of the compiler. The simplest one is when both the writer and the reader on a linear channel are on the same thread.
new w1 r1 : !integer.end
w1!5. r1?x. printStringLn!"Got " ++ x
The program terminates prematurely; in particular the message is never
written on the console. Now consider a situation with two channels and
"enough" code to consume the two channels, that is, one write on the
w1 end and one read on the r1 end, and similarly for w2-r2:
new w1 r1 : !integer.end
new w2 r2 : !integer.end
All we have to do is to create an explosive mix of these four operations. In the example below, even though writers are on one thread and readers on the other, the order of reads and writes do not match.
new w1 r1 : !integer.end
new w2 r2 : !integer.end
w1!5. w2!7 |
r2?x. r1?y. printStringLn!"Got " ++ x+y
Once again the program terminates prematurely, printing no message.
This section puts in practice the concepts introduced before while developing some simple programs.
How does one print two strings in a given order? The simplest way is
just to print one, and then print the other. The "then" is rendered
in SePi in the form of the sequencing "." operator. So we could try
the following code.
printString!"Hello". printString!" world!"
The code is guaranteed to print first Hello, and then
world!. But will we ever read Hello world on the console? Let
us put another process running in parallel.
printString!"Hello". printString!" world!" |
printString!"Hi". printString!" there!"
What are the possible outcomes? If we get lucky we will see Hello
world!Hi there!. But there are other possible outcomes, for example,
Hello Hi world!there!. In fact any sequence that contains the
strings Hello, world!, Hi, and there! is possible in so far
as the Hello occurs before the world!, and the Hi before the
there!.
Exercise. Enumerate all possible outcomes.
This is a typical example of interference. How can we avoid such a
situation? In this simple case, we can send strings Hello word! and
Hi there! in single messages, as in:
printString!"Hello world!" |
printString!"Hi there!"
But this may not be always possible. It may be the case that we want to print an undetermined number of values, without interference.
The support in SePi for output is very basic; there is little more that we can do by using the primitive print messages. But we can do some programming. The idea is to hide the primitive print messages behind a server, a print server. Clients use the print server, rather than the primitive print channels.
The print server enforces a protocol that allows clients to print sequences of values of variable length, of any of the three basic types. That is in order to print two or more values clients get hold of a channel that conforms to the following protocol.
type PrintSession = +{printBoolean: !boolean. PrintSession,
printInteger: !integer. PrintSession,
printString: !string. PrintSession,
quit: end}
Suppose that the printer server responds on channel end print. This
is a shared channel, known by all processes that may be interested in
printing without interference. From the print shared (unrestricted,
un) channel, clients obtain a private (linear, lin) channel on
which they conduct a printing session that cannot be interfered with,
as per the session initiation protocol that we have in Section
Session initiation. The code for clients is
easy:
print?p.
p select printString. p!"Hello".
p select printString. p!" world!".
p select quit
And we can have another process running in parallel:
print?p.
p select printString. p!"Hi".
p select printString. p!" there!".
p select quit
And we can rest assured that, if we place the two processes n
parallel, the console will read either Hello word!Hi there or Hi
there!Hello world!, but never Hello Hi world!there!.
The client code is simple, which is good, for there will be many clients, developed separately. The complexity lies in the server. But this is written once only. So, the server must
Serve an unbound number of clients, for which we need a loop (written with a process definition),
For each client it must establish a new session, for which we use the session initiation protocol,
In each session the server needs to serve an undetermined number of print requests, for which we need a second (nested) loop.
Here is the code of a server that serves session initiation requests
on the server shared channel.
// The outer loop that serves multiple clients, one at a time
def serverLoop server: *!PrintSession =
// The inner loop that conducts a print session
def sessionLoop p: dualof PrintSession =
case p of
printBoolean -> p?x. printBoolean!x. sessionLoop!p
printInteger -> p?x. printInteger!x. sessionLoop!p
printString -> p?x. printString!x. sessionLoop!p
quit -> serverLoop!server // recur once done
// Session initiation: the write channel end is sent to clients
// and the read end is kept by the server
server!(new read: dualof PrintSession).
// The reader channel end is used in the inner loop to conduct
// a session with a client
sessionLoop!read
We still have to a) create the shared print channel, and b) launch the server:
// The shared print channel: clients use the print end;
// the server uses the server end
new server print: *!PrintSession
// Launch the server
serverLoop!server
Notice that we are again in the presence of a session initiation, only that the channel that is exchanged is shared. We decided however not to use the special syntax for session initiation, for it would require use to write the "rest of the program" within a brace-delimited block (if the program is a parallel composition of two or more processes). See the differences. Without session initiation:
new server print: *!PrintSession
serverLoop!server
|
// rest of the program
With session initiation:
serverLoop!(new print: *? PrintSession).{
// rest of the program
}
Here is the whole code, so that you may run it:
type PrintSession = +{printBoolean: !boolean. PrintSession,
printInteger: !integer. PrintSession,
printString: !string. PrintSession,
quit: end}
def serverLoop server: *!PrintSession =
def sessionLoop p: dualof PrintSession =
case p of
printBoolean -> p?x. printBoolean!x. sessionLoop!p
printInteger -> p?x. printInteger!x. sessionLoop!p
printString -> p?x. printString!x. sessionLoop!p
quit -> serverLoop!server // recur once done
server!(new read: dualof PrintSession).
sessionLoop!read
new server print: *!PrintSession
serverLoop!server
|
print?p.
p select printString. p!"Hello".
p select printString. p!" world!".
p select quit
|
print?p.
p select printString. p!"Hi".
p select printString. p!" there!".
p select quit
Now that we have a print server running, are we guaranteed that clients that rely on the print server service will never see their output interfered? No! unfortunately. Two things can go wrong:
There may be code that uses the primitive print channels (there is no way we can hide these channels in SePi), and
The server side of the print server is public; code can launch further copies of the server:
serverLoop!server | // Launch a server
serverLoop!server // Launch another server
In conclusion, for interference to be under control, we need a) no code other than the server should use the primitive print channels, and b) there must be a single copy of the server running.
What is the protocol of a function? It receives it(s) arguments and
sends back the result. Let us concentrate on integer-to-integer
functions. The protocol can be written as follows:
type IntToInt = ?integer.!integer.end
Writing functions is easy. Here's two common functions:
def double x: IntToInt =
x?n. x!2*n
def square x: IntToInt =
x?n. x!n*n
Now these functions are persistent: they can be called as many times
as needed. In fact, these functions answer on shared channels: both
double and square are of type *!IntToInt. This means that a
little session initiation protocol is needed to interact with
them. This time we conduct the session initiation process at the
client side. Clients create a shared channel of type IntToInt; send
one end to the function and keep the other for interaction, as for
example in:
double!new c: dualof IntToInt.
c!55.c?x.
printStringLn!"double of 55 is " ++ x |
double!new d: dualof IntToInt.
d!77.d?y.
printStringLn!"double of 77 is " ++ y
How do we write a recursive function? We need no more machinery than the one we have now. We know how to act as a function server and as a function client; we know all it takes. A recursive function will have a part that behaves like a server and a part that behaves like a client (for each recursive call).
Suppose we want to write the factorial function. The code starts as a
function server to compute the factorial of n, then goes into
"client mode" to compute the factorial of n-1, and finally returns
to "server mode" in order to send the result back to the client. And
because the functions we write are persistent (and hence can be used
multiple times), we do not even have to special care when it comes to
make sure there are copies of the function waiting to answer the
recursive calls. Here's the complete code with an example, so that you
may try it:
type IntToInt = ?integer.!integer.end
def factorial x: IntToInt =
x?n.
if n == 0
then x!1
else
factorial!(new y: dualof IntToInt).
y!n-1. y?f.
x!f*n
factorial!new c: dualof IntToInt.
c!15.c?x.
printStringLn!"factorial of 15 is " ++ x
Let us now try a higher order function, for example the function composition operator: (f . g) x = f (g x).
We start by giving a name to the type of shared integer-to-integer
functions:
type IntToIntFun = *!IntToInt
So now we know the type of the composition function: it receives two
IntToIntFun, and returns one such function, that is:
type Composition = ?IntToIntFun.?IntToIntFun.!IntToIntFun.end
def compose c: Composition =
...
According to its type, the code for the compose function must be of
the form:
def compose c: Composition =
c?f. c?g.
// Definition of h
c!h
where h is a function that
reads an integer value, say n,
calls g on n and collects the result, say m
calls f on m, and collects the result, say p, and finally
sends p back to the client.
That is h must be of this form:
def h x: IntToInt = {
x?n.
g!(new d: dualof IntToInt). d!n. d?m.
f!(new e: dualof IntToInt). e!m. e?p.
x!p
}
As for clients, they will use session initiation to start interaction
with compose (as before for double and square), then send two
functions and then get one back. Finally they may (but need not)
interact with the new function. Here's an example:
// Call compose on double and square
compose!(new c: dualof Composition).
c!double. c!square. c?h.
// Exercise the thus obtained function
h!(new c: dualof IntToInt).
c!55. c?x.
printStringLn!"double of square of 55 is " ++ x
Putting everything together so that you may try it, yields the code below.
type IntToInt = ?integer.!integer.end
def double x: IntToInt =
x?n. x!2*n
def square x: IntToInt =
x?n. x!n*n
type IntToIntFun = *!IntToInt
type Composition = ?IntToIntFun.?IntToIntFun.!IntToIntFun.end
def compose c: Composition =
c?f. c?g.
def h x: IntToInt = {
x?n.
g!(new d: dualof IntToInt). d!n. d?m.
f!(new e: dualof IntToInt). e!m. e?p.
x!p
}
c!h
// Call compose on double and square
compose!(new c: dualof Composition).
c!double. c!square. c?h.
// Exercise the thus obtained function
h!(new c: dualof IntToInt).
c!55. c?x.
printStringLn!"double of square of 55 is " ++ x
So far we have been computing on integers, booleans and strings, for these are the primitives types SePi is provided with. What about lists, maps, trees, arrays? There is no structured type built into SePi. Fortunately the language, the pi calculus for that matter, is flexible enough to encode all these data structures. Let us concentrate on lists.
Since lists are not builtin, and SePi does not possess any structured type as primitive, lists must be represented as processes. We use an inductive definition of lists (of integer values), something like List = nil | cons integer List.
Now suppose you are a client to a list, that, is you possess a channel
end and know that at the other hand lies a process behaving as a list.
The first thing you may want to know is what kind of list lies on the
other side, a nil or a cons? In case it is a nil there is
nothing else you may want to know for all empty lists are alike. In
the case of a cons, then you may want to know the integer that
lies at the head of the list, as well as the tail of the list. So, the
protocol of a list, as seen from the side of the client, is as
follows:
type ListSession = &{Nil: end, Cons: ?integer.?List.end}
Lists should answer on shared channels, for they may have many
clients. As such a little session initiation protocol is in order. We
let the list itself initiate the protocol, so that clients only have
to read a ListSession channel on the shared channel. The type of the
list as seen from the side of the client is then:
type List = *?ListSession
Now suppose that list3 is a list. Here is a client that checks
whether the list is empty:
list3?l.
case l of
Nil -> printString!"Its an empty list"
Cons -> l?h. l?t. printStringLn!"Its a list that starts with "++h
So how do lists look like so that they may conform to the protocol
above? We design two processes, one to describe nil lists, the other
to describe cons lists. They both obey the same protocol, that is
List, and they both perform session initiation. Nil says "I am Nil":
def nil l: dualof List =
l!(new s : dualof ListSession).
nil!l. s select Nil
Cons says "I am Cons, and here's my head and my tail":
def cons (l: dualof List, h: integer, t: List) =
l!(new s : dualof ListSession).
cons!(l, h, t). s select Cons. s!h. s!t
Notice both processes perform a "recursive" call after accepting a
connection from a client. The nil process recurs with nil!l and
the cons process with cons!(l, h, t). These calls are necessary in
order to reestablish the processes, so that they may answer to further
clients. But these calls need not be in sequence. In fact, more
parallelism can be obtained if we write cons as follows (and
similarly for nil):
def cons (l: dualof List, h: integer, t: List) =
l!(new s : dualof ListSession).
{cons!(l, h, t) | s select Cons. s!h. s!t}
Now we can build a few lists to play with:
nil!(new list0: List).
cons!(new list1: List, 56, list0).
cons!(new list2: List, 287, list1).
cons!(new list3: List, 23, list2).
...
Here's the whole code so that you may try it.
type List = *?ListSession
type ListSession = &{Nil: end, Cons: ?integer.?List.end}
// The list constructors
def nil l: dualof List =
l!(new s : dualof ListSession).
s select Nil. nil!l
def cons (l: dualof List, h: integer, t: List) =
l!(new s : dualof ListSession).
s select Cons. s!h. s!t. cons!(l, h, t)
// A few lists
nil!(new list0: List).
cons!(new list1: List, 56, list0).
cons!(new list2: List, 287, list1).
cons!(new list3: List, 23, list2).
// A simple client
list3?l.
case l of
Nil -> printString!"Its an empty list"
Cons -> l?h. l?t.
printStringLn!"Its a list that starts with "++h
We now try to convert the code above that checks whether a list is
empty into a function that can be reused. Let us call it null.
The type of a session that converts a list into a boolean value is, when seen from the side of the client, as follows:
type ListToBoolean = !List.?boolean.end
Suppose that the null predicate answers on the null channel end. The
code of a client is simple: get a ListToBoolean channel from the
server, send the list on this channel, wait for the answer (a boolean
value).
null?c. c!list3. c?b. printStringLn!"Is null? " ++ b
The server side a bit more complicated. We need a process that
Performs session initiation,
Reads a channel representing a list,
Runs the List protocol on this channel, and
Returns a boolean value according to the outcome of running the protocol on the list.
At this point we could follow the strategy we used when implementing functions in section A little functional programming. We instead try a more "client-server" approach, by setting up a null server that repeatedly answer clients' requests.
We have seen that clients use the null end of the channel. If we
decide to call the other end nullServer, we need the following
declaration:
new nullServer null: *!ListToBoolean
Here is a first attempt to write our server, following the strategy outlined above:
def nullLoop() =
nullServer!(new c: dualof ListToBoolean).
nullLoop!(). // restore the server
c?list. list?s.
case s of
Nil -> c!true
Cons -> c!false
nullLoop!() // start the server
There is a little glitch in the above code. Can you spot it? Since c
is a linear channel, it must be "consumed" to the end. Then, in the
case of a Cons, we must also read the head and the tail of the list,
even if we do not need them. Here is the revised version, using
wild cards for these two values:
def nullLoop() =
nullServer!(new c: dualof ListToBoolean).
nullLoop!(). // restore the server
c?list. list?s.
case s of
Nil -> c!true
Cons -> c!false. s?_. s?_
nullLoop!() // start the server
Here is the whole code, so that you may try it:
type List = *?ListSession
type ListSession = &{Nil: end, Cons: ?integer.?List.end}
// The list constructors
def nil l: dualof List =
l!(new s : dualof ListSession).
s select Nil. nil!l
def cons (l: dualof List, h: integer, t: List) =
l!(new s : dualof ListSession).
s select Cons. s!h. s!t. cons!(l, h, t)
// A few lists
nil!(new list0: List).
cons!(new list1: List, 56, list0).
cons!(new list2: List, 287, list1).
cons!(new list3: List, 23, list2).
cons!(new list4: List, 1, list3).
// The null server
type ListToBoolean = !List.?boolean.end
new nullServer null: *!ListToBoolean
def nullLoop() =
nullServer!(new c: dualof ListToBoolean).
nullLoop!().
c?list. list?s.
case s of
Nil -> c!true
Cons -> c!false. s?_. s?_
nullLoop!() | // start the server
// Two clients
null?c. c!list3. c?b. printStringLn!"Is null? " ++ b |
null?c. c!list0. c?b. printStringLn!"Is null? " ++ b
Having setup a very basic list operator in the form of a server, we can try more ambitious operators. The overall scheme, however, remains the same. This time, let us know try writing a "function" that gets a list and returns its textual representation. The type of the session that converts a list into a string is, as seen from the side of the client, is as follows:
type ListToString = !List.?string.end
Suppose that the function answers on the toStringServer/toString
channel. The client code is simple:
toString?c. c!list3. c?aString.
printStringLn!"Textual representation: " ++ aString
Given the list3 defined above one should get a string of the form
Textual representation: 23::287::56::[]. The server is not much more
complicated than that of the null predicate. The difference is that
now, when time comes to run the list protocol, the process will have
to make a "recursive" call to obtain the string representing the tail
of the list. Here is the code:
def toStringLoop() =
toStringServer!(new c: dualof ListToString).
toStringLoop!(). // restore the server
c?list. list?s.
case s of
Nil -> c!"[]"
Cons -> s?head. s?tail.
toString?d.
d!tail. d?tailString.
c!head ++ "::" ++ tailString
toStringLoop!() // start the server
Here is the whole code so that you may try it.
type List = *?ListSession
type ListSession = &{Nil: end, Cons: ?integer.?List.end}
// The lists constructors
def nil l: dualof List =
l!(new s : dualof ListSession).
s select Nil. nil!l
def cons (l: dualof List, h: integer, t: List) =
l!(new s : dualof ListSession).
s select Cons. s!h. s!t. cons!(l, h, t)
// A few lists
nil!(new list0: List).
cons!(new list1: List, 56, list0).
cons!(new list2: List, 287, list1).
cons!(new list3: List, 23, list2).
cons!(new list4: List, 1, list3).
// The toString server
type ListToString = !List.?string.end
new toStringServer toString: *!ListToString
def toStringLoop() =
toStringServer!(new c: dualof ListToString).
toStringLoop!().
c?list. list?s.
case s of
Nil -> c!"[]"
Cons -> s?head. s?tail.
toString?d.
d!tail. d?tailString.
c!head ++ "::" ++ tailString
toStringLoops!() | // start the server
// A client
toString?c. c!list3. c?aString.
printStringLn!"Textual representation: " ++ aString
SePi provides a refinement types, and assume/assert primitives to
restrain the usage of resources.
Imagine a bank that accepts credit card transactions. A transaction is
a channel on which the bank reads a credit card number (a string)
and the amount (an integer) to be charged. Whenever the bank
receives a transaction channel, it reads the credit card number and
the amount from the channel, and charges the card for the given
amount.
type CreditCard = string
type Transaction = !CreditCard.!integer.end
def bank (t: dualof Transaction) =
t?card. t?amount.
printStringLn!"Charging card "++amount++" on card "++card
Now imagine you are shopping online, and the time comes for you to provide the store with your credit card number. The store, in turn, forwards the credit card and the purchase amount to the bank.
def store (t: dualof Transaction) =
bank!(t)
Here is the composition of a client, a store and a bank. Try it!
type CreditCard = string
type Transaction = !CreditCard.!integer.end
def bank (t: dualof Transaction) =
t?card. t?amount.
printStringLn!"Charging card "++amount++" on card "++card
def store (t: dualof Transaction) =
bank!(t)
new c s : Transaction
store!s |
c!"1234".c!100
There are are honest stores and not so honest stores. How can you make sure that stores do not charge handling fees that were not part of the deal? A not so honest store may read the transaction data, and create a new "fake" transaction with a different amount, as in:
def store (t: dualof Transaction) =
t?card.t?amount.
new s b : Transaction
bank!b | s!card. s!amount+10
}
Or perhaps the store just duplicates the transaction, effectively charging the card twice, but for the correct amount.
def store (t: dualof Transaction) = {
t?c.t?a.
new s b : Transaction
bank!b | s!c.s!a |
new s b : Transaction
bank!b | s!c.s!a
}
assume and assert primitivesThe usage of resources can be controlled via the assume and assert
primitives. In this case the client asserts that his card is to be
charged exactly once for a given amount. The card number and the
amount may then be sent to the store.
assume charge("1234", 100) |
new c s : Transaction
store!s |
c!"1234". c!100
The bank in turn, makes sure that permission was given to charge the
card by issuing a complementary operation - assert - as in:
def bank (t: dualof Transaction) =
t?card. t?amount.
assert charge(card, amount).
printStringLn!"Charging card "++amount++" on card "++card
Here is the situation so far: the client assumes his credit card is to
be charged exactly once for a fixed amount, prepares a transaction
and sends it to the store. The store, in turn, forwards the
transaction to the bank. Finally, the bank reads the transaction data
and asserts that permission was given to charge the card. The problem
is that the client and the bank are completely unrelated; without
further information, we have no means of making sure that asserts
match assumes, and vice-versa.
The permission from the client to the store and then to the bank is
conveyed via types. We add to the "plain" transaction a charge
predicate: we are only interested in transaction for which the
charge(card,amount) has been issued. This we write as
type Transaction = !c:CreditCard. !{a: integer | charge(c,a)} .end
There are two novelties in this sort of types. One is that values
transmitted on channels may be named at the type level. This is the
case with variable c in the part c:CreditCard. The second is that
types may be refined with predicates, as in {a: integer |
charge(c,a)}. This type is read as an integer a for which the
permission charge(c,a) has been issued.
Stores cannot easily cheat. The following code is not well formed. The
type checker will complain at the point where amount+10 is written in
the transaction. Expect a type error of the form "Expecting {x:
integer | charge(card,x)}; found integer", for there is no information
in the context on predicate charge(card, amount+10).
type CreditCard = string
type Transaction = !c:CreditCard. !{a: integer | charge(c,a)} .end
def bank (t: dualof Transaction) =
t?card. t?amount. assert charge(card, amount).
printStringLn!"Charging card "++amount++" on card "++card
def store (t: dualof Transaction) = {
t?card.t?amount.
new s b : Transaction
bank!b | s!card.s!amount+10
}
assume charge("1234", 100) |
new c s : Transaction
store!s |
c!"1234". c!100
For the same reason, stores cannot duplicate the transaction. assume
and assert are both treated linearly. For each assume there must
be one exact assume, and vice-versa. This means that the bank cannot
charge your card, unless you give permission. But it also means that
the bank will never forget to charge your card (once permission has
been given).
If for some reason you want a card to be charged twice, then you must
grant a double permission. This can be accomplished by two separate
assume operations or by a composed one, of the form below.
assume charge("1234", 100) * charge("1234", 100)
The same applies to assert. One can write two asserts or one only,
using the * combination operator. The number of different asserts
need not match the number assumes: assume charge("1234", 100) *
charge("1234", 100) may be matched against assume charge(c,a) |
charge(c,a)
There is a limit to what one can do with refinement types, assume
and assert. The only way stores are guaranteed not to cheat is by
forbidding them to assume and assert the charge
predicate. Otherwise there is an easy way for the store to circumvent
the policy: just assert on behalf of the bank and assume
(differently) on behalf of the client. Here is a store that cheats by
appropriately asserting and assuming.
type CreditCard = string
type Transaction = !c:CreditCard. !{a: integer | charge(c,a)} .end
def bank (t: dualof Transaction) =
t?card. t?amount. assert charge(card, amount).
printStringLn!"Charging card "++amount++" on card "++card
def store (t: dualof Transaction) =
t?card. t?amount. assert charge(card,amount). {
new s b : Transaction
bank!b |
assume charge(card,1000) |
s!card. s!amount}
new c s: Transaction
store!s |
assume charge("1234", 100) |
c!"1234". c!100
The syntax of types is not complicated. The following are types.
end, boolean, string, and integer - primitive.end describes a channel on which no interaction is possible.
Furthermore, if T1, T2, ..., Tn are types, l1, l2, ..., ln
are labels, p is a proposition, and a is a type variable, then the
following are also types:
!T1.T2 and ?T1.T2 - input/output;
+{l1: T1, ..., ln: Tn} and &{l1: T1, ..., ln: Tn} - choice;
{x: T1|p} - refinement;
a and rec a.T1 - recursion;
dualof T1 - dualof.
In addition, input/output and choice types may be qualified: lin
describes a channel end that can be used exactly once; un qualifies
a channel end that can be used zero or more times. Qualifier lin is
optional, that is why we do not see it often: rather than using
lin!boolean.end one usually writes !boolean.end.
Unbounded interaction requires unbounded types. For example, the type
of an infinite stream of integer values can be written as rec
a.lin!integer.a, as seen from the point of view of the writer
process.
SePi poses one restriction on un types. For a type un!boolean.T to
be well-formed, it must be that case that T is equal to the type
itself, that is to, un!boolean.T. Such a type can be written with the
rec operator. In this case, T can be, for example, rec
a.un!boolean.a, in which case type un!boolean.T is equal to rec
a.un!boolean.a. Types of the form rec a.un!U.a are so common that
we abbreviate them to *!U, and similarly for unbounded input, *?V,
external choice. *+{...}, and internal choice *&{...}.
So now we know why we do not see qualifiers lin and un often: the
former is optional, the latter disappears under abbreviations *!U
*?V, *+{...}, and *&{...}.
Types *+{...}, and *&{...} are handy to encode enumerable
data. For example
type Boolean = *&{False, True}
could denote the type of (persistent) boolean values, of which we need
exactly one of each kind. Persistent processes are usually written in
def format.
def trueServer(v: dualof Boolean) =
v select True. trueServer!v
def falseServer(v: dualof Boolean) =
v select False. trueServer!v
We now create the truth value channels:
new tServer tt: dualof Boolean
new fServer ff: dualof Boolean
And start the servers. Servers use the tServer and fServer ends;
clients use the tt and ff ends.
trueServer!tServer |
falseServer!fServer
For example, rather than using if b then P else Q one can write:
case b of
True -> printStringLn!"Is true"
False -> printStringLn!"Is false"
Putting everything together, so that you may try it.
type Boolean = *&{False, True}
def trueServer(v: dualof Boolean) =
v select True. trueServer!v
def falseServer(v: dualof Boolean) =
v select False. trueServer!v
new tServer tt: dualof Boolean
new fServer ff: dualof Boolean
trueServer!tServer |
falseServer!fServer |
case tt of
True -> printStringLn!"Is true"
False -> printStringLn!"Is false"
(to be completed)