Quentin Miller Bernard Sufrin
Oxford University Computing Laboratory
Wolfson Building, Parks Road
OXFORD OX1 3QD
U.K.
{Quentin.Miller,Bernard.Sufrin}@comlab.ox.ac.uk
November 1999
Support for intelligent telecommunication services (such as messaging, personal phone numbers, and number translation) is an increasingly important part of the functionality offered by the vendors of switching equipment. As the complexity of services increases, the expressive power of current design notations for such services -- often based on ad-hoc extensions of standard techniques for describing finite state machines -- is being severely challenged. Although the graphical environments in which services are designed can look very attractive, the rationality of the design process and the reliability and predictability of the resulting services are fundamentally limited by the inadequate expressive power of the underlying notations.
These considerations lead us to conjecture that the design and implementation of intelligent networking services will in future require no less than the power of a modern, general purpose, programming notation. In this note we introduce the main features of Eclectic CSP (eCSP) -- an experimental specification and programming notation designed for work in this field. Its semantic features have been borrowed from many sources: notably OCCAM [5], CSP [2], and Z [3].
As well as basic scalar types such as int, char, and bool, eCSP provides tuples, vectors, and sets. Values of all these types may be anonymous -- for example, the 3-tuple
('a', 5, true)may appear in an expression without a name having been declared for it; its storage space will be allocated and freed automatically.
Complex vector and set expressions may be given concisely by replication, as in
{( for x in 1..4) x*x}whose value is the set {1,4,16,9}, or
#[( for 't' in v) true]whose value is the number of instances of character 't' in character vector v (the vector generated contains one instance of true for each instance of 't' in v, and # yields the length of that vector).
Free data types can be simple enumerations of constants,
data Colour = red + green + blueor collections of constructed values; as in this type IntTree whose nodes are leaves containing integer values, or interior nodes containing a pair of subtrees:
data IntTree = Leaf int + Branch (IntTree, IntTree)An element of type IntTree would have a form such as
Branch (Leaf 0, Branch (Leaf 5, Leaf 6))
Values of these types may be analysed by pattern-matching. For example, this recursive procedure assigns the leftmost integer in binary tree t (type IntTree, above) to the variable i:
proc findLeft (t:IntTree) isThe ( or) construct selects between two alternatives. Iterative pattern-matching is also provided; we could perform the same assignment as findLeft non-recursively by
if v is
Branch (l,r) -> findLeft (l)
or
Leaf x -> i := x
fi
do v isThe do... od construct pattern-matches repeatedly until none of its patterns match the datum being matched.
Branch (l,r) -> v := l
od;
if v is Leaf x -> i := x fi
Patterns which incorporate the catenation operator (+) are useful for working with vectors and sets -- for example, here we generate a set s containing the elements from vector v:
s := {};
do v is [x]+v' ->
s := {x}+s;
v := v'
od
Processes communicate synchronously with one another by writing values to channels, using the notation
channel ! valueand reading values from channels, using
channel ? pattern -> processAll such channel communication is synchronous; the reader and the writer will both wait until the data has been transferred before continuing.
As reading involves pattern-matching, it may use ( or) to select from a number of possible reads -- for example, this process loops indefinitely, merging the inputs from two channels into a single output channel:
do
left?x -> out!x
or
right?x -> out!x
od
Channel reading may also be replicated; here is a process which merges data from a vector of input channels:
do
or( for i in 0..n) input(i)?x -> out!x
od
A channel which carries data of type T has two distinct ends, called ports. The type of an input port is written ?T, and that of an output port is !T -- the type-checker confirms that the ends are being used consistently, with one process writing at one end and one process receiving at the other. Channels and ports may be declared as being shared in which case several processes may have access to either end, but a process must acquire a lock on its end of the channel before using it. If c is a shared channel, a process may read or write with it only in the body of a server or client construct:
server c in c?x -> ... end(In fact the server may also write to a channel and the client may read, but the server/ client distinction is needed to specify that the processes are claiming opposite ends of the channel.)
client c in c!v; ... end
A process may use ( or) to attempt to claim any of a number of shared channels:
do
server c0 in
(perform a service using channel c0)
end
or
server c1 in
(perform a different service using channel c1)
end
od
Processes are executed concurrently by joining them with the ( ||) operator. They can communicate with each other through channels declared in an enclosing scope.
let chan c: int inConcurrency may also be replicated --
begin ...; c!v; ... end
||
begin ...; c?x -> ... end
end
||( for i in v) P(i)means
P(v(0)) || P(v(1)) || ... || P(v(n))where P(i) is a process which may refer to i.
Concurrent processes created by ( ||) must all terminate before the enclosing process is allowed to proceed. Alternatively, the construct
fork pcreates a process which executes p in parallel with the current process; no action is taken on its termination (unless such action is specifically programmed).
Modules provide a way of packaging a data structure with a particular behaviour whilst hiding its implementation. The set of exported types and values is called the module's interface. It can be declared independently of the module declaration, thus allowing more than one module to implement an interface.
Modules and interfaces may be parameterised by types and/or values. Thus, a module implementing the structure and operations of, say, a linked list can be given independently of the type of data stored within such a structure. Instances may then be declared using different types, to create integer lists, boolean lists, etc. These instantiations of the module will be strongly-typed, and their use can be type-checked at compile time (all eCSP type-checking is performed at compile time).
Here is a small example. The TokenService module exports three values: a server procedure which implements a process to provide tokens on request, and two ports through which these tokens may be received from or sent to the server. The token type is a parameter of the module, so it may be instantiated with any type. The server process is parameterised by an initial set of tokens to manage. The ports are shared, thus the server may interact with any number of clients.
module TokenServiceInput and output channels are declared in the module. One end of each is exported, the other end is used by the server.<token>implements
proc serve ({token})
con alloc: shared ?token
con unalloc: shared !token
with
shared chan alloc: tokenThe server repeatedly makes itself available for communication through the shared channels. The guard expression pool!={} ensures that the server does not attempt to communicate on the alloc channel if it has no tokens to allocate. The server is always prepared to accept a returned token on its unalloc channel.
shared chan unalloc: token
proc serve (free:{token}) is
let
var pool = free
in
do
pool!={} & server alloc in
if pool is {t}+pool' ->
pool := pool';
alloc ! t
fi
end
or
server unalloc in
unalloc ? t -> pool := {t}+pool
end
od
end
end
A client process can obtain or relinquish a token by claiming and communicating through the appropriate channel:
...
client alloc in alloc ? t -> token:=t end;
...
client unalloc in unalloc ! token end;
...
To run the client/server network, we declare an instance of the module with the appropriate type, and execute a server (with its initial pool) in parallel with the clients:
instance IntServer is TokenService<int>
IntServer.serve (0..1023) ||
client0 || client1 || client2 || ...
The first experimental implementation of eCSP is now completed. A compiler translates eCSP source into Java [1]. A simple correspondence between eCSP modules and Java classes is maintained -- this has benefits for programming in either language:
A fuller description of Eclectic CSP can be found in
ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Bernard.Sufrin/ecsp.ps
Our intellectual debt to Tony Hoare and David May will be evident: the conceptual clarity offered by CSP, and the semantic coherence offered by the Occam programming language have been an inspiration to us and provided a secure base from which to explore. The essence of the design of shared channels is due to Geoff Barrett.
This work was supported by Marconi Communications Ltd.