Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to understand JSR-133 Happens-Before is too Weak Figure6/7

In the JSR-133, there are two example that state presumably correctly synchronized programs.

The first example is given by figure 6 where:

x == y == 0

Then, thread 1 modifies the state by:

r1 = x; 
if (r1 != 0) 
y = 1; 

and thread 2 modifies the state by:

r2 = y;
if (r2 != 0)
x = 1;

The author states that this program is correctly synchronized,However, there is an execution of this program that results in r1 == r2 == 1. How would this latter value even be possible?

Furthermore, figure 7 states as an initial state:

x == y == 0

With thread 1 modifying:

r1 = x; 
y = r1; 

and thread 2 executing:

r2 = y;
x = r2;

How could this result in r1 == r2 == 42?

like image 835
Hanter Avatar asked Dec 01 '15 06:12

Hanter


1 Answers

Figure 6 is an example for the JMM's out of thing air restriction. Because no field is marked as volatile, the JVM is normally allowed to apply optimizations to the example code. This might result in surpising outcomes.

Assume that thread 1 observed x = 1 to be true. Do not worry for now, how this could be the case. In this case, it the thread would set y = 1. The latter observation would then justify the initial observation of x = 1 what is however cyclic reasoning. If this was true, x = y = 1 would be a legal outcome and the JVM could simply replace the code in both threads to write each value. This form of reasoning is forbidden by the JMM such that x = y = 0 is the only legal result according to the JMM.

A similar argument is made in figure 7. Again, assume the observation x = 42 by thread 1. In this case, the thread would write y = 42. Based on this observation, one can now argue that the previous x = 42 is a legal observation. The initial assumption was however made out of thin air what is forbidden such that x = y = 0 is the only legal outcome.

The definition of a happens-before relationship only applies to explicitly synchronized programs and would not forbid the hypothetical cyclic reasoning. Therefore, the out of thin air restriction is needed. This is of course rather academic but with the JMM being an academic model, it is still necessary to define this limitation.

Because of this, there are no racing conditions in either figure for which value x or y can take, i.e. there is no racing condition and x = y = 0 is the only possible observation. It follows that both examples are correctly synchronized despite the absense of volatile.

like image 78
Rafael Winterhalter Avatar answered Oct 23 '22 05:10

Rafael Winterhalter