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

Ruslan Cheremin cheremin at gmail.com
Fri Apr 12 15:12:29 EDT 2013


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
> 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/20130412/67ffa828/attachment.html>


More information about the Concurrency-interest mailing list