[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Priority modeling with CSP?

Jim Davies wrote:

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).

I absolutely agree with everything above from Jim, just in case anyone might think otherwise....

  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.

Again, I agree. Especially about discrete models of time.
Yet modelling a more abstract sort of priority is painful done as above.

Adding priority into CSP without doing violence to the existing language, in particular retaining the abstraction and the algebraic laws seems to help in several ways.

1) It is general: you don't need to invent the extra events and build a special model for every instance.

2) It provides algebraic laws. The motivation here is rather different from the usual applications of CSP in vogue today: provably correct rewriting laws built into compilers and other tools.

3) Not forgetting that this is an occam group, it helps us understand and clarify the meaning of priority in that language. Priority was explicitly excluded from the pair of papers from Michael, Bill and Bryan.

4) It provides an extended language in which to *think* about concurrency in general. For me at least, that is by far greatest value of CSP. Just as other parts of mathematics allow us to grasp and formulate more subtle and precise questions and understanding.

5) Refinement. One of my motivations for extending CSP was that I wanted to be able to add detail, right down to the level of code. I didn't want to have to change paradigm (yuck, that word again) at some arbitrary point between the high level specification and the final circuit or code generated.

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.

Absolutely. But it is not general, and it is complicated. If you want to model check something with priority with the tools available today, and FDR is *wonderful*, then this is what you have to do. I hope you have plenty of time :-). Actually, this is akin to testing rather than proving: you have to prove each individual case. Sorry, that was a bit below the belt. :-)

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.

If you want to model communications with a satellite at the level of nanoseconds, you can't ignore relativity. Of course, I am not (yet) suggesting that this is something that is likely to be done at that level of detail in CSP. Yet there is no reason why we cannot extend the ideas in a sympathetic way to encompass such things. And much more.

CSP is *so powerful*, mainly because its abstractions are so simple, and capture just the right intuitions -- the idea of a CSP event and the idea of a space-time event match very closely, and even survive into the quantum world in the many worlds interpretation. It is a great pity to restrict such a useful language to the original applications of interleaved software with synchronisation as communication. As long as we can do that without spoiling the simplicity, compositional properties, and so on.

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

I don't think Gavin is on ths list is he? :-) Maybe Steve is lurking..

Just a last point. If you have ever struggled with a VHDL or verilog description of a parallel circuit,or even a complex schematic and you know CSP, then you scream for a clear transparent description. Just to *understand*. And if it allows you to prove or generate a correct version, then you are in heaven...

Dr A E Lawrence