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

Vitaly Davidovich vitalyd at gmail.com
Mon Apr 15 20:12:17 EDT 2013


Yes, threading is hard :) There's nothing stopping people from using
different designs to minimize the hairy parts (e.g. message passing,
immutability, etc) in java.  Deliberate data races are an "expert"-only
tool, and last resort at that.  I think this list typically reiterates that
point when the subject comes up.
On Apr 15, 2013 6:46 PM, "Gregg Wonderly" <gregg at cytetech.com> wrote:

> Happens-before doesn't play a part in program=order, only thread-order.
>  This is the problem that a lot of developers seem to struggle with.  If
> you want the history of all possible paths, then the complexity of that
> possibility is huge.  Basically for X unrelated instructions, the possible
> histories are X^2. Because happens-before injects a "barrier", it can
> appear to simplify the complexity, but, the global ordering still is X^2
> for all "blocks" between happens-before spots.
>
> This is why I keep waving my hands here, and saying "stop that".  It makes
> it extremely difficult for "racy" software to be understood as "racy",
> because "reordering" introduces a whole realm of "unknown compiler
> reorderings changing JLS specified behaviors" that many developers, may not
> recognize as needing their attention.  I still encounter developers who
> just don't understand that the JLS doesn't describe "inter-thread"
> behaviors, because of the JMM.  People expect that they will just see data
> races, and not programmatic run time data corruption such as the
> Thread.getThread()/.setThread(**) discussion here revealed.
>
> Many people pick java for the some reason that James Gosling wrote quite
> some time ago, regarding it working correctly.  The JLS and JMM decoupling
> of "behaviors" causes software to break with "corrupted data" (word tearing
> included) and that's something which I don't think is on the radar for as
> many people writing Java software, as seems to be expected by the
> aggressive demands on the JMM being perfectly understood and adhered to.
>
> Gregg
>
> On 4/15/2013 2:18 PM, oleksandr otenko wrote:
>
>>
>> On 15/04/2013 17:55, thurstonn wrote:
>>
>>> oleksandr otenko wrote
>>>
>>>> When "data race" means "broken logic", there must be a place where that
>>>> logic is defined.
>>>>
>>> Yes, there is an assumption in my OP that "data-race" ==> "incorrect" (or
>>> "broken logic" in your words)
>>> Vitaly does not necessarily equate "raciness" with "incorrectness" (and
>>> probably Brian as well) and that's OK with me
>>>
>>> oleksandr otenko wrote
>>>
>>>> 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.
>>>>
>>> Yes, what I'm in (a quixotic?) search for is a process that does the
>>> following:
>>> given a set of operations that can execute across multiple threads (like
>>> the
>>> example in the OP)
>>> -define a set of "execution histories" (your "history of events") that
>>> are
>>> possible given the MM in effect and consistent with the original
>>> program's
>>> set of operations (of course there will be multiple such histories)
>>> -each "execution history" defines at least a partial ordering among
>>> conflicting operations (r/w or w/w on the same shared data item)
>>> -analyze each execution history for "correctness"
>>> if each possible history is correct, then you're good
>>> else add explicit happens-before relations. Repeat
>>>
>> This sounds awfully like Java PathFinder.
>>
>> Not tractable for less-trivial code. (I couldn't test a semaphore-like
>> primitive
>> with more than 4 threads).
>>
>>
>> Alex
>>
>>
>>  oleksandr otenko wrote
>>>
>>>> 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.
>>>> Alex
>>>>
>>> Agreed (the example 'program' is simplistic at best).
>>>
>>> What my original post described was exactly the kind of process (viz. an
>>> acyclic serialization graph) that I'm in search of, but is applied to
>>> database concurrency control.  The problems are very similar (turning
>>> concurrent executions into serial, partially-ordered ones; operations are
>>> reads/writes of data items), but they are not exactly the same.  I was
>>> wondering if we could use the same techniques (with a serialization graph
>>> ==> "execution graph") to analyze the "correctness" of, e.g. non-locking
>>> concurrent algorithms/data structures.
>>>
>>> Thurston
>>>
>>>
>>>
>>> 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/&gt<http://www.ibm.com/developerworks/library/j-jtp03304/&gt>;
>>>>  ) 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<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 .oswego
>>>> http://cs.oswego.edu/mailman/**listinfo/concurrency-interest<http://cs.oswego.edu/mailman/listinfo/concurrency-interest>
>>>>
>>>
>>> ______________________________**_________________
>>> Concurrency-interest mailing list
>>> Concurrency-interest at .oswego
>>> http://cs.oswego.edu/mailman/**listinfo/concurrency-interest<http://cs.oswego.edu/mailman/listinfo/concurrency-interest>
>>>
>>>
>>>
>>>
>>>
>>> --
>>> View this message in context:
>>> http://jsr166-concurrency.**10961.n7.nabble.com/On-A-**
>>> Formal-Definition-of-Data-**Race-tp9408p9425.html<http://jsr166-concurrency.10961.n7.nabble.com/On-A-Formal-Definition-of-Data-Race-tp9408p9425.html>
>>>
>>> Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
>>> ______________________________**_________________
>>> Concurrency-interest mailing list
>>> Concurrency-interest at cs.**oswego.edu<Concurrency-interest at cs.oswego.edu>
>>> http://cs.oswego.edu/mailman/**listinfo/concurrency-interest<http://cs.oswego.edu/mailman/listinfo/concurrency-interest>
>>>
>>
>> ______________________________**_________________
>> Concurrency-interest mailing list
>> Concurrency-interest at cs.**oswego.edu <Concurrency-interest at cs.oswego.edu>
>> http://cs.oswego.edu/mailman/**listinfo/concurrency-interest<http://cs.oswego.edu/mailman/listinfo/concurrency-interest>
>>
>>
>>
> ______________________________**_________________
> Concurrency-interest mailing list
> Concurrency-interest at cs.**oswego.edu <Concurrency-interest at cs.oswego.edu>
> http://cs.oswego.edu/mailman/**listinfo/concurrency-interest<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/3434f6a1/attachment-0001.html>


More information about the Concurrency-interest mailing list