Java Memory Model

Java Memory Model

Purpose

Prove which values an execution is permitted to observe. The JMM constrains compiler, runtime and hardware transformations through actions and consistency rules; it is not merely a cache-coherence or processor-reordering explanation.

The central review question is not “will the other thread probably see it?” It is: which rule orders each conflicting access, which atomic invariant is represented, and what outcomes remain legal if the program has a data race?

Ownership boundary

• This skill owns the JLS memory-model proof and safe-publication contract.
• varhandles-and-memory-ordering owns explicit access modes and fences.
• java-thread-safety-contracts owns class-level guarantees and lock policy.
• lock-free-patterns owns algorithms, progress, ABA and reclamation.
• concurrency-testing owns jcstress/model/stress test construction.
• cpu-cache-and-numa owns cache/coherence/locality cost, not language correctness.

Proof contract

The specification reference is Java SE 25; distinguish it from the project's compiler release, runtime and concurrency-library versions. Inspect those, relevant JVM flags and all participating access paths before applying a release-sensitive API rule. Do not upgrade or enable preview. If a write path or handoff contract is unavailable, report an incomplete proof and name the missing edge evidence; do not substitute a successful run for it. Java snippets below are partial patterns with omitted types/enclosing declarations, not standalone executable tests.

shared locations and conflicting reads/writes:
threads/tasks and action lifecycle:
state invariant and required atomic transition/snapshot:
program-order actions per thread:
synchronization actions and synchronizes-with edges:
happens-before graph and read-allowed writes:
final-field construction/freeze and reachability:
publication and post-publication mutation:
cancellation/interruption/shutdown edges:
legal, interesting, forbidden and unacceptable outcomes:

If the claim depends on elapsed time, “eventually,” x86 behavior, debug logging, a safepoint, or a test never failing, it is not yet a JMM proof.

Core model

• Two accesses conflict when they target the same variable, at least one is a write, and they are not both reads. A data race exists when conflicting accesses are not ordered by happens-before.
• Program order orders actions within a thread according to that thread's inter-thread semantics; it is not a global wall-clock order.
• Synchronization actions participate in a synchronization order. Specific pairs create synchronizes-with edges; happens-before is program order plus synchronizes-with plus transitivity.
• A correctly synchronized program—sequentially consistent executions have no data races—has the sequential-consistency guarantee described by JLS 17.4.5.
• A racy execution is still constrained by the JMM, but ordinary sequential reasoning is not a valid proof. “It works on this CPU” does not narrow the language-permitted executions.

Happens-before is stronger than “earlier in time” and subtler than “read B sees the last write A.” A read is allowed to observe a write only under the JLS rules; intervening/unordered writes and races matter. Draw actual actions rather than using “visibility” as a magic word.

Synchronization and derived happens-before edges used in reviews

Monitor/volatile pairs are primitive synchronizes-with edges; lifecycle/API rows summarize derived guarantees. Expand them into actual actions before treating them as a proof graph.

Default initialization also has a happens-before rule. Final-field semantics are special freeze/ dereference rules and should not be mislabeled as a generic publication happens-before edge. Timed join can return before termination, and isAlive() == false on an unstarted thread does not detect completed work. Confirm the actual lifecycle before using termination ordering.

Volatile publication

For immutable or safely isolated data built before publication, with exactly one publisher and one publication per holder instance (ready initially false, never reset):

private Config config;
private volatile boolean ready;

void publish(Config next) {
    config = next;      // ordinary writes before anchor
    ready = true;       // volatile write
}

Config current() {
    if (!ready) throw new IllegalStateException(); // volatile read first
    return config;                                  // ordinary read after anchor
}

The proof uses program order, volatile synchronizes-with, and transitivity. Every reader must read the anchor before dependent state, and every publishing path must perform the ordered anchor write. Post-publication mutation needs its own synchronization. This flag is not a reusable version protocol: a reader can observe an earlier true while a later publisher overwrites ordinary config. For replacement updates publish the immutable configuration through one volatile reference and read it once, as in the publication reference.

volatile makes each access to that variable atomic and ordered as specified; it does not make a compound read-modify-write (x++) atomic, nor a multi-field invariant a snapshot. Multi-field state can use one lock, an immutable aggregate published through one volatile/atomic reference, or another formally proven protocol.

Final-field semantics

At normal constructor completion, writes to final fields are frozen. If the object reference is later observed through a permitted execution and this did not escape during construction, special final-field rules provide stronger guarantees for the final values and referenced object/array state reachable through those finals as defined by JLS 17.5.

This is not “safe publication for free”:

• the reader can still fail to obtain the reference correctly or observe stale non-final fields;
• mutation after the freeze is not covered;
• constructor escape can break the guarantee;
• reflection, deserialization and special mutation mechanisms have additional rules;
• final fields do not make referenced mutable objects immutable or operations thread-safe.

Prefer proper safe publication even for immutable objects: class initialization, volatile/atomic reference, monitor/lock handoff, thread start, or a concurrent collection/queue with documented memory effects.

Constructor escape and lifecycle

Escape includes exposing this through listener registration, submitted/started work, static/shared state or callbacks. Merely creating a lambda that captures this is not escape until that callback is exposed; constructor-time callbacks can still observe partial state without another thread. Subclass fields may not be initialized when base-constructor escape invokes overridden behavior. Construct privately, then publish from a factory or owner after completion.

Thread pools complicate start() intuition: submitting a task does not start a new worker per task. Rely on the executor/queue/Future API's documented memory-consistency effects, not the historical creation of the worker thread.

Wait, notification and conditions

wait() atomically releases and later reacquires the monitor, but wakeups can be spurious and the condition can be consumed by another thread. Always wait in a predicate loop under the same lock:

synchronized (lock) {
    while (!condition()) lock.wait();
    consumeState();
}

Notification is not state; update the predicate under the lock. Define interruption, timeout, shutdown and notify versus notifyAll consequences. Prefer higher-level synchronizers/queues when their contract fits.

Architecture and code generation

JLS guarantees do not depend on x86, AArch64, RISC-V, interpreter, C1, C2 or Graal. Stronger hardware ordering can make some racy outcomes hard to observe, while compiler optimizations remain legal. Conversely, an architecture migration does not guarantee a race will reproduce.

Use assembly only to study implementation/cost after the language proof is complete. Do not encode specific instructions or “volatile reads are free” as portable correctness/performance rules.

Diagnosis and validation

1. Preserve the wrong business outcome and relevant inputs/version; thread dumps/JFR may show liveness/contention but usually not a data race.
2. Minimize the state/action pattern and enumerate outcomes.
3. Build a jcstress test with explicit acceptable/interesting/forbidden outcomes.
4. Use static analysis and code review for inconsistent locking, unsafe publication and compound operations, but verify tool rule limitations.
5. Fix the proof, then run stress/load tests across target JDKs/architectures for integration—not as proof that all executions are safe.

Anti-patterns

Definition of done

• Every conflicting access is ordered or all racy outcomes are explicitly acceptable.
• Compound invariants have one atomicity protocol, not per-field assumptions.
• Publication, mutation and lifecycle edges use exact JLS/API contracts.
• Final-field guarantees are separated from safe publication and immutability.
• Constructor escape, interruption, timeout and shutdown paths are covered.
• Legal/forbidden outcomes and jcstress/static/integration evidence are recorded.
• Correctness does not depend on processor/JIT timing folklore.

References

• Happens-before and publication proofs — read when proving publication, initialization or a compound operation.
• Concurrency review and incident checklist — read for incident evidence, outcome classification and test planning.
• JLS 17: Threads and Locks
• JLS 17.4: Memory Model
• JLS 17.5: Final Field Semantics
• OpenJDK jcstress