Java: proving that DCL is not working

I wonder whether it’s possible reliably to prove that double checked locking is broken:

public static Singleton getInstanceDC() {
  if (_instance == null) {                // Single Checked
    synchronized (Singleton.class) {
      if (_instance == null) {        // Double checked
        _instance = new Singleton();
      }
    }
 }
 return _instance;
}

Is there any reliable way to create a test or program which shows that it doesn’t work? Is there any formal verification proof?

Answer

I’ve found what I was looking for: there is java tool called jcstress, it’s used to verify correctness of JVM.

More precisely sourcecode of DCL test case could be found here: http://hg.openjdk.java.net/code-tools/jcstress/file/9270b927e00f/tests-custom/src/main/java/org/openjdk/jcstress/tests/singletons/UnsafeDCL.java#l71

I would say this is proof-by-the-spec 🙂