OK, I did what I should have done in the first place, which is a
literature search; thank goodness for citeseer! The paper I found with
the best discussion on this topic is:
R.H.B. Netzer, B.P.Miller,
"What are Race Conditions? - Some Issues and Formalizations ",
ACM Letters on Progr. Languages and Systems, Vol. 1(1) (1992).
http://citeseer.nj.nec.com/netzer92what.html
which uses the terminology "data race" for r/w and w/w conflict, and the
terminology "general race" for nondeterminism caused by timing. "Data
race" is certainly a widely accepted term (138 papers found by
citeseer); "general race" doesn't seem to have caught on as well (only
12 papers found by citeseer). Netzer (in his Ph.D. thesis) says in
passing that "previous work uses the term race condition [for general
race]".
You're looking for a defn of "data race", I was providing a defn of
"general race". Hence the confusion.
The rest of this email is a reply back to some of Martin's points...
> > 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.
I have always learned that races are a fact of life in concurrent
programs, the problem is making sure they don't cause safety violations.
> 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".
OK, typo spotted. If you want an example which doesn't depend on the
atomicity of assignment, take:
local y = 0;
( y := 1 | y := 0 );
if (y == 0)
then x := 2; x := 22;
else x := 22; x := 2;
> 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 sounds like what you're looking for is a model which allows for
atomic high-level operations to be mapped to multiple low-level
operations (and therefore to lose atomicity), i.e. a model which
supports action refinement. This is going to get you into the world of
true concurrency models, since action refinement breaks the expansion
lemma (refining a to cd allows you to distinguish a|b and ab+ba). As
you said:
> the problem is that the translation does not preserve
> atomicity.
Action refinement has quite a literature, and I'm not really a good
person to recommend a starting point for a literature review. Luca
Aceto's thesis might be somewhere to start from, and has the advantage
of existing in book form in CUP's Distinguished Dissertation series.
Of course, even once you've dealt with non-atomic read/write, you've
still got to deal with the non-serial memory model that many languages
(e.g. C, Java) have, which results in weird inequivalences like:
Object lock = new Object (); synchronize (lock) { }
is not equivalent to:
Object lock = new Object ();
> i think it is pushing things slightly to say that this is *the*
> standard argument. but it suggests some questions: what is stochastic
> choice in this context (i mean, can it be described just in the
> language of reduction systems for example? and is stochastic
> choice enough to express concurrency?
I think I'll keep pushing on this one (although I should have just said
"choice" and not "stochastic choice"). The decision to equate choice
with concurrency is at the heart of the distinction between interleaving
and non-interleaving models.
Cheers,
Alan.
PS: Action refinement, non-interleaving models, time warp, which George
Bush is president right now?
--
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