Re: Priority modeling with CSP?

[Jim Davies <Jim.Davies@xxxxxxxxxxxxxxx>]

The `standard' language of CSP - being the one defined in the original
book, which is essentially the same as the one used in Roscoe's book,
which is again the same as the one used in Schneider's book (the
differences are cosmetic) doesn't attempt an explicit treatment of

 * time
 * priority

Actually, Alan Jeffrey showed some years ago that a treatment of
either would be a treatment of both, effectively (more specifically:
csp + discrete time = csp + priority).  When you abstract from time,
you are abstracting from priority, and vice versa.  But either way, it
doesn't have it.

This is intentional, and a good idea.  Both Tony and Edsger Dijkstra
were of the same mind on this one: from Edsger's most recent talk in
Oxford, I would guess that he is still of exactly the same opinion;
Tony may have changed his position, I couldn't tell you. 

They wanted a language that can be used to convey the essence of a
design, the protocol for usage, the intended pattern of interaction,
the communication outline: something as =abstract= as possible, yet
intuitive and with a convenient, practical theory (you'd like to be
able to =reason=, mathematically, about properties of the design).

They regarded priority and timing information as an implementation
concern.  Of course it might be considered in the early stages of
design, or re-design, but correctness - as expressed and demonstrated
=using the process model= ought to be independent of these issues.

Put another way: you don't use the (CSP) model to describe these
things directly, or explicitly.  You calculate, you count, you figure
out what will happen, but at the level of the code, and there's no
point having a model at the level of the code (unless you have
refactored the information to produce that model, and it's more
amenable to slicing). 

  BUT WAIT!  (WAIT 0.1414).  Didn't I do a doctorate on Timed CSP?
  Wasn't there a whole research effort (that the Australians are still
  running with?).  What about all of the (quite remarkable) work that
  Bill, Mike and Steve did?  

  Well, you can use a simple notation to add timing information to
  your process descriptions.  It's a nice set of hooks for subsequent
  calculation about timing properties.  You might think of the timing
  bits as a well-defined language of annotations; the effort goes into
  making sure that these are used consistently, and interpreted
  properly.  It's a remarkable piece of work.

  But you don't need Timed CSP for every model in which time and/or
  priority is important to you.

You can address timing and priority in models constructed using
ordinary CSP by using additional, auxiliary events: events which are
observable in the model yet do not correspond to observable
interactions, or sequences of interactions, in the system.  

These events can represent the end of a time interval, or internal
events that have a bearing upon priority (message A arrived before
message B).  They can be linked by an auxiliary process, which
enforces certain properties (e.g., time intervals end in order - or in
some order, if you are modelling multiple time frames) or assumption.

The relationship between these events and the behaviour of the
implementation may be subtle: the energy goes into the abstraction;
but the model is accessible, and amenable to mechanical (and manual)
analysis.

Sometimes an explicit treatment is exactly what you want, and then you
want timed CSP, or a prioritised CSP, but - in my experience - most of
the people who have said `ah, we need real-time CSP' or even `I need a
relativisitic model, a real-space, real-time algebra' could get all of
the reasoning that they are ever going to do, and more, done using
ordinary CSP, and a bit of lateral, as opposed to literal, thinking. 

best regards

Jim 

p.s., before someone offers me an example in which real-time,
probabilistic csp is absolutely the only thing that will do, let me
say two things (i) I did say `most of the people', and that might not
include you (ii) I probably don't have time to prove you wrong if
you are x