[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Introducing Spin.



In standard (FD) CSP div has two responsibilities:-

1) to model livelock;

and

2) to represent the worst possible process (it is the bottom of the refinement partial order).


In CSPP, "div" only describes livelock, matching 1) but not 2) above.
CSPP "div" is very far from the bottom of the refinement order: it is immediately below the top miraculous element.

This is a source of confusion for people familiar with the standard interpretation, not helped by the connotations of "divergence".

I have therefore decided to do what I ought to have done much earlier: change the name. So I will now call it "Spin". Hence in CSPP we have the 3 elementary processes (Stop, Skip, Spin) whereas it is (Stop,Skip,div) in standard CSP.

So standard CSP is more abstract than CSPP in handling livelock: in fact it cannot represent pure livelock.

This is only a change in the name: nothing else. One reason that I stayed with div for so long is that in practical CSP most uses of "div" can just be replaced by "Spin" to get the equivalent CSPP. The reverse was not always true, hence the confusion...

I have updated the tutorial to reflect this change, although that is primarily about standard CSP:

  http://www-staff.lboro.ac.uk/~coael/download/csptut.pdf
and
  http://www-staff.lboro.ac.uk/~coael/download/csptut.pdf.bz2 .

And all the gory details in
  http://www-staff.lboro.ac.uk/~coael/download/thcspp.ps.gz
have also been updated to use Spin.

Comments welcome. Thanks to Michael Goldsmith for making me think about this.

Adrian

--
Dr A E Lawrence
http://www-staff.lboro.ac.uk/~coael/