The Java Memory Model promises that correctly synchronized programs behave as if sequentially consistent. What does the specification mean by a correctly synchronized program, and what is still guaranteed for a program that is not?

## Sequential consistency, in one line Sequential consistency (SC) is the intuitive model: all threads' operations appear in one global total order, each thread's operations appear in program order within it, and every read returns the most recent write in that order. It is how everyone naturally reasons - and it is *not* what hardware or compilers actually provide, because enforcing it everywhere would forbid registers, reordering and store buffers. ## The bargain the specification strikes Rather than give SC to everyone (too slow) or to no one (unusable), the JMM offers a conditional guarantee, usually written SC-DRF: **if your program is data-race-free, all of its executions are sequentially consistent.** You get the easy model precisely when you have paid for it with synchronization. ### What a data race is, exactly Two accesses **conflict** if they touch the same variable and at least one is a write. A **data race** is a pair of conflicting accesses not ordered by happens-before. Two points people miss: - Two reads never conflict, so read-only sharing is race-free by definition. This is the formal reason immutable data needs no synchronization. - "Ordered by happens-before" is what synchronization buys. Unlocking a monitor happens-before a later lock of the same monitor; a volatile write happens-before a subsequent read of that same field; a thread's start and join, and the freeze of final fields at the end of a constructor, contribute edges too. Any of those, applied to the right accesses, removes the race. ### The definition's circularity, resolved The subtle part: correctly synchronized is defined as "no data race in any **sequentially consistent** execution", not "in any execution". Without that restriction the definition would be circular - you would need to know the legal executions to know whether the program is race-free, and you need race-freedom to know the executions are SC. Anchoring the test in SC executions makes it usable: you may analyze your program with the simple interleaving model, and if no interleaving exposes an unsynchronized conflicting pair, the model promises the simple interleaving model was the right one all along. ## Data race is not the same as race condition A *data race* is the formal, model-level property above. A *race condition* is a design bug where the outcome depends on timing. They are independent. `if (!map.containsKey(k)) map.put(k, v)` on a concurrent map has no data race - every access is properly synchronized inside the map - but it is a race condition, because two threads can both pass the check. Conversely a program can have a data race on a status flag whose only visible effect is a delayed shutdown. Passing a race detector is not proof of correctness. ## What racy programs still get The JMM does not declare racy programs undefined. Its causality rules exist to forbid **out-of-thin-air** values: a read may only return a value that some write in the execution actually wrote. Consequences: - A racy read of a reference cannot forge a pointer, so memory safety and type safety hold even in badly written concurrent code. This is a security requirement - untrusted bytecode must not break the sandbox by racing. - What you *do* lose is real: stale values that never refresh, partially constructed objects visible to other threads, and threads that disagree about ordering, so no single global order explains what they observed. - 64-bit non-volatile `long` and `double` accesses are additionally permitted to be split into two 32-bit halves, so a racy read of one may see a value no thread ever wrote as a whole. ## How to use this in practice SC-DRF is the reason the practical rule "synchronize every access to shared mutable state, then reason sequentially" is sound rather than folklore. It also tells you what you are signing up for when you deliberately race - lock-free code, benign-looking status flags, racy caches - namely that you must argue correctness under the weak model itself, because the easy model is no longer on offer.