CSP Patterns and Style for OO: The good the bad and the ugly?

[gordon_hutchison@xxxxxxxxxx]

Dear All,

I am very interested in modelling OO systems in CSP and
my interest was caught by one of Marcel's points
in his append to java-threads@xxxxxxxxx

Therefore: If you love CSP, and want to make it rule the world
  - Beware to stay realistic: also CSP has weaker points.

As a real fan of CSP and as someone who uses it (a little and to no great
degree of expertise)
to model both Java and the JVM I am aware of some common patterns that
turn up when modelling commercial software that perhaps might be stemming
from the CSP notation rather from the underlying problem I am trying to
model.

Do other people see the same patterns and do they consider them
syntactically clumsy
or a necessary part of the exactness of a mathematical model?

How often when designing a network of processes that represent an OO system
does
one end up with a design of channels/events of the form:

1) class_name.method_name.this_instance.target_instance
(here the classname is really used for labelling and is often omitted)

Can the pattern be abstracted and specific instances of it expressed more
succinctly/powerfully?

It reminds me a little of the non-OO, OO systems such as SOM for C which
drag 'this' around as a parameter to all the methods.

Does the occurrence of this pattern indicate a level of inexperience in the
CSP
skills of the author or is it a necessary part of crossing between the
domains of
OO and process algebra?

2) Manually assigned limits in the models targeted for tool assisted
checking.

The desire, especially when the model is going to be checked by
some tool such as FDR,  to limit the state explosion by placing limits
on the system. These limits stem from the capacity of our tools rather
than the problem domain.

An example of this is a fixed number of 'instances' of a particular
process.
Often these are composed into a 'pool' of such with a parallel composition.
The dynamic nature of the system modelled by having processes start
and return for recycling to some sleeping state.

There is an almost unstated proposal when these are introduced that they
form a sufficient base case for the induction: "If I can prove the
properties
I seek with these limits then they will also hold with larger networks".

However on what basis are these limits proven to be sufficient
(and ideally minimal) and is anyone working on the mathematics (and
modelling
notation to express) that these values could be calculated and as such
abstracted
out of a human friendly model of a system.

3) CSP models can sometimes appear clumsy with regard to typing

For example in the model of java threads
http://www.cs.ukc.ac.uk/projects/ofa/java-threads/203.html

How often do the phrases "t in Threads" and "O in Objects" appear?
Would it be helpful or would it result in lack of clarity to be able to
express this
more concisely?

The cultural convention is that Threads and Objects can be constrained
down to some small set of values (say 3 or 5) that will allow the machine
checking
of the model.  The model above also shows the common "method.target.this"
pattern.


4) State centralises as behavior becomes more deterministic.

Aspects of CSP models often have decentralised 'state' and fully
non-deterministic
choices. For example one can model all the threads waiting for a monitor
purely by
the set of thread processes that are offering the
'wait-exit/monitor-reentry'
events with the monitor in question simply choosing when the event occurs
rather than which thread takes part [well without dynamic alphabets all the
threads will
actually take part just that only of them will move to a new state - see
point 5) ].

Constructed software is usually much more deterministic. Being able to
model
event selection priorities and also some notion of 'fairness' or event
'queueing'
in a compact manner would be a powerful aid in modelling some systems. In
doing
this with CSP one tends to artificially centralise state too early e.g.
"if the set of notified-waiters is non-empty allow one of them to
re-enter/lock
else allow a fresh monitor entry/lock" requires a set of 'notified-waiters'
to
be maintained - twice, both in the set of processes currently offering this
event and
once by the monitor via this set. One thinks of a set construction operator
along the lines of
'(some instance data of) the set of processes currently offering this
event'  - but
here I am straying too far from the fact that we have a declarative model
not
a running system perhaps.

5)  Without dynamic alphabets would we want a shorthand for 'ignore these
events'?

This pattern seems to turn up when one is modelling networks of processes
that have transient associations - such as that classes that have dynamic
relationships between particular instances.

How often does one see a term something like:

IgnoreEventsNotForMe(me) = channel.event.object:{ o | o <- Objects, o!=me}
->Process(me)

Process(me) =   channel.event.me -> NewProcess(me)
                 [] IgnoreEventsNotForMe

Of course this becomes cumbersome if one is dragging state through
some process 'parameters' or if one has lots of different channels.

I am not proposing dynamic alphabets as such
(I must keep remembering its declarative)
just a little syntactic sugar to make the model clear and succinct.
=================================================

Tinkering with CSP may destroy some of its important properties -
notably its feeling of 'cleanness' and the vital ability to push refinement
through composition - so I am very reticent about the above 'aids' - all
of them can be expressed in the basic CSP after all.

I would be very happy to have these suggestions rigorously disposed
of by those perhaps more experienced or clearer thinking than myself -
as I would learn a lot about CSP and modelling OO (and Java) systems
in CSP in the process.


Gordon Hutchison
IBM Java Technology Centre,
IBM Hursley, UK.
Notes:   Gordon Hutchison/UK/IBM
Internet: gordon_hutchison@xxxxxxxxxx
Phone: (+44)/(0) 1962 815646 (Internal IBMUK-245646)