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?


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:

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

Leave a Reply

Your email address will not be published. Required fields are marked *