Re: [moca] definitions of race conditions?

[martinb@xxxxxxxxxxxxxx]

Alan Jeffrey wrote:

> Hmm, my original reply went just to Martin, but his reply went to the
> whole list...  Oh well.

i apologise for the mistake. i realised too late that your (and
somebody else's) mail wasn't sent to moca, probably because it had
"moca" in its subject line and hence appeared in my moca folder.

> Yes, I think this program does have a race condition: there's a race as
> to which thread locks the mutex first.

that's right, but that isn't a problem. i have always learned that
races are bad and must be avoided.

>  Presumably you're looking for a
> definition where the following program (it's the same as your example
> but with the mutex made local) does not have a race condition:
>
>     local mutex = unlocked;
>        lock( mutex )     |    lock( mutex )
>        x := 2            |    x := 22
>        unlock( mutex )   |    unlock( mutex ),
> but the following program does:
>
>     local y = 0;
>        ( y := 2 | y := 22 );
>        x := y; x := (20-y);

exactly

> but these programs have graph-isomorphic lts's (up to eliding some
> beta-reductions which do satisfy the diamond property -- adding enough
> dummy tau steps to the examples will actually make them graph
> isomorphic):

if you write 24-y instead of 20-y and, more importantly, if you assume
that assignment is atomic. this latter assumption cannot be taken for
granted (think of 64 bit integers on a 32 bit machine) and is at the
heart of my quest for a good definition of "race conditions".

> If we consider the following definitions of an IntRef class:
>
>   class IntRef {
>     private int contents;
>     int get () { return contents; }
>     void set (int x) { contents = x; }
>   }
>
> and:
>
>   class IntRef {
>     private int contents; private Object lock = new Object ();
>     int get () { synchronized (lock) { return contents; } }
>     void set (int x) { synchronized (lock) { contents = x; } }
>   }
>
> under most any semantics I can think of (ignoring stale objects and
> other weirdnesses of the Java memory model for now) these classes will
> be equivalent, but the former has a race condition (in the sense of r/w
> and w/w conflicts), and the latter does not since all the race
> conditions (in the sense of failing to satisfy diamond) are on acquiring
> locks.

yes and no. the problem is that most implementations of locks i can
think of work by a race between two atomic writes. 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.

> It seems that the main difference here is whether you think race
> conditions are a semantic or a syntactic property.

from what i've said, i think the conclusion can only be that its
a semantic property. however, from experience as working programmers
we have (minimal) expectations as to what the units of atomicity in
a program must be. in particular we want assignments or statements
like x := x + 2 to atomic. hence, if such statements work on shared
variables, they must be guarded by locking. but here comes the twist
that makes r/w or w/w conflicts too weak a criterion for race conditions:
if we translate x:=x+2 into some lower-level language like this:

  lock( mutex )
  r1 := readMemoryLocation( x )
  unlock( mutex )
  add r1, 2
  lock( mutex )
  writeToMemoryLocation( x, r1 )
  unlock( mutex )

then we don't seem to have any relevant r/w or w/w conflicts, and yet
the program suffers from a race condition w.r.t. the source program's
semantics. the problem is that the translation does not preserve
atomicity.

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