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

oleksandr otenko oleksandr.otenko at oracle.com
Mon Apr 15 13:44:58 EDT 2013


My example wasn't even showing the actual thing, because unfortunately 
it is based on a trivial one-field access.

Happens-before is more powerful when considered as a thread-local 
property. It is pointless to consider just one write. What is important, 
is the ordering of all other reads and writes preceding the volatile 
store - in the writing thread. Then you can use the value of the last 
stored variable as evidence, when reasoning about the state transition 
that thread undertook.

So, back to your example - if this.shared is not volatile, a more 
powerful observation is that even if local == 10 there is no ordering 
with respect to other effects observed and applied in that other thread. 
And back to my point - when you declare it volatile, you are not 
creating a happens-before between the write and the read in another 
thread; you are creating a happens-before edge between all preceding 
reads and writes in the mutator thread and a store to this.shared.


With regards to "how to express validity". I pepper my code with 
asserts. But not everything can be expressed with simple tests of a few 
variables - sometimes it is necessary to assert a system-wide property.


Alex


On 15/04/2013 18:07, thurstonn wrote:
> oleksandr otenko wrote
>> happens-before is sooo misunderstood!..
>>
>> What do you mean - "no explicit happens-before"? happens-before doesn't
>> create barriers "between threads"; volatile or not, locked or not, there
>> is no order enforced between the first and the second thread.
>> happens-before is a *reasoning mode* about visibility of effects from
>> another thread.
>>
>> In this example, you need to show:
>>
>> this.shared was 0.
>>
>> this.shared = 10               local = this.shared;
>>
>> if (local == 10) "this.shared = 10" happens-before "local = this.shared"
>> else unknown
>>
>>
>> Alex
> I do understand happens-before, the difficulty is talking about it.
> What I mean is that given the code (no explicit "happens-before"),
>
> local == 0 (one possible outcome) tells you *nothing* about the partial
> ordering of this.shared = 10, i.e. the write may or may not have 'happened'
>
> now with an explicit "happens-before", e.g.
> volatile int shared = 0
> . . .
>
> if local == 0, then there is a partial ordering defined between the writer
> and reader threads (the reader < writer)
>
> Perhaps "explicit happens-before" is grating to your eyes, but you shouldn't
> presume that it means that I don't understand
>
>
>
>
>
>
>
>
>
>
> On 14/04/2013 02:42, thurstonn wrote:
>> Before I answer fully, let me ask you about another variant of the
>> program:
>>
>>
>> Thread 1                     Thread 2
>> this.shared = 10            local = this.shared
>>
>> Is this "racy"?  Clearly there is no explicit happens-before.  But, at
>> least
>> in my reading of the (your) definition that I quoted in my OP, it wouldn't
>> qualify as a data-race.
>>
>>
>>
>> --
>> View this message in context:
>> http://jsr166-concurrency.10961.n7.nabble.com/On-A-Formal-Definition-of-Data-Race-tp9408p9413.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
>
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest at .oswego
> 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-tp9408p9426.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/c91a83eb/attachment.html>


More information about the Concurrency-interest mailing list