Re: CSP, JMM and better processor architectures

["P.H.Welch" <P.H.Welch@xxxxxxxxx>]

Richard,

> Fortunately, it turned out that they didn't need to be scared: all
> the other shared variable accesses in the kernel were sensibly guarded
> by semaphores.  It was only this one instance where, to avoid a problem
> with nesting of locked regions, they had carefully reasoned that one
> lock could safely be eliminated.  But the proof depended on implicit
> assumptions about memory coherence which turned out to be too optimistic.

It was exactly this line of reasoning that led to the failure (race hazard
leading to deadlock) of the original monitor algorithms for the JCSP
ALT implementation.  I had to avoid a deadlock by removing a lock and
thought I had "carefully reasoned" that it would be safe - I was wrong.
The fixed algorithm, with the lock back in, avoided the deadlock by
cutting out another shortcut into which I had been tempted.  The now
verified code is much prettier than the incorrect clever one ...

> The moral: using shared variables is hard, and the cleverer you are
> the harder it gets.

Yup ... don't do it ... use languages that won't allow it ... and get fast
syncs instead and eliminate deadlock by correct (even verified) design.

;)

Peter.