Re: Re design & checking tools

[Bryan Scattergood <bryan@xxxxxxxx>]

Ian East wrote:
> Jeremy Martin wrote:
> >* This leads us to the point that Bryan made about state-space
> >  explosion. A single input of an INT32 variable in an Occam process
> >  would give rise to at least 2^32 states in the equivalent state
> >  transition system, so we need to apply some sort abstraction
> >  to reduce the number of states in each constitutent process.
> >
> >* This abstraction is difficult to automate - how do we decide how
> >  much information may be safely thrown away? Some very important work
> >  in this area has been done by Ranko Lazic (see Bill Roscoe's book:
> >  The Theory and Practice of Concurrency - Prentice Hall). 
> >
> >* Much work has also been done regarding state-space compression. I
> >  wonder if there might not be some kind of higher-level state machine,
> >  that could be used, where the input of an INT32 variable would only
> >  require one new state to be added?

It is possible to imagine state machines which work more symbolically;
when values are input we defer any decision on _which_ value for as
long as possible. The two problems with that are closure (determining
when states have been visited before) and efficiency (states checked
per second).

> Surely this has to do just with degree of abstraction. The only reason 
> for considering a single state for each state value (eg with an INT32) is 
> if the process behaves differently with regard to others according to 
> every distinct case (0, 1 , 2 etc). This is rarely true.

This sort of abstraction is usually obvious to a human, but as Jeremy
said, it is hard to automate. The same work is involved in producing
(say) a tractable CSP model of an existing implementation, but that
currently requires a competent CSP user and is tedious and
error-prone.

> What we can do (as suggested in the last chapter of my little book) is 
> _partition_ the domain of that INT32 according to process behaviour, and 
> define a distinct shared event for each sub-domain.

Essentially this is what Lazic's data-independence theory does.
Intuitively, the size of the partition is driven by equality tests.
(There are subtleties since synchronisations contain implicit equality
tests.) The work is significant because it has

* Theorems giving (static) bounds for the partition size.

* Criteria for when the bounds exist.

Together those should be enough to allow for automation.

	 Bryan