Re: Priority modeling with CSP?

[A E Lawrence <adrian.lawrence@xxxxxxxxxxxxx>]

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

Adrian
--
Dr A E Lawrence