There are two conclusions from JLS:
- C1: If a program is free of data races, then all executions of the program will appear to be sequentially consistent:
data-race-free => sequentially consistent - C2: If a program is correctly synchronized, then all executions of the program will appear to be sequentially consistent:
correctly synchronized => sequentially consistent
If the converse of C1 is true, then we can conclude that:
- C3: If a program is correctly synchronized, then it is free of data races:
correctly synchronized => data-race-free
But unfortunately, there is no such statement in the JLS, so I get to the fourth conclusion:
- C4: A program can be correctly synchronized and have data races.
But I am not satisfied with this approach and want to get a proof that this conclusion is true (or false), even in an informal way or in sample way.
First of all, I think a code segment that shows a sequentially consistent execution of a multi-threaded program that contains a data race is helpful to understand and resolve this problem.
After serious consideration, I still can not find a proper sample. So would you please give me such a code segment?