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. 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. -- 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.
