Re: [moca] definitions of race conditions?

["Cormac Flanagan" <cormac@xxxxxxxxxxx>]

> > Race conditions are a very good heuristic for detecting unintended
> > atomicity violations, but they are only a heuristic.
> 
> that's a very good observation. that makes a lot of sense and clarifies
> a lot of things!
> 
> the next level of confusion for me now is that some race conditions
> are indeed indicative of a problem, but some others are just the
> opposite: i mean those races that are used to implement
> mutexes/semaphores and the like. we seem to need races to guarantee
> atomicity! can one come up with a neat criterion to distinguish them?

As you point out, there is indeed a race on the mutex, which controls which atomic block gets executed first, and so we get non-determinism as to the order in which the atomic blocks of the various threads are executed. Essentially, atomicity increases the granularity of interleaving, but still leaves open the question of how to verify that all possible interleavings of the atomic blocks of the various threads lead to correct program behavior.

Cormac.
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html