Hmm, my original reply went just to Martin, but his reply went to the
whole list... Oh well.
> > I don't have a citation to back this up, but I always thought of a race
> > condition as being any failure of the diamond property,
>
> but that's way too rqestrictive. it would decree just about any
> concurrent program i have ever, including
>
> lock( mutex ) | lock( mutex )
> x := 2 | x := 22
> unlock( mutex ) | unlock( mutex ),
>
> to be suffereing from race conditions.
Yes, I think this program does have a race condition: there's a race as
to which thread locks the mutex first. 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);
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):
=> =x:=2=> =x:=22=>
//
start
\\
=> =x:=22=> =x:=2=>
so any such definition is going to fail to preserve graph isomorphism,
which is going to make "race condition" a syntactic property rather than
a semantic property (at least for any semantics coarser than graph
isomorphism on lts's).
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.
It seems that the main difference here is whether you think race
conditions are a semantic or a syntactic property.
Cheers,
Alan.
PS: My original reply to Martin's email was:
Hi Martin,
I don't have a citation to back this up, but I always thought of a race
condition as being any failure of the diamond property, that is two
distinct transitions:
P1 <-a1- P -a2-> P2
such that there is no P' satisfying:
P1 -a2-> P' <-a1- P2
One instance of this is read/write and write/write conflicts, which is
the defn you proposed. In some languages, the only race conditions are
r/w and w/w conflicts, but that's not always the case (e.g. pi-c).
My 2p (or 3c over here).
Alan.
PPS: One counterargument to the defn of race condition as failing to
satisfy diamond is that it equates nondeterminism caused by parallelism
with nondeterminism generated by stochastic choice: this is the standard
argument for non-interleaving models, so if you're worried about this
you'd need to replay the defn in your favourite true concurrency model.
--
Alan Jeffrey http://fpl.cs.depaul.edu/ajeffrey/
CTI, DePaul Univ., 243 S. Wabash Ave, Chicago, IL 60604, USA
Attachment:
signature.asc
Description: This is a digitally signed message part