========================================
              A Semantics for occam-pi Mobile Channels
              ========================================

              P.H.Welch, TUNA Project Meeting, 7-8 July, 2005.


We apply the same trick to model mobile channels that we used for mobile
barriers.  Namely, model the occam-pi channel as a CSP process, *not* as
a CSP channel!


======================================
Modelling a CSP Channel with a Process
======================================

The model follows the simple handshake mechanism used by the occam-pi channel
implementation.  Suppose:

  (P |{c} union X| Q) \ {c}                                               [1]

is a system containing a hidden channel 'c' and operating under occam-pi useage
rules for channels:

  o the process 'P' only ever writes on 'c';
  o the process 'Q' only ever reads on 'c';
  o the process 'P' always commits when it writes on 'c' - i.e. channel output
    (e.g. 'c!p') is never the prefix of a component of external choice, [].

Then, the system is equivalent to one in which the channel is replaced with a
simple buffer-with-handshake process:

  ((P' |X| Q') |{writeC, ackC, readC}| ChanC) \ {writeC, ackC, readC}     [2]

where 'writeC' and 'readC' are channels carrying the same protocol as 'c' and
'ackC' is an event and:

  ChanC = writeC?p -> readC!p -> ackC -> ChanC

and where P' is P but with prefixes:

  c!p -> X

replaced with:

  writeC!p -> ackC -> X

and where Q' is Q but with prefixes:

  c?q -> Y

replaced with:

  readC?q -> Y

Note that the P' sequence of events, "writeC!p -> ackC -> X", cannot happen
without the matching "readC?q -> Y" in Q' ... just as "c!p -> X" in P cannot
happen without "c?q -> Y" in Q.

The proof of equivalence between [1] and [2] is left as an exercise!  :)

Note that termination of the ChanC process, when P' and Q' terminate, is needed
but not addressed in the above.  This is easy though -- see later.

Note that the model gives us distinct channel-ends: the 'writeC/ackC' pair
and 'readC'.

Note that using the 'writeC/ackC' pair as a prefix of an external choice does
not yield the semantics of using 'c!p' in the same context.  Hence, the ban on
output guards in occam-pi.

The following extends this idea to capture all the dynamic semantics of
occam-pi mobile channels: channel types (bundles), channel-end variables,
shared channel-end variables, run-time construction, communication, assignment,
and their passing as arguments to forked processes.


===============================
occam-pi Mobile Channel-Bundles
===============================

An occam-pi mobile channel type declares a bundle of individual channels - e.g.

  CHAN TYPE X
    MOBILE RECORD
      CHAN P0 p0? :     -- message protocol P0, field channel p0, server input
      CHAN P1 p1! :     -- message protocol P1, field channel p1, server output
      CHAN P2 p2? :     -- message protocol P2, field channel p2, server input
  :

Bundle-end variables may be declared shared or (the default) unshared:

  X? a, b, c:           -- three X server-end variables
  X! d, e, f:           -- three X client-end variables
  SHARED X? g, h:       -- two X shared server-end variables
  SHARED X! i, j:       -- two X shared client-end variables

Bundle-end variables are initially undefined.  Actual mobile channel bundles
are constructed dynamically and must be assigned to a matching pair of bundle
end-variables (either, none or both of which may be shared):

  a, j := MOBILE X      -- creates an X bundle, shared at the client ends

One end, at least, is usually routed to another (concurrent) process:

  m ! j                 -- where m has type CHAN SHARED X!

Note: the 'j' variable, because it is shared, remains defined.  Only a clone
was sent.

The unshared 'a' variable may now be used for communication:

  a[p0] ? p             -- wait for and receive message 'p' from the 'p0' field

At the other end, the shared 'j' variable may be used for communication, but
first it must be claimed:

  CLAIM j               -- blocks if another process is using the bundle
    SEQ                 -- this process now has exclusive use of this bundle-end
      j[p0] ! 42        -- send '42' down the 'p0' field channel
      ...               -- may use other channel fields within the 'j' bundle

Note: if an unshared bundle-end variable is communicated (or assigned) away:

  n ! a                 -- where n has type CHAN X?

the 'a' variable becomes undefined.


=================================================================
Modelling occam-pi Mobile Channel-Bundles with (Kernel) Processes
=================================================================


Our model is built around the above process model of a simple channel, but with
proper attention to termination, sharing and mobility.

A channel bundle is a parallel collection of processes: one holding a reference
count, two semaphores (one for each possibly shared end) and one channel process
for each field in the bundle:

  Bundle (c, f) =
    ( |{kill}| {Refs (c, 2), Sem (c, server), Sem (c, client), Channels (c, f)}
    ) \ {kill}

where 'c' is an index, unique for each mobile channel bundle, and 'f' is the
number of channels in the bundle (which is 3 for the X example above).  Also:

  server = 0
  client = 1
 
occam-pi mobile-channel-bundle-end variables become mobile integer variables,
holding indices to the actual bundles.  The latter are (kernel) processes,
running in parallel to all application processes and created dynamically as
needed.  This means that they are accessible to all application processes,
even though their construction is triggered by individual ones.  So, we don't
require the awkward "scope extrusion" concept of the pi-calculus, :).

Note: in this exposition, we are modelling the channels independent of the data
types and structures of the messages they carry.  This can be modelled with
only some modest added detail.

The reference count for a newly constructed bundle is 2 ... one for each end.
If an end is a shared type, initially only one process has the reference.  Here
is the controlling process:

  Refs (c, n) =
    enroll.c -> Refs (c, n + 1) []
    resign.c -> Refs (c, n - 1)                                 ,  n > 0

  Refs (c, 0) = kill -> SKIP

The semaphore is given by:

  Sem (c, x) =
    claim.c.x -> release.c.x -> Sem (c, x) []
    kill -> SKIP

where x:{server, client}.

The channels are installed with:

  Channels (c, f) = |{kill}| {Chan (c, i) | i:{0 .. f - 1}}

and their behaviour is given by:

  Chan (c, i) =
    write.c.i?p -> read.c.i!p -> ack.c.i -> Chan (c, i) []
    kill -> SKIP

Mobile channel bundles are generated by the following server:

  MC (c) =
    setMCfields?f -> getMC!c -> (Bundle (c, f) ||| MC (c + 1)) []
    noMoreBundles -> SKIP

Application processes send the number of fields for the mobile channel bundle
they want constructed and receive its index number.

Application processes, for simplicity in this model, sometimes try to resign
from undefined bundle-end variables.  For convenience, mobile channel bundles
have indices greater than zero and we define:

  UndefinedBundle =
    resign.undefined -> UndefinedBundle []
    noMoreBundles -> SKIP

where:

  undefined = 0

The complete mobile channel kernel is:

  MobileChannelKernel = MC (1) |{noMoreBundles}| UndefinedBundle


================
The Whole System
================

If System is an occam-pi application and System' is the CSP modelling of its
mobile channel primitives (see below), the full model is:

  ( (System'; noMoreBundles -> SKIP) |MobileChanKernelChans| MobileChannelKernel
  ) \ MobileChanKernelChans

  MobileChanKernelChans =
    { 
      noMoreBundles,     -- terminate MobileChannelKernel
      setMCfields.f,     -- construct a bundle with 'f' channels
      getMC.c,           -- return bundle index 'c'
      enroll.c,          -- enroll a process on bundle 'c'
      resign.c,          -- resign a process on bundle 'c'
      claim.c.x,         -- claim shared 'x'-end of bundle 'c'
      release.c.x,       -- release shared 'x'-end of bundle 'c'
      write.c.i.p,       -- write 'p' to channel 'i' of bundle 'c'
      read.c.i.p,        -- read 'p' from channel 'i' of bundle 'c'
      ack.c.i            -- acknowledge reading from channel 'i' of bundle 'c'
      
      | f > 0, c >= 0, i >= 0, x:{server, client}
    }


================================================
Modelling the occam-pi Mobile Channel Primitives
================================================

Note: we're using here the syntax of Circus, allowing us to combine variables
and assignment into CSP.  Pure CSP could be reached by introducing parallel
terminatable state-processes for each variable, whose duration matches their
scope, plus 'load', 'store' and 'kill' channels for writing and reading their
values and for termination.


-------------------------------------
Mobile channel-bundle-end declaration
-------------------------------------

All varieties of declaration:

  X! cli:      SHARED X! cli:      X? svr:      SHARED X? svr:   
  P            P                   P            P

become:

  Var Natural cli .
  cli := undefined;  P';  resign.cli -> SKIP

or:

  Var Natural svr .
  svr := undefined;  P';  resign.svr -> SKIP

respectively, where P' is the CSP model of P.

The sharing makes no difference to the declaration.  Unshared ends will
interact with slightly over-engineered kernel processes -- the relevant
semaphores will be redundant -- but no matter!


----------------------------------
Mobile channel-bundle construction
----------------------------------

  cli, svr := MOBILE X

becomes:

  setMCfields!nf(X) -> getMC?tmp -> ((cli := tmp) ||| (svr := tmp))

where 'nf(x)' is the number of channel fields in 'X' (3 in the example above).


------------------------------------
Claiming a shared channel-bundle-end
------------------------------------

Claiming a client-end:

  CLAIM cli
    P

becomes:

  claim.cli.client -> P';  release.cli.client -> SKIP

Claiming a server-end:

  CLAIM svr
    P

becomes:

  claim.svr.server -> P';  release.svr.server -> SKIP


--------------------------------------------------
Reading and writing to a field of a channel bundle
--------------------------------------------------

It makes no difference whether the bundle end is client or server.  Here,
'X', 'cli' and 'svr' are as declared above.  First, using field 0:

  cli[p0] ! p

becomes:

  write.cli.0!p -> ack.cli.0 -> SKIP

and:

  svr[p0] ? p

becomes:

  read.svr.0?tmp -> (p := tmp)

The channel direction of field 1 in 'X' is the opposite to that for field 0:

  svr[p1] ! p

becomes:

  write.svr.1!p -> ack.svr.1 -> SKIP

and:

  cli[p1] ? p

becomes:

  read.cli.1?tmp -> (p := tmp)

Note: we rely on certain 'healthiness conditions' from the application processes
being transformed here.  For instance, if a bundle-end variable is shared, it
must be claimed before use and released afterwards.  We could enforce this in
the kernel processes, but there is no need.  The necessary 'healthiness conditions'
are enforced by the occam-pi compiler and, so, the kernel -- and these semantics
-- need not bother, ;).


-----------------------------------------
Mobile channel-bundle-end send (unshared)
-----------------------------------------

Sending a client-end:

  m ! cli              -- where CHAN X! m:

becomes:

  m!cli -> (cli := undefined)

Sending a server-end is the same:

  n ! svr              -- where CHAN X? n:

becomes:

  n!svr -> (svr := undefined)

Note: the compiler (or whoever is doing these transformations) knows whether
the bundle variables (and channel) are shared.  So, knowing whether to apply
the above transformation, or the following one, is no problem.


---------------------------------------
Mobile channel-bundle-end send (shared)
---------------------------------------

Sending a client-end:

  m ! cli              -- where CHAN SHARED X! m:

becomes:

  enroll.cli -> m!cli -> SKIP

Sending a server-end is the same:

  n ! svr              -- where CHAN SHARED X? n:

becomes:

  enroll.svr -> n!svr -> SKIP


---------------------------------------------------
Mobile channel-bundle-end receive (shared/unshared)
---------------------------------------------------

Receiving a client-end:

  m ? cli              -- where CHAN X! m: (or CHAN SHARED X! m:)

becomes:

  m?tmp -> resign.cli -> (cli := tmp)

Receiving a server-end is the same:

  n ? svr              -- where CHAN X? n: (or CHAN SHARED X? n:)

becomes:

  n?tmp -> resign.svr -> (svr := tmp)


--------------------------------
Mobile channel-bundle-end assign
--------------------------------

In the following, 'a' and 'b' must be mobile bundle-end variables of the same
channel type and endianism (client or server).

First, if they are unshared ends:

  a := b

becomes:

  resign.a -> (a := b);  b := undefined

Second, if they are shared:

  a := b

becomes:

  (enroll.b -> SKIP ||| resign.a -> SKIP); (a := b)


-----------------------------------------------------------
Forking a process with a mobile channel-bundle-end argument
-----------------------------------------------------------

Let 'c' be an unshared mobile bundle-end variable.  Then:

  FORK P (c)

becomes:

  forkP!c -> c := undefined

where 'forkP' is a channel specific for forking instances of 'P'.  See ForkP
below.

More usually, of course, *shared* variables are passed, so that the forking
process retains the bundle-end (for passing to future forked processes).
Let 'c' be a shared mobile bundle-end variable.  In this case:

  FORK P (c)

becomes:

  enroll.c -> forkP!c -> SKIP

Forking processes run in a FORKING block (by default, the whole system):

  FORKING
    F

which becomes:

  ((F'; done -> SKIP) |{forkP, done}| ForkP) \ {forkP, done}

where F' is the CSP model of F and:

  ForkP =
    (forkP?c -> ((P'(c); resign.c -> done -> SKIP) |{done}| ForkP))
    []
    (done -> SKIP)

where P'(c) is the CSP model of P(c).

Note: the 'done' event above is just to make sure that the forking block, F,
cannot exit until all processes forked in that block have terminated.