[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
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