[concurrency-interest] On A Formal Definition of 'Data-Race'

oleksandr otenko oleksandr.otenko at oracle.com
Mon Apr 15 10:31:50 EDT 2013

When "data race" means "broken logic", there must be a place where that 
logic is defined.

Literature on linearizability introduces a history of events (not the 
only place where it is done so). If a valid reordering of events 
produces a invalid history, you have a data race. But you need a 
definition of a valid history.

Your argument is that any reordering of instructions in your example is 
a valid history. But in order to state that, we would need to see the 
rest of history. The subsequent use of local will determine the validity 
of history.


On 12/04/2013 19:55, thurstonn wrote:
> In thinking about whether code is thread-safe or not, one can attempt to
> identify whether it 'contains a data-race'.  If not, you're good.  Else you
> need to add an explicit happens-before relationship.
> Which begs the question: what exactly constitutes a 'data-race'?  And here
> I'm interested in something a little more formal than the famed judicial
> judgement of obscenity (I know it when I see it)
> If you do a web search, you unfortunately get quite a few divergent
> definitions, many of which seem to be inconsistent.
> IIRC, the official JMM defines a data-race as any two conflicting operations
> from two or more threads on shared data (where at least one of the two
> operations is a write).
> Brian Goetz (in his excellent  article
> <http://www.ibm.com/developerworks/library/j-jtp03304/>  ) defines data-race
> thusly:
> "A program is said to have a data race, and therefore not be a "properly
> synchronized" program, when there is a variable that is read by more than
> one thread, written by at least one thread, and the write and the reads are
> not ordered by a happens-before relationship."
> But this would mark the following code as a data-race
> int shared = 0
> Thread 1                  Thread 2                 Thread 3
> local = this.shared      this.shared = 10       local = this.shared
> This clearly meets his definition, yet I do not consider this a 'data-race'.
> I've always relied on traditional database concurrency control theory (I
> still find the treatise by Bernstein, Hadzilacos, and Goodman to be the
> best), which has a formal definition of 'serializability', viz. that any
> transaction log is 'serializable', if and only if, its serialization graph
> is acyclic.  Why can we not use this as the basis for a formal definition of
> 'data-race' (excluding the notion of commit and abort of course):
> "A program is said to have a data-race, if any legal (as prescribed by the
> MM) execution order produces a serialization graph that is *cyclic*"
> It has the advantage of a formal, mathematical model and although it is has
> historically been confined to databases (and transactions), it seems
> applicable to concurrent execution of any kind?
> Hoping that I don't get flamed.
> --
> View this message in context: http://jsr166-concurrency.10961.n7.nabble.com/On-A-Formal-Definition-of-Data-Race-tp9408.html
> Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest at cs.oswego.edu
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20130415/bb70b483/attachment.html>

More information about the Concurrency-interest mailing list