OEP

110

Title

Extended rendezvous

Summary

Allow code to be executed during an input while the other process is blocked.

Owner

Fred Barnes <F.R.M.Barnes@kent.ac.uk>

Status

Accepted

Date-Accepted

2001-12-19

Keywords

language input channels

The extended rendezvous allows an inputting process to specify a process which will be executed after the communication has been performed, but before the outputting process resumes. The syntax uses the double question-mark "??". For example, a (semantically invisible) data logging process looks like:

PROC logging (CHAN BYTE in?, out!, log!)
  WHILE TRUE
    BYTE b:
    in ?? b
      SEQ   -- during process
         -- the following action is undetectable by processes on either side,
         -- assuming it does not block forever!
         log ! b
         -- forward the data
         out ! b
      ...  after process (optional)
:

Indented under the extended input "??" are two processes. The first (during process) is the one executed before the outputting process continues; the second (after process) is the one executed after the outputting process has resumed. The after process is optional and never needed for a committed simple input, as above (since its actions could simply follow the extended input process). The during process may not re-engage in the extended input channel ("in" in the above example), since this would cause deadlock, and the compiler checks for this.

Inputs from tagged protocol channels may be extended with a similar syntax, but separate during and (optional) after processes are allowed for each variant. For example:

PROTOCOL TAGGED
  CASE
    empty(
    num; INT
:

PROC foo (CHAN TAGGED in?, CHAN BYTE out!)
  WHILE TRUE
    SEQ
      ...
      in ?? CASE
        empty
          out ! '**'              -- during process
        INT n:
        num; n
          out ! BYTE (n /\ #FF)   -- during process
          out ! '**'              -- after process
      ...
:

Extended inputs may also be used in ALT processes. In this case, the extended input together with its during process is the ALT guard and the after process is the response to selecting and executing that guard. However, if no response is needed (because the during process has done it all), the after process may be omitted:

ALT
  BYTE b:
  in.0 ?? b
    ...  during process
    ...  after process (response to extended input)
  BYTE b:
  in.1 ?? b
    ...  during process
  tim ? AFTER timeout
    ...  response to timeout

Note: the optional nature of the after process in both the above examples is inconsistent with the strict rules in other parts of the language. Normally, if the language syntax requires a process where the application logic has nothing to perform, a SKIP process must be written. More thought should be given either to relax the strict rules (so that all SKIP processes may simply be omitted) or to enforce the strict rules everwhere (so that SKIP processes must be inserted in the above examples that have missing after processes).

Semantics: this is given by a formal transformation of the system code employing it. Suppose we have a simple extended input process:

BYTE b:
c ?? b
  ...  during process
  ...  after process

running in parallel with:

c ! 42

Invent a BOOL acknowledge channel, say c.ack. The extended input process becomes:

BYTE b:
SEQ
  c ? b
  ...  during process
  c.ack ! TRUE
  ...  after process

The sending process becomes:

BOOL any:
SEQ
  c ! 42
  c.ack ? any

If the extended input process were an ALT guard or processing a tagged protocol, obvious variations of the transformation apply.

Note: the implementation is much lighter than this - no need for a request channel and additional communication ... and no overhead on non-extended communications.

OEP/110 (last edited 2012-08-09 14:13:35 by phw)