What's "sequentially consistent executions are free of data races"?

Question

In JLS, §17.4.5. Happens-before Order, it says that

A program is correctly synchronized if and only if all sequentially consistent executions are free of data races.

It only give us definition about "sequentially consistent", it does not give us definition about "sequentially consistent executions". Only after knowing about what is "sequentially consistent executions", we may make further discussion about the topic.

So what's "sequentially consistent executions" and what's "sequentially consistent executions are free of data races"?

Answer 1

An execution has a very simple formal definition: it is simply a total ordering on the set of all memory actions that is under consideration.

A sequentially consistent execution is represented by any total ordering on actions which is sequentially consistent.

The term "free of data races" is also precisely defined by the JLS.

Note that the JLS does not require sequential consistency. In fact, the whole formalism of happens-before exists in order to define precisely the terms under which sequentially inconsistent executions can maintain an illusion of sequential consistency.

Answer 2

sequentially consistent executions means basically that each read operation on a variable sees the last write operation on that variable, no matter on which thread or processor the read/write operations are performed.

However, the JLS does not guarantee sequential consistency out of the box. Programmers have to achieve this consistency by proper synchronisation. Without synchronisation, threads may see inappropriate data, e.g. data that is being modified by another thread at the same time. This is called "data race".

Answer 3

To ensure that two actions are free of a data race, you must establish a happens-before relationship between the two actions using any of the five conditions specified in §17.4.5 and recapitulated in Memory Consistency Properties. Once you do that, your program is correctly synchronized with respect to those two actions. All executions of that program will appear to be sequentially consistent, and you can safely ignore any re-ordering permitted in §17.4.3. Programs and Program Order.