From owner-occam-com-out@ukc.ac.uk Wed Aug 22 06:15:02 2001 To: java-threads@ukc.ac.uk, occam-com@ukc.ac.uk, CSPUG@JISCMAIL.AC.UK MIME-Version: 1.0 X-Mailer: Lotus Notes Release 5.0.7 March 21, 2001 From: "Gordon Hutchison" Date: Wed, 22 Aug 2001 14:13:46 +0100 X-MIMETrack: Serialize by Router on d06ml006/06/M/IBM(Release 5.0.6 |December 14, 2000) at 22/08/2001 14:13:58, Serialize complete at 22/08/2001 14:13:58 Content-Type: text/plain; charset="us-ascii" Message-ID: Precedence: bulk I am afraid I do not have a very good tool for 'replying' to posts neatly - none the less I am responding to: A E Lawrence wrote: > > Gordon Hutchison wrote: > > > > (Note I have copied CSPUG@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. 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@uk.ibm.com Phone: (+44)/(0) 1962 815646 (Internal IBMUK-245646)