OEP

162

Title

TRACES TYPEs extensions

Summary

Provides a mechanism for formal specification (and compiler checking of) process behaviours

Owner

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

Status

Proposed

Date-Proposed

2007-10-01

Keywords

language formal traces

Currently, the compiler checks only that processes behave themselves with respect to parallel usage and aliasing. What it cannot currently check is the behaviour of a particular process. For example, the standard "id" component, with the implementation:

   1 PROC id (CHAN INT in?, out!)
   2   WHILE TRUE
   3     INT v:
   4     SEQ
   5       in ? v
   6       out ! v
   7 :

Has a behaviour that the environment (anything external to the process) sees as alternating communications on 'in' and 'out'. This is the desired behaviour, and may in fact be required if the component is to function correctly within a process network. There is currently no way to specify this behaviour in the occam-pi language, nor a mechanism for checking processes against those behaviours; the subject of this OEP.

It is proposed that the behaviours of a process are defined by a new TRACES TYPE definition:

   1 TRACES TYPE name (params) IS "traces specification":

The parameters (params) are simple names tagged an optional '!' or '?' (indicating output and input behaviours respectively). The traces-specification is a string describing a particular behaviour (or set of behaviours) using a CSP/FDR style syntax, whose names are bound to the given parameters or local variables within the expression. For example:

   1 TRACES TYPE T.INOUT (a?, b!) IS "a? -> b!":

This states that the T.INOUT traces-type has a behaviour of input from 'a' followed by output to 'b'.

The traces specification is made up from the following grammar:

traces-name ::= <occampi-name> [ ? | ! ]                # name (event) with optional input or output specifier
traces-expr ::= Skip                                    # primitive processes
              | Stop
              | Chaos
              | Div
              | <traces-name>                           # event synchronisation
              | <traces-name> -> <traces-expr>          # event synchronisation, then ..
              | <traces-expr> || <traces-expr>          # parallel events
              | <traces-expr> [] <traces-expr>          # external choice over events
              | <traces-expr> |~| <traces-expr>         # internal choice over events
              | <traces-expr> ; <traces-expr>           # sequential events
              | @ <traces-name> , <traces-expr>         # repeating events (fixpoint)
              | <traces-name> [ <traces-expr> ]         # extended input action
              | <occampi-name> ( <traces-name>, ... )   # instance of another named traces type
traces-spec ::= { <traces-expr> , ... }                 # list of possible traces
              | <traces-expr>                           # single trace

To have the compiler check PROCs for a particular behaviour, a TRACES addition is made to the procedure declaration. In the case of id, this would be:

   1 PROC id (CHAN INT in?, out!) TRACES T.INOUT (in?, out!)
   2   ...  body of id
   3 :

The compiler can then check and verify that the implementation of "id" does in fact behave in the way specified by "T.INOUT" (with "a" and "b" in the trace replaced by "in" and "out").

For the given "T.INOUT" trace specification above, the compiler will allow that sequence of events to be repeated indefinitely. If we wish the behaviour to be single-shot, that must be stated explicitly in the trace with Skip (meaning successful termination). For example:

   1 TRACES TYPE T.INOUT.ONESHOT (a?, b!) IS "a? -> b! -> Skip":

The implementation of "id" above would not satify this particular trace specification.

Within the traces language, other named occam-pi trace types may be instanced. For example:

   1 TRACES TYPE T.PREFIX (x?, y!) IS "y! -> T.INOUT (x?, y!)":

which is equivalent to:

   1 TRACES TYPE T.PREFIX (x?, y!) IS "y! -> @X,(x? -> y! -> X)":

i.e. the expanded "T.INOUT" is allowed to repeat indefinitely. However, if the substituted trace terminates with a "Skip", this will be removed in the trace it's being substituted into. For example:

   1 TRACES TYPE T.TWOSHOT (a!) IS "a! -> a! -> Skip":
   2 TRACES TYPE T.EVENSHOT (b!) IS "T.TWOSHOT (b!)":

the expanded case, "T.EVENSHOT", will be allowed to repeat.

Future applications

The implementation of the above mechanisms within the compiler results in the compiler generating actual traces for implementations, which are then checked against their formal specifications. From these, the compiler can potentially check that networks of processes satisfy certain properties (such as deadlock freedom), but probably not for all cases. One example would be a ring of "id" processes, which is effectively deadlock. Through a combination of trace extraction and static analysis, a compiler would be able to reject this code at compile-time.

From the CSP perspective, this is essentially failures analysis -- something which tools like FDR do currently -- so the term traces analysis is slightly misleading. Processes in CSP are characterised by traces, failures and divergences, separately. What the compiler is really dealing with are descriptions of process behaviours, from which we could extract the possible CSP traces if desired.

Other future uses include the checking of phased barrier access to shared resources (see OEP/137).

OEP/162 (last edited 2007-11-21 08:59:10 by frmb)