Re: [moca] definitions of race conditions?

[martinb@xxxxxxxxxxxxxx]

> OK, I did what I should have done in the first place, which is a
> literature search; thank goodness for citeseer!

am i mad or is citeseer scanning papers and using OCR to extract
titles and abstracts?

> which uses the terminology "data race" for r/w and w/w conflict, and the
> terminology "general race" for nondeterminism caused by timing.

yes, i am trying to understand "data races". netzer's terminology does
not seem widespread. in particular, i have never really seen anyone
use "race condition" for general races ... but that may just show my
lacking erudition.

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

yes, but it should be possible to think about race condition without
reference to refinements, for otherwise we would end up with an
infinite sequence of refinements. it seems that having a way of
talking about the atomicity or granularity of a computation is the
key.  an atomicity operator should be some form of inverse to action
refinement, but so far i haven't been able to convert this vague
intuition into something mathematical sound.

> and has the advantage of existing in book form in CUP's
> Distinguished Dissertation series.

you mean the advantage of not being available on-line?

> Of course, even once you've dealt with non-atomic read/write, you've
> still got to deal with the non-serial memory model

indeed. that's where the fun really starts. i definitily wanna go there, but
simple things first!

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

yes, and it works very well indeed for untimed computation. as soon as
the computation can be made contingent upon timing, it breaks down though.

> PS: Action refinement, non-interleaving models, time warp, which George
> Bush is president right now?

eternal return of the same innit?

martin

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