Checker GuardedBy   as of Julia version 2.6.0 (built on 6 Sep 2018)

belongs to group Advanced

Check and infer @GuardedBy and @Holding annotations


Java uses synchronized statements and methods to guarantee that data is accessed in a sequential way and avoid race conditions in multithreaded applications. In C#, this is achieved with the lock statements, or by surrounding a block between calls to Monitor.Enter(obj) and Monitor.Exit(obj). Incorrect uses of synchronization result in unexpected behaviors and subtle bugs, very hard to identify and reproduce. This checker helps the programmer by identifying or checking the locks that are held when a field is accessed or a method is called. This information can be inferred, and reported in a jaif file, or verified, if the programmer provides source code annotations on the locks that must be held for specific fields and methods. Moreover, this checker signals situations where a synchronization seems missing on a field.

Action: Verify if the missing synchronization should actually be there. Annotate fields and methods with the lock that must be held when they are accessed or called, by using the @GuardedBy and @Holding annotations. If this checker does not accept those annotations, it is likely the case that your program has a synchronization problem.

The @GuardedBy annotation for fields and parameters and the @Holding annotation for methods and constructors accepts a string argument, according to the following syntax

  • @GuardedBy/@Holding("this"): the lock on the receiver of a non-static field or method must be held
  • @GuardedBy("itself"): the lock on the same parameter or field must be held
  • @GuardedBy/@Holding("field-name"): the lock on the named field of the receiver of a non-static field or method must be held
  • @GuardedBy/@Holding("Class.field-name"): the lock on the named static field of the named class must be held
  • @GuardedBy/@Holding("Class.class"): the lock of the unique class object representing the class named Class must be held
  • @GuardedBy/@Holding("foo()"): the lock on the return value of the named instance method called on the receiver of a non-static field or method must be held. Method foo must return a reference type
  • @GuardedBy/@Holding("Class.foo()"): the lock on the return value of the named static method of the named class must be held. Method foo must return a reference type.


Examples



Identifying missing synchronizations

Programmers often forget about the consistent use of synchronization statements, which results in fields being accessed without the required lock being held. This checker identifies such situations, even without any explicit annotation by the programmer. An example is the following:

import java.util.HashSet;
import java.util.Set;

public class UserRegistry {
  private final Set<String> users = new HashSet<String>();

  public void register(String user) {
    synchronized (users) {
      users.add(user);
    }
  }

  public void unregister(String user) {
    synchronized (users) {
      users.remove(user);
    }
  }

  public boolean isRegistered(String user) {
    return users.contains(user);
  }

  public int countUsers() {
    synchronized (users) {
      return users.size();
    }
  }
}

This checker issues in this case the following warning:

UserRegistry.java:20: [GuardedBy: MissingSynchronizedWarning] "users" is usually locked when you access field "users". Did you miss a synchronized statement here?

In this case, the programmer should add a synchronization on the access to field users inside method contains() as well. We recall that hashsets are not synchronized in Java and concurrent access to the same hashset might result in inconsistent behaviors or even deadlock. Another solution, here, would be to use a synchronized or concurrent set, by exploiting the classes already available in the standard Java library. In that case, no synchronized statement would be needed anymore.

We observe that an automatic static analyzer cannot decide if, in some special situation, a missing synchronization does not affect correctness. Julia can only use in this case a statistical approach: if most accesses are synchronized, then all accesses are likely to be synchronized.


Inferring @GuardedBy/@Holding annotations

Consider the following class:

import lock.quals.GuardedBy;
import lock.quals.Holding;

public class GuardedByTest {
  private int counter;
  private Object lock = new Object();
  private long counter2;
  private static int counter3;
  private static Object lock4 = new Object();
  private static int counter4 = 13;
  private final Object[] locks = new Object[10];
  private int next;
  private final Object lock5 = new Object();
  private final static Object lock6 = new Object();
  private int counter5;

  public GuardedByTest() {
    this.counter = 1;
    this.counter5 = 17;
    this.counter5 += counter;
  }

  public synchronized void incrementCounter() {
    counter++;
  }

  public void decrementCounter() {
    synchronized (this) {
      counter--;
    }
  }

  public boolean checkCounterIs0() {
    Object copy = this;
    synchronized (copy) {
      return counter == 0;
    }
  }

  public void incrementOtherCounter(GuardedByTest other) {
    GuardedByTest copy = other;
    synchronized (copy) {
      incrementCounterAux(other);
    }
  }

  private void incrementCounterAux(@GuardedBy("this") GuardedByTest other) {
    other.counter += 2;
  }

  public void incrementCounter2() {
    synchronized (lock) {
      counter2++;
    }
  }

  public void decrementCounter2() {
    synchronized (lock) {
      counter2--;
    }
  }

  public boolean checkCounter2Is0() {
    Object copy = lock;
    synchronized (copy) {
	  return counter2 == 0;
    }
  }

  public void incrementOtherCounter2(GuardedByTest other) {
    GuardedByTest copy = other;
    synchronized (copy.lock) {
      incrementCounter2Aux(other);
    }
  }

  private static void incrementCounter2Aux(GuardedByTest other) {
    other.counter2 += 2;
  }

  public void incrementCounter3() {
    synchronized (GuardedByTest.class) {
      counter3++;
    }
  }

  @Holding("GuardedByTest.class")
  public static synchronized void decrementCounter3() {
    counter3--;
  }

  public void incrementCounter4() {
    synchronized (lock4) {
      counter4++;
    }
  }

  public static void decrementCounter4() {
    synchronized (lock4) {
      decrementCounter4Aux();
    }
  }

  @Holding("GuardedByTest.lock4")
  private static void decrementCounter4Aux() {
    counter4--;
  }

  private Object getLock() {
    return locks[next % locks.length];
  }

  public void incrementCounter5() {
    synchronized (getLock()) {
      counter5++;
      next++;
    }
  }

  public void decrementCounter5() {
    synchronized (getLock()) {
      decrementCounter5Aux();
    }
  }

  private void decrementCounter5Aux() {
    counter5--;
  }

  public void accessLock5() {
    synchronized (lock5) {
      lock5.hashCode();
    }
  }

  public static void accessLock6() {
    synchronized (lock6) {
      lock6.hashCode();
    }
  }

  public synchronized void parameterTest1(Object o1, String o2, String o3) {
    System.out.println(o1);
    synchronized (lock) {
      System.out.println(o2);
    }
    synchronized (o3) {
      System.out.println(o3 + " ");
    }
  }
}

This checker, with the jaif option and in library mode, generates the following jaif file:

package lock.quals:

annotation @GuardedBy:
    String value
annotation @Holding:
    String value

package java.lang:

annotation @SuppressWarnings:
    String[] value


class GuardedByTest:
    field counter:
      type: @GuardedBy("this")
    field counter2:
      type: @GuardedBy("lock")
    field counter3:
      type: @GuardedBy("GuardedByTest.class")
    field counter4:
      type: @GuardedBy("GuardedByTest.lock4")
    field counter5:
      type: @GuardedBy("getLock()")
    field lock5:
      type: @GuardedBy("itself")
    field lock6:
      type: @GuardedBy("itself")
    method decrementCounter()V:
      receiver: @GuardedBy("itself")
    method decrementCounter3()V:
    method decrementCounter4Aux()V: @Holding("GuardedByTest.lock4")
    method decrementCounter5Aux()V: @Holding("getLock()")
      receiver: @GuardedBy("getLock()")
    method incrementCounter()V:
      receiver: @GuardedBy("itself")
    method incrementCounterAux(LGuardedByTest;)V:
      parameter #0:
        type: @GuardedBy("itself")
    method parameterTest1(Ljava.lang.Object;Ljava.lang.String;Ljava.lang.String;)V:
      receiver: @GuardedBy("itself")
      parameter #0:
        type: @GuardedBy("this")
      parameter #1:
        type: @GuardedBy("lock") @GuardedBy("this")
      parameter #2:
        type: @GuardedBy("itself") @GuardedBy("this")

These are @GuardedBy and @Holding annotations automatically inferred from the code. Let us look at them closely.

  • Field counter is inferred to be accessed only when its receiver is locked. Note that this does not include the accesses in the constructor, as long as its receiver has not escaped before accessing counter. Note that Julia considers definite aliasing in method checkCounterIs0, since by locking copy one actually locks this as well. Moreover, note that the receiver of counter must be locked, which is not always a synonym for the this object of the method. For instance, consider method incrementCounterAux, where other is checked to be locked, not the this variable of the method.
  • Field counter2 is inferred to be accessed only when the lock field of its receiver is locked. Similar considerations as above for counter apply.
  • Field counter3 is inferred to be accessed only when GuardedByTest.class (a java.lang.Class object) is locked. Note that this happens by an explicit synchronization on that object (as in method incrementCounter3) or through an implicit synchronization at call-time (as in the static method decrementCounter3).
  • Field counter4 is static and is inferred to be accessed only when the static field GuardedByTest.lock4 is held. Note that a static field can only be guarded by another static field or a class tag or a static method call.
  • Field counter5 is locked by the return value of a call to method getLock on the same receiver of the field. Julia checks that that method is deterministic (that is, it yields the same value when run from the same initial context) and that its execution does not modify the context that it reads. Note that the assignment at line 116 modifies the return value of getLock, which is fine as long as the assignment comes after any access to counter5. If the programmer swaps lines 115 and 116, field counter5 is not inferred to be guarded anymore.
  • Fields lock5 and lock6 are always accessed after getting a lock to themselves. Hence they are guarded by itself, which can be seen here as a shorthand for a field notation.
  • Methods decrementCounter4Aux and decrementCounter5Aux are also inferred to be guarded by some locks. That is, those locks are held when the methods are called. It is interesting to observe that decrementCounter5Aux is guarded because it is private, and hence there cannot be any other call to that method beyond that at line 122. If the method is made public, Julia does not infer it as guarded anymore. Note that guard annotations for methods are reported as @Holding.
  • The parameter other of method incrementCounterAux() is always locked when it is accessed. Hence the analyzer has inferred the @GuardedBy("itself") annotation for it and reports that annotation in the jaif file. Note that this is different from what the programmer seemed to expect (line 47). Hence the analyzer issues the following warning:
    GuardedByTest.java:47: [GuardedBy: UnguardedParameterWarning] is "this" locked when accessing the formal parameter "other"?

Checking user-provided @GuardedBy/@Holding annotations

As we have seen in the last paragraph, this checker can be used both to infer a jaif file, reporting the synchronization information inferred by Julia, and to check that some user-provided @GuardedBy or @Holding annotation is actually valid. For instance, this checker reports also the following warning for our example:

GuardedByTest.java:88: [GuardedBy: UnguardedMethodOrConstructorWarning] decrementCounter3 is public hence there is no guarantee that "GuardedByTest.class" is locked at its call

since a public method might be called from still unknown contexts, where GuardedByTest.class might not yet be locked. This also clarifies that the @Holding("GuardedByTest.class") annotation refers to the calling context, not to the beginning of the method. In other terms, it states that that lock must be held whenever the method is called and the fact that the static method decrementCounter3 is synchronized becomes irrelevant here.

For a further example of checking annotations, assume that the programmer decorates field counter as follows:

  @GuardedBy("this")
  private int counter;

By running this checker again, no new warning is issued, stating that the synchronization of field counter on its receiver has been validated. But the programmer might instead go wrong and annotate the field as:

  @GuardedBy("lock")
  private int counter;

In this case, this checker issues the following warnings, that express the fact that the accesses to field counter do not respect the expected synchronization policy:

GuardedByTest.java:24: [GuardedBy: UnguardedFieldAccessWarning] is "lock" locked when accessing field "counter" here?
GuardedByTest.java:29: [GuardedBy: UnguardedFieldAccessWarning] is "lock" locked when accessing field "counter" here?
GuardedByTest.java:36: [GuardedBy: UnguardedFieldAccessWarning] is "lock" locked when accessing field "counter" here?
GuardedByTest.java:48: [GuardedBy: UnguardedFieldAccessWarning] is "lock" locked when accessing field "counter" here?