This section on the symmetry between volatile and synchronized is a jewel.

This symmetry allows constructing locks:

int x;
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:

Main Page

Online explorer (cppmem)