Java: Fix FP in DoubleCheckedLocking.ql

java/ql/src/Likely Bugs/Concurrency/DoubleCheckedLocking.ql

@@ -15,9 +15,21 @@
 import java
 import DoubleCheckedLocking
 
+predicate allFieldsFinal(Class c) { forex(Field f | c.inherits(f) | f.isFinal()) }
+
 from IfStmt if1, IfStmt if2, SynchronizedStmt sync, Field f
 where
   doubleCheckedLocking(if1, if2, sync, f) and
-  not f.isVolatile()
+  not f.isVolatile() and
+  not (
+    // Non-volatile double-checked locking is ok when the object is immutable and
+    // there is only a single non-synchronized field read.
+    allFieldsFinal(f.getType()) and
+    1 = strictcount(FieldAccess fa |
+        fa.getField() = f and
+        fa.getEnclosingCallable() = sync.getEnclosingCallable() and
+        not fa.getEnclosingStmt().getParent*() = sync.getBlock()
+      )
+  )
 select sync, "Double-checked locking on the non-volatile field $@ is not thread-safe.", f,
   f.toString()

java/ql/src/Likely Bugs/Concurrency/DoubleCheckedLockingBad3.java

@@ -0,0 +1,13 @@
+private Object lock = new Object();
+private MyImmutableObject f = null;
+
+public MyImmutableObject getMyImmutableObject() {
+  if (f == null) {
+    synchronized(lock) {
+      if (f == null) {
+        f = new MyImmutableObject();
+      }
+    }
+  }
+  return f; // BAD
+}

java/ql/src/Likely Bugs/Concurrency/DoubleCheckedLockingShared.qhelp

@@ -66,6 +66,26 @@ variable can be used to avoid reading the field more times than neccessary.
 </p>
 <sample src="DoubleCheckedLockingGood.java"/>
 
+<p>
+As a final note, it is possible to use double-checked locking correctly without
+<code>volatile</code> if the constructed object is immutable in the sense that
+all its fields are declared <code>final</code> and the double-checked field is
+read exactly once outside the synchronized block.
+</p>
+<p>
+Given that all fields in <code>MyImmutableObject</code> are declared
+<code>final</code> then the following example is protected against exposing
+uninitialized fields to another thread. However, since there are two reads of
+<code>f</code> without synchronization, it is possible that these are
+reordered, which means that this method can return <code>null</code>.
+</p>
+<sample src="DoubleCheckedLockingBad3.java"/>
+<p>
+In this case, using a local variable to minimize the number of field reads is
+no longer a performance improvement, but rather a crucial detail that is
+necessary for correctness.
+</p>
+
 </example>
 
 <references>
@@ -80,6 +100,12 @@ Java Language Specification:
 <li>
 Wikipedia: <a href="https://en.wikipedia.org/wiki/Double-checked_locking">Double-checked locking</a>.
 </li>
+<li>
+<a href="https://shipilev.net/blog/2014/safe-public-construction/">Safe Publication and Safe Initialization in Java</a>.
+</li>
+<li>
+<a href="https://shipilev.net/blog/2016/close-encounters-of-jmm-kind/">Close Encounters of The Java Memory Model Kind</a>.
+</li>
 
 </references>