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 🙂