[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Priority modeling with CSP?
A E Lawrence wrote:
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.
I forgot to add that I think the above identification of priority and time
only applies in an interleaving semantics. Of course, original pure CSP is
based on an interleaving semantics. Indeed, that is one gloss we can give
nowadays to the word "sequential" in the name which we may otherwise think
to be an anachronism.
But when we are modelling a synchronous circuit in full detail,
interleaving semantics is inadequate. But it is possible to add true
concurrency into CSP with very little change including retention of traces.
Of course, you can no longer have
( a -> Stop) ||| (b -> Stop) = (a -> b -> Stop)  (b -> a -> Stop)
When true concurrency is present there is another possibility:
a and b happening together. Furthermore, most implementations, in hardware
at least will be "eager" : that is perform a and b together if they are
both offered. In HCSP there is an eager refinment of ||| that does exactly
that. All this works out with very little change to standard CSP. And if
you have an (global) alphabet which excludes concurrent events -- then you
get standard CSP back. And the equation above holds again.
I expect to present that and more at CPA2002 :-)
Dr A E Lawrence