Re: [moca] definitions of race conditions?

["Cormac Flanagan" <cormac@xxxxxxxxxxx>]

Martin Berger wrote:
> this suggests to me
> that race conditions are "really" failures of atomicity: the semantics
> or specifications of a program require that a block of code is executed
> atomically or deterministically or at least in a manner satisfying
> church-rosser or something like that, but the implementation does not
> guarantee this, presumably because of concurrency.

I would certainly agree that atomicity is crucial in reasoning about concurrent programs, since we can analyze each atomic block using sequential reasoning techniques. Race conditions are a very good heuristic for detecting unintended atomicity violations, but they are only a heuristic. It turns out that race-freedom is neither necessary nor sufficient for ensuring atomicity. 

Perhaps a better correctness property to focus on is atomicity, and in particular the question:

	Is a given code block atomic? 

My recent work has focused on developing a type system to verify such properties (see Flanagan&Qadeer, TLDI'03/PLDI'03). In this approach, the programmer specifies which code blocks and methods are intended to be atomic, much like programmers currently specify which variables should hold integer values. Provided the program type-checks, the programmer can safely reason about atomic code blocks using sequential reasoning techniques, and can ignore interleaved actions of concurrent threads since the type system has proven that they essentially "commute away".

> to see why i have a problem with this definition consider the
> following procedure.
> 
>     void transfer( Account from, Account to, Money amountToTransfer )
>     {
>         from.amount := from.amount - amountToTransfer;
>         to.amount := to.amount + amountToTransfer
>     }
> 
> does it have a race condition?
> 
> it depends. if it is executed sequentially, then clearly not. but what
> if we execute
> 
>     transfer( from, to, 100 )  |  transfer( from, to, -32 )?
> 
> well, if Money is a synonym for 32bit words on a 32bit CPU, then this
> program is not exhibiting race conditions according to my (and
> flanagan&abadi's) definition, because of the atomicity of 32 bit
> memory accesses. 

As a minor correction, according to the definition of race conditions in our "types for safe locking" paper, the above program does have a race condition. In particular, the program can reach a state where both threads are about to access "from.amount", which satisfies our definition of a race condition.


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