Oleg Zabluda's blog
Friday, April 27, 2012
 
In C/C++ data races are undefined behavior.
In C/C++ data races are undefined behavior. Java has a problem: there is no such thing as undefined behavior due to security requirements, so it has to give meaning to them, while not suffering too much of a performance hit ("Java is faster then C/C++", remember?) i.e. allowing allowed reodering, which is the whole point.

Java "solution" is in

Java Language Specification 3d Ed, (SE 7) chapter
17.4.8. Executions and Causality Requirements
http://docs.oracle.com/javase/specs/jls/se7/html/jls-17.html#jls-17.4.8
is a formidable-looking formal specification with fancy set-theoretic math.

Manson, Pugh, Adve: "The Java Memory Model", POPL 05 chapter 9.1.2 "Semantics Allow Reordering" "proves" in Theorem 1 that non-conflicting operations may be reordered by a compiler or runtime.

But in Aspinall, Sevcik, “Java Memory Model Examples: Good, Bad, and Ugly”, VAMP 2007, chapter 5 "Ugly executions", subchapter 1. "Reordering of independent statements"
http://groups.inf.ed.ac.uk/request/jmmexamples.pdf

we read "The first example (from [2]) demonstrates that it is not the case that any independent statements can be reordered in the JMM2 without changing the program’s behaviour [...] This falsifies Theorem 1 of [6].

Oops. As of now, this problem in Java spec is unresolved.

This story is retold from Hans Boehm "Programming Language Memory Models: What do Shared Variables Mean?", ECOOP 2011 Summer School talk.
http://www.hpl.hp.com/personal/Hans_Boehm/misc_slides/boehm-ucb10-no-quotes.pdf

Also see
https://plus.google.com/112065430692128821190/posts/KiPn95fTcoa
http://www.hpl.hp.com/personal/Hans_Boehm/misc_slides/boehm-ucb10-no-quotes.pdf

Labels:


- posted by Oleg Zabluda @ 5:01 PM | permalink | | | technorati | bloglines | feedster
| |

Home

Powered by Blogger