A false negative in DEADLOCK detection

[Zustin]

Hi, I found a bug in Infer's deadlock detector. Consider the following code example: methods foo1 (line 8) and foo2 (line 20) attempt to acquire locks la and lb in reverse order, which causes the program to hang during execution. Infer should have reported a DEADLOCK warning for this case, but no warning was actually generated. So, this is a false negative bug. It appears that Infer incorrectly assumes the concurrency bug is resolved by using AtomicReference.

import java.util.concurrent.atomic.AtomicReference;

public class DeadlockExample {
    
    private final AtomicReference<Object> lockA = new AtomicReference<>(new String("A"));
    private final AtomicReference<Object> lockB = new AtomicReference<>(new String("B"));

    private void foo1() {
        Object la = lockA.get(), lb = lockB.get();
        synchronized (la) {
            try {
                Thread.sleep(100);
            } catch (InterruptedException e) {
                e.printStackTrace();
            }
            synchronized (lb) {}
        }
    }

    private void foo2() {
        Object la = lockA.get(), lb = lockB.get();
        synchronized (lb) {
            try {
                Thread.sleep(100);
            } catch (InterruptedException e) {
                e.printStackTrace();
            }
            synchronized (la) {}
        }
    }

    public static void main(String[] args) {
        DeadlockExample demo = new DeadlockExample();
        Thread thread1 = new Thread(() -> {
            demo.oneWay();
        }, "thread-1");
        Thread thread2 = new Thread(() -> {
            demo.anotherWay();
        }, "thread-2");
        
        thread1.start();
        thread2.start();
        
        try {
            thread1.join();
            thread2.join();
        } catch (InterruptedException e) {
            e.printStackTrace();
        }
    }
}

Infer Log

infer run -- javac DeadlockExample.java
Capturing in javac mode...
Found 1 source file to analyze in infer-out
 0/15 [..............................................................................] 0% 41.2ms
⊢ [ 0.0s][17.8M] DeadlockExample.java: void DeadlockExample.foo2()
⊢ [ 0.0s][17.8M] DeadlockExample.java: void DeadlockExample.foo1()
⊢ [ 0.0s][17.8M] idle
⊢ [ 0.0s][17.8M] idle
⊢ [ 0.0s][17.8M] idle
⊢ [ 0.0s][17.8M] idle
⊢ [ 0.0s][17.8M] DeadlockExample.java: DeadlockExample.<init>()
⊢ [ 0.0s][17.8M] DeadlockExample.java: DeadlockExample$Lambda$_6_29.<init>(DeadlockExample)
 0/15 [..............................................................................] 0% 131ms
⊢ [ 0.1s][20.4M] DeadlockExample.java: void DeadlockExample.foo2()
⊢ [ 0.1s][20.4M] DeadlockExample.java: void DeadlockExample.foo1()
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][20.4M] DeadlockExample.java: DeadlockExample.<init>()
⊢ [ 0.1s][17.8M] DeadlockExample.java: DeadlockExample$Lambda$_6_29.<init>(DeadlockExample)
 0/15 [..............................................................................] 0% 176ms
⊢ [ 0.1s][20.4M] DeadlockExample.java: void DeadlockExample.foo2()
⊢ [ 0.1s][20.4M] DeadlockExample.java: void DeadlockExample.foo1()
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][20.4M] DeadlockExample.java: DeadlockExample.<init>()
⊢ [ 0.1s][17.8M] DeadlockExample.java: DeadlockExample$Lambda$_6_29.<init>(DeadlockExample)
 8/15 [#########################################.....................................] 53% 228ms
⊢ [ 0.1s][20.4M] idle
⊢ [ 0.1s][20.4M] idle
⊢ [ 0.0s][17.8M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][17.8M] DeadlockExample.java: void DeadlockExample.access_DeadlockExample$Lambda$_6_29(DeadlockExample)
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][20.4M] DeadlockExample.java: void DeadlockExample.main(String[])
⊢ [ 0.1s][17.8M] idle
13/15 [###################################################################...........] 86% 278ms
⊢ [ 0.0s][20.4M] idle
⊢ [ 0.0s][20.4M] idle
⊢ [ 0.0s][17.8M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.0s][17.8M] idle
⊢ [ 0.0s][17.8M] void DeadlockExample$Lambda$_6_13.run()
⊢ [ 0.0s][20.4M] idle
⊢ [ 0.1s][17.8M] idle
15/15 [##############################################################################] 100% 285ms
⊢ [ 0.0s][20.4M] idle
⊢ [ 0.1s][20.4M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.0s][17.8M] idle
⊢ [ 0.1s][20.4M] idle
⊢ [ 0.1s][17.8M] idle
⊢ [ 0.2s][17.8M] idle

  No issues found  

[ngorogiannis]

If I remember correctly, the check will only report on non-private methods.

[Zustin]

Hi @ngorogiannis , after changing all private modifiers to public, Infer still does not report this warning. See the following code example for reference.

import java.util.concurrent.atomic.AtomicReference;

public class DeadlockExample {
    
    public final AtomicReference<Object> lockA = new AtomicReference<>(new String("A"));
    public final AtomicReference<Object> lockB = new AtomicReference<>(new String("B"));

    public void foo1() {
        Object la = lockA.get(), lb = lockB.get();
        synchronized (la) {
            try {
                Thread.sleep(100);
            } catch (InterruptedException e) {
                e.printStackTrace();
            }
            synchronized (lb) {}
        }
    }

    public void foo2() {
        Object la = lockA.get(), lb = lockB.get();
        synchronized (lb) {
            try {
                Thread.sleep(100);
            } catch (InterruptedException e) {
                e.printStackTrace();
            }
            synchronized (la) {}
        }
    }

    public static void main(String[] args) {
        DeadlockExample demo = new DeadlockExample();
        Thread thread1 = new Thread(() -> {
            demo.foo1();
        }, "thread-1");
        Thread thread2 = new Thread(() -> {
            demo.foo2();
        }, "thread-2");
        
        thread1.start();
        thread2.start();
        
        try {
            thread1.join();
            thread2.join();
        } catch (InterruptedException e) {
            e.printStackTrace();
        }
    }
}