Re: [moca] definitions of race conditions?

[Martin Berger <martinb@xxxxxxxxxxxxxx>]

> could you please tell me the source of this definition? I'm
> interested.

from nowhere in particular. i made it up for my moca posting,
reflecting what i seem to have read in many a concurrency theory
text. for a prototypical example you could look at page 9 of "types
for safe locking" by flanagan and abadi.

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. but that is clearly wrong.  if we ran two
instantiations of transfer in parallel, we expect it to behave as if
we had written

   void transfer( Account from, Account to, Money amountToTransfer )
   {
       from.lock();
       to.lock();

       from.amount := from.amount - amountToTransfer;
       to.amount := to.amount + amountToTransfer

       from.unlock();
       to.unlock();
   }

in other words, we expect

   from.amount := from.amount - amountToTransfer;
   to.amount := to.amount + amountToTransfer

to be executed atomically. however, what if, in the first definition
of transfer, Money was a synonym for 64bit word, but still executed on
a 32 bit machine? would my definition indicate a race condition?  i
can think of two answers:

* no, despite the fact that each read or write access to an instance of
  Money now takes two memory accesses, which can be interrupted and
  hence corrupted. why would it still not be a race condition? again
  because the hardware guarantees that at most one memory access at
  a time.

* yes, because -- from the point of view of the high level language --
  each access to a memory location takes two physical accesses and
  if one thread starts to write at x at cpu-cycle t and another at
  cpu-cycle t+1, we have two threads accessing x at overlapping
  intervals.

this suggests to me that the proposed definition is too simple.
what's really going on in race conditions is violation of atomicity,
and that cannot be determined just by looking at when reads and writes
are done. but what counts as an atomic or "critical" part of a
program?  can that even be seen just by looking at code?

what if the above programs weren't nicked from banking software, but
rather my entry to last years "obfuscated toy-language coding contest,
and their intended behaviour was that of a random generator?

so i guess my question is: where can i find throughly formal accounts
of race conditions in the sense that i have tried to describe? of
course my aim is to see how such accounts pan out in the pi-calculus.

martin

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