Hi, On March 10, 2017 at 1:49:01 PM, agsha ([email protected]) wrote: > In reference to java memory model specification > https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html > > I'm not talking about the complexity of the formalism there, which is > indeed quite complex. > > I'm talking more of the semantic mistakes that just seem like sloppy > technical writing: > > example 1: > In section 17.4.8 It says > "Given these sets of actions C0, ... and executions E1, ... , every action > in Ci must be one of the actions in Ei." > > So it would follow that actions in C0 must be in the actions of E0 > But E*0 *would is simply not defined. (E_1 is the first defined execution) > Of course, I understand what the authors are trying to say but the sentence > is technically incorrect. > > example 2: > In section 17.4.8 , the paragraph right after table 17.4.8-A It says > "Remember, however, that a program is correctly synchronized if, when it is > executed in a sequentially consistent manner, there are no data races" > This sentence implies that if *there exists* a sequentially consistent > execution without data races then it is correctly synchronized. > > But the correct definition of correctly synchronized as given in 17.4.5 is > "A program is correctly synchronized if and only if *all* sequentially > consistent executions are free of data races." > The two sentences are clearly not equivalent.
I'm with you on the first point but not on the second. I'd still read the second statement as "((the JVM executes the program in a sequentially consistent manner) implies (the program has no data races)) implies (program is correctly synchronized)". Since it is up to the JVM to decide which sequentially consistent execution exactly, the onus on the program is to be race free on every one of them. > Am I just not reading the sentences right? or is there really a problem? > The formalism of JMM is complex enough without us having to deal with > ambiguities of this sort. I'm not sure if this is the right forum for this digression, but one of the recent developments in this area is a paper from POPL 2017: "Kang, J., Hur, C. K., Lahav, O., Vafeiadis, V., & Dreyer, D. A promising semantics for relaxed-memory concurrency". They present a memory model for Java / C++ like languages, and fully formalize it in Coq. If the next iteration of the JMM adopts the above model then we won't have to worry about this kind of ambiguity. -- Sanjoy -- You received this message because you are subscribed to the Google Groups "mechanical-sympathy" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
