[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Re design & checking tools
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
> 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
> 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.