On A Formal Definition of 'Data-Race'

classic Classic list List threaded Threaded
73 messages Options
1234
Reply | Threaded
Open this post in threaded view
|

On A Formal Definition of 'Data-Race'

thurstonn
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) 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.
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Ruslan Cheremin
As far, as I understand, notation of data race comes from technical, not mathematical point of view. Data race, defined as above, is exactly the case there it is hard for _implementation_ to hide dirty details of underlaying mechanics -- e.g that stores/loads are not "instant", and may have "stages", they can be pipelined, so started executing early and actually finished latter. Hide this details is not impossible, in theory, but just hard to implement. And because of this, it was decided to put on programmer the responsibility to "order" such instructions. There are exist algorithms to find and order such races, but, afaik, they are NP-complete with N around total instructions in program (i.e. such algorithms require global program analyze), so not practical today.

 
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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Boehm, Hans

Right.  The absence of a data race, as defined by the JMM guarantees that synchronization-free code sequences appear indivisible.  No other thread can see an intermediate state.  That means that:

 

-          Programmer no longer has to reason about instruction-level interleaving.  As far as they’re concerned, context switches only happen at synchronization operations, even if there is a multiprocessor involved.

-          It no longer matters whether your stores are done a byte or a word at a time.

-          Sync-free library calls to e.g. copying an array, are no different from single byte assignments; they appear to happen at once, and you no longer need to reason about intermediate, half-completed. int assignments behave like long assignments.

-          Compilers can optimize in a fairly conventional way within these sync-free regions, and you can’t tell the difference.

 

These can clearly not hold unless programs like the one below are considered to have a data race.

 

There are asymptotically efficient (perhaps 10x-100x slowdown) ways to test dynamically whether a data race has occurred.  (And much more efficiently with hardware assist.)  I don’t think there are practical ways to statically and fully accurately check non-tiny applications for data races.

 

Hans

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Ruslan Cheremin
Sent: Friday, April 12, 2013 12:12 PM
To: thurstonn
Cc: [hidden email]
Subject: Re: [concurrency-interest] On A Formal Definition of 'Data-Race'

 

As far, as I understand, notation of data race comes from technical, not mathematical point of view. Data race, defined as above, is exactly the case there it is hard for _implementation_ to hide dirty details of underlaying mechanics -- e.g that stores/loads are not "instant", and may have "stages", they can be pipelined, so started executing early and actually finished latter. Hide this details is not impossible, in theory, but just hard to implement. And because of this, it was decided to put on programmer the responsibility to "order" such instructions. There are exist algorithms to find and order such races, but, afaik, they are NP-complete with N around total instructions in program (i.e. such algorithms require global program analyze), so not practical today.

 

 

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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

 


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Brian Goetz-3
In reply to this post by thurstonn
Consider this similar-looking programing:

Object lock = new Object();
int shared = 0;

Thread 1: synchronized (lock) { local = shared; }
Thread 2: synchronized (lock) ( shared = 10; }
Thread 3: synchronized (lock) { local = shared; }

Is what you're saying "in either my racy program or Brian's non-racy
program, the effect will be the same -- threads 1 and 3 will each see
either 0 or 10, and can't predict which because they do not control the
timing of thread scheduling and lock acquisition", and from there, going
to "so why do we call one racy and not the other?"

In a properly synchronized program, you only see changes to shared
variables at synchronization points, whereas in a racy program, they
happen whenever, and the order in which they appear to happen may be
different from the perspective of different threads.

Or, maybe you just don't like the happens-before model because its
different from what you're used to?  HB seems no less well-defined and
tractable than the other models you seem to like.  The rules are simple:

  - Synchronization actions (lock acquire/release, volatile read/write)
are totally ordered
  - If two actions A and B are in the same thread, and A precedes B in
the program order, then A happens-before B
  - Writes of volatile variables happen-before subsequent reads of that
same variable (we can say "subsequent" because of the first rule above)
  - Releasing a lock happens-before subsequent acquisitions of that lock

There are a few other rules (having to do with starting/joining with
threads, finalizers, etc) but they rarely come into play.

On 4/12/2013 2:55 PM, 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
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>
_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

thurstonn
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.
ys
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

ys
Is "this.shared" a non-volatile long or double? If so, how would it not be racy? And if not, isn't there precedent to declare it a benign race (rather than not a race at all)?


On Sat, Apr 13, 2013 at 9:42 PM, thurstonn <[hidden email]> 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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Kirk Pepperdine
In reply to this post by thurstonn
To be honest, without any context it's hard to determine if any of the behaviours are racy or not. Brian's example looked very racy, this one looks worse... the original is obviously the worst of the bunch... the question is; what do you mean by racy and at some point you have to have some domain context to understand intend so you know what is or isn't allowed in that context. Any less and it's a discussion of semantics to which all I can say is that you're all right and you're all wrong at the same time.

-- Kirk

On 2013-04-14, at 2:42 AM, thurstonn <[hidden email]> 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
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Brian Goetz-3
In reply to this post by ys
The "long or double" part is irrelevant.  People get all torn up about
word-tearing -- as if it somehow was a case unto itself -- but even if
long/double reads/writes were guaranteed tear-free, it would *still* be
a data race if the variable is not volatile.  The word-tearing risk
simply expands the set of "bad things that can happen in a data race"
from "could read stale values" to "could read half-stale values."

On 4/13/2013 11:04 PM, ys wrote:

> Is "this.shared" a non-volatile long or double? If so, how would it not
> be racy? And if not, isn't there precedent to declare it a benign race
> (rather than not a race at all)?
>
>
> On Sat, Apr 13, 2013 at 9:42 PM, thurstonn <[hidden email]
> <mailto:[hidden email]>> 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
>     [hidden email]
>     <mailto:[hidden email]>
>     http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>
>
>
>
> _______________________________________________
> Concurrency-interest mailing list
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>
_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Gregg Wonderly-2
In reply to this post by Brian Goetz-3
Atomic views of the changes in values is a different issue than the
Happens-Before model creates/addresses.  Total program order is different from
thread order.  If you expect total program order to have a specific behavior,
and you use more than 1 thread, then you've created a situation that you need to
manage explicitly.

It's like a traffic light.  The light must be honored for safe traffic flow
guarantees.  But, if someone ignores the light, safe traffic flow is not
necessarily denied, but must be negotiated.

Happens before is like the case of no traffic lights.

Gregg Wonderly

On 4/13/2013 3:04 PM, Brian Goetz wrote:

> Consider this similar-looking programing:
>
> Object lock = new Object();
> int shared = 0;
>
> Thread 1: synchronized (lock) { local = shared; }
> Thread 2: synchronized (lock) ( shared = 10; }
> Thread 3: synchronized (lock) { local = shared; }
>
> Is what you're saying "in either my racy program or Brian's non-racy program,
> the effect will be the same -- threads 1 and 3 will each see either 0 or 10, and
> can't predict which because they do not control the timing of thread scheduling
> and lock acquisition", and from there, going to "so why do we call one racy and
> not the other?"
>
> In a properly synchronized program, you only see changes to shared variables at
> synchronization points, whereas in a racy program, they happen whenever, and the
> order in which they appear to happen may be different from the perspective of
> different threads.
>
> Or, maybe you just don't like the happens-before model because its different
> from what you're used to?  HB seems no less well-defined and tractable than the
> other models you seem to like.  The rules are simple:
>
>   - Synchronization actions (lock acquire/release, volatile read/write) are
> totally ordered
>   - If two actions A and B are in the same thread, and A precedes B in the
> program order, then A happens-before B
>   - Writes of volatile variables happen-before subsequent reads of that same
> variable (we can say "subsequent" because of the first rule above)
>   - Releasing a lock happens-before subsequent acquisitions of that lock
>
> There are a few other rules (having to do with starting/joining with threads,
> finalizers, etc) but they rarely come into play.
>
> On 4/12/2013 2:55 PM, 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
>> [hidden email]
>> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>>
> _______________________________________________
> Concurrency-interest mailing list
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>
>

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Vitaly Davidovich
In reply to this post by thurstonn

Yes this is racy; it may be benign but that depends on context.  If you have reader/writer of shared memory with no explicit synch or HB, it's a race by (informal) definition.

On Apr 13, 2013 9:51 PM, "thurstonn" <[hidden email]> 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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Mudit Verma
Another question,

Is data race a race even when it is OK to loose updates/writes and read older stuff while working on shared memory?


On Mon, Apr 15, 2013 at 3:41 PM, Vitaly Davidovich <[hidden email]> wrote:

Yes this is racy; it may be benign but that depends on context.  If you have reader/writer of shared memory with no explicit synch or HB, it's a race by (informal) definition.

On Apr 13, 2013 9:51 PM, "thurstonn" <[hidden email]> 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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest



_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Vitaly Davidovich

The short of it is that a data race is a data race - it describes shared memory access pattern.  Whether it yields correct execution is what determines if it's benign or not, and that's circumstantial.  The classic example is String.hashCode - it's (deliberately) data racy, but benign.

On Apr 15, 2013 9:46 AM, "Mudit Verma" <[hidden email]> wrote:
Another question,

Is data race a race even when it is OK to loose updates/writes and read older stuff while working on shared memory?


On Mon, Apr 15, 2013 at 3:41 PM, Vitaly Davidovich <[hidden email]> wrote:

Yes this is racy; it may be benign but that depends on context.  If you have reader/writer of shared memory with no explicit synch or HB, it's a race by (informal) definition.

On Apr 13, 2013 9:51 PM, "thurstonn" <[hidden email]> 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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest



_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

oleksandr otenko
In reply to this post by thurstonn
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.


Alex


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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

oleksandr otenko
In reply to this post by thurstonn
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


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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

thurstonn
In reply to this post by oleksandr otenko
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

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/>  ) 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
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

thurstonn
This post was updated on .
In reply to this post by oleksandr otenko
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 write and read (the read < write)

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
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

oleksandr otenko
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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
[hidden email]
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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

oleksandr otenko
In reply to this post by thurstonn

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
>> &lt;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
>> Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
>> _______________________________________________
>> Concurrency-interest mailing list
>> Concurrency-interest@.oswego
>> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest@.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-tp9408p9425.html
> Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
> _______________________________________________
> Concurrency-interest mailing list
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Gregg Wonderly-2
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
>>> &lt;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
>>>
>>> Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
>>> _______________________________________________
>>> Concurrency-interest mailing list
>>> Concurrency-interest@.oswego
>>> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>>
>> _______________________________________________
>> Concurrency-interest mailing list
>> Concurrency-interest@.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-tp9408p9425.html
>>
>> Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
>> _______________________________________________
>> Concurrency-interest mailing list
>> [hidden email]
>> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>
> _______________________________________________
> Concurrency-interest mailing list
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>
>

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: On A Formal Definition of 'Data-Race'

Vitaly Davidovich

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" <[hidden email]> 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
&lt;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

Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
_______________________________________________
Concurrency-interest mailing list
Concurrency-interest@.oswego
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
Concurrency-interest@.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-tp9408p9425.html

Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest



_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
1234