This section on the symmetry between volatile and synchronized is a jewel.
This symmetry allows constructing locks:
volatile boolean busyFlag;
while (!compareAndSet(lock.busyFlag, false, true)); // burn for the mutual exclusion Gods
a = x;
b = 1;
lock.busyFlag = false;
There’s an interesting similar line of work formalizing the C++11 memory model which includes a tool to explore possible behaviors (relative to the stress tester here it systematically explores possible behaviors based on a the model).
Here’s some links for those interested:
Online explorer (cppmem)