|Title:||A Fast Resolution of Choice between Multiway Synchronisations|
|Conference:||Communicating Process Architectures 2006|
Peter H. Welch
School of Computing, University of Kent
Communicating processes offer a natural and scaleable
architecture for many computational systems: networks-within-networks,
explicit dependencies (through 'visible plumbing', i.e. shared events),
and explicit independencies (through 'air gaps', i.e. no shared
events). CSP is a process algebra enabling the formal specification of
such systems and their refinement to executable implementation. It allows
the description of complex patterns of synchronisation between component
processes and provides semantics sufficiently powerful to
reason about non-determinism, multiway synchronisation, channel communication,
deadlock and divergence.
However, programming languages (such as occam-pi) and libraries (JCSP, CTJ, C++CSP, etc.), offering CSP primitives and operators, have always restricted certain combinations from use. The reasons were solely pragmatic: implementation overheads. The main restriction lies in the set of events that a process may offer - and non-deterministically choose between if more that one becomes available. The constraint is that if one process is choosing between event e and some other events, other processes offering e must do so only in a committed way - i.e. not as part of a choice of their own. The choice can then be resolved with a simple handshake. Hence, only the process on the input side of a channel may offer it within a choice construct (ALT) - an outputting process always commits. Similarly, choice between multiway synchronisations is banned; since symmetry allows no one process the privilege.
This is unfortunate since free-wheeling choices between all kinds of event are routinely specified by CSP designers and they must be transformed into systems that meet the constraints. Because any process making such a choice withdraws all bar one of its offers to synchronise as it makes that choice, resolution is usually managed through a 2-phase commit protocol. This introduces extra channels, processes and serious run-time overheads. Without automated tools, that transformation is error prone. The resulting system is expressed at a lower level that is hard to maintain. Maintenance, therefore, takes place at the higher level and the transformations have continually to be re-applied.
This talk presents a fast resolution of choice between multiway synchronisation (the most general form of CSP event). It does not involve 2-phase commit logic and its cost is linear in the number of choice events offered by the participants. A formal proof of its correctness (that the resolution is a traces-failures-divergences refinement of the specified CSP) has not been completed, but we are feeling confident. Preliminary bindings of this capability have been built into the JCSP library (version 1.0 rc6) and an experimental (read complete re-write) occam-pi compiler. This will remove almost all of the constraints in the direct and efficient realisation of CSP designs as executable code. An example of its use in a (very) simple model of blood clotting (from our TUNA project) will be presented.