Re: [moca] definitions of race conditions?

[martinb@xxxxxxxxxxxxxx]

> 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?

> 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?

totally agree.

>> 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.

yes, but what has puzzled me (and is now a lot clearer) is that in
case of atomic memory access, the problem with the above program is
not syntactic possibility of concurrent access but the dodgy interleavings
between different memory accesses, i.e. violation of a more general atomicity
constraint.

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