From: Gordon Hutchison (gordon_hutchison_at_email.domain.hidden)
Date: 2001-08-22 14:13:46
I am afraid I do not have a very good tool for 'replying' to posts neatly
-
none the less I am responding to:
<start>
A E Lawrence wrote:
>
> Gordon Hutchison wrote:
> >
> > (Note I have copied CSPUG_at_JISCMAIL.AC.UK - we need one place for this
> > like "comp.X.processalgebra"perhaps)
> >
> > I was quite interested in the references from Adrian Lawrence to CSP
> > models
> > that tried to describe more about which actual event is accepted/fired
> > rather that the set of possible
> > events in the ready set. CSPP etc.
>
> If you are concerned with the model itself, rather than mapping onto
> real world events I see no reason why what you suggest below might not
> work. For me. at least, my Acceptances seems more intuitive and much
> closer in spirit to the Failures style. Your suggestion is a bit more
> operational. Not that that is a problem.
>
> Acceptances does allow me to capture several sorts of useful priority
> (e-priority and p-priority), and now, thanks to Bill Roscoe's
> suggestion, neutrality in the form of "compliant" processes.
>
> > This seems less 'clean' to me to model what actually will be accepted
in
> > the model itself.
> >
> > Could one not take a 'standard' CSP model plus a set of rules
(meta-model)
> > that relate to the
> > "firing engine" (eg given this ready set of events - probably
decorated
> > in some
> > way by the participating processes) that results in a subsetting of
the
> > traces.
> > I am thinking along the lines of controlling the selection of the next
> > event into
> > the combined trace possibly based on both the types of events and the
> > processes involved.
> >
> > This might be a cleaner road to a refinement order from possibilities
to
> > actualities? CSP models
> > often have 'governing' type process added just to control event
selection
> > in this way.
I don't really know enough about operational semantics, but would the
approach above give you a simple way of defining fixed points for
recursion? Acceptances does rather well in that area, including
unbounded behaviour.
<end>
I guess you are right, my view of the CSP world is very operational (I am
just
a jobbing programmer you see so tend to think of CSP in terms of its
operational semantics - or more exactly the operational semantics of the
few wmodels I have written and how they relate to the software I am
modelling. I do this generally because I want to check something
eg search for some timing window; or prove something - like some
'optimization' of a locking algorithm is really a refinement; or sort out
in my
head some concurrent behaviour.
I am attracted to the idea of being able to factor a prioritized model
into
a vanilla CSP model and another chunk (that in my operational world view
would
affect the 'firing rules' - what a programmer like me might wrongly think
as the
thing analogous to the scheduler).
where prioritized_model = vanilla_model operatorP meta_model
and then if one worked carefully on the meanings then by definition the
priorized_model would always be a refinement (under the semantics) of the
vanilla_model, the meta_model just selecting the subset of
traces/failures.
Plainly my thinking is rather wooly to discuss at this level (so I will
have to do
some revision :-) )
I am drawn to this idea that just as one cannot always (ie NEVER)
rely on the OS schedular to save one from being found out when
writing concurrent programs with races/timing windows but testing well.
(It somehow knows how to apply the most fiendish combination
of thread progression ONCE the code has left your machine.)
I think there is something, probably a much smaller thing than addressed
by Acceptances,
in a form of prioritisation that provides for a strict refinement of a
non-prioritised version of a model that can be easily split out and which
represents the semantics of some software + the behaviour of its (read
operating system)
environment - eg which waiting locker will get a OS mutex - the OS chooses
based on priority,time-of-arrival,priority-inheritance etc
but we do not want such things to clutter every individual model
rather we want some re-usable meta-model?
Would this be useful?
Gordon Hutchison
IBM Java Technology Centre,
IBM Hursley, UK.
Notes: Gordon Hutchison/UK/IBM
Internet: gordon_hutchison_at_uk.ibm.com
Phone: (+44)/(0) 1962 815646 (Internal IBMUK-245646)
This archive was generated by hypermail 2.1.7 on 2004-10-31 20:03:59 GMT
© Copyright WoTUG
All rights reserved