Checker GuardedBy

belongs to group Advanced
Check and infer @GuardedBy and @Holding annotations

Frameworks supported by this checker

  • java up to 11
  • android up to API level 28
  • dotnet

Warnings generated by this checker

  • MissingSynchronizedWarning: a synchronized statement is needed to access a field [ CWE567 ]
  • UnguardedFieldWarning: a field is accessed without the expected lock being held [ CWE567 ]
  • UnguardedMethodOrConstructorWarning: a public or protected method or constructor might be called without the expected lock being held [ CWE820 ]
  • UnguardedParameterWarning: a parameter of a method or constructor is accessed without the expected lock being held [ CWE567 ]

Options accepted by this checker

  • annotationPackage: specify the package for the annotations used in the jaif file
    This option specifies which package must be used in the jaif file to identify the @GuardedBy and @Holding annotations. If it is not used, the default Julia package for those annotations is used
  • callsAreDereferences: instance method calls are considered as dereferences for the by-value @GuardedBy inference
    This option assumes that method calls are dereferences and consequently should be guarded if the dereferenced value must be annotated with @GuardedBy. This option is normally false, since instance method calls only access the class tag of the value, which is constant in Java and cannot be involved in a data race. By setting this option to true, the number of inferred @GuardedBy annotations by-value will shrink
  • fullyQualifiedNames: use fully qualified class names in the jaif files
    The generated jaif file is a compact report of the program places that are guarded by some lock. This option forces the use of fully qualified class names in the jaif file, also when referring to classes in the same package that is being reported
  • init: perform a preliminary class initialization analysis that simplifies the code
    A class initialization analysis determines where a class is already initialized, and hence its static initializer will never be called again. This option allows one to simplify the code before the actual lock analysis and can sometimes improve its precision. However, it increases the total cost of the analysis
  • jaif: dump a jaif file with the @GuardedBy information of the program
    A jaif file is a compact report of the program places that are guarded by some lock. It can be used for reference and documentation, but can also be imported in the source code of the program by using the annotation file utilities (see http://types.cs.washington.edu/annotation-file-utilities)
  • kind: specify the kind of semantics for the @GuardedBy annotations
    This option specifies if the annotations refer to the variables and fields or rather to the values that are contained inside those variables or fields
    • byName: @GuardedBy annotations refer to the name of the variables or fields. This is the default
    • byValue: @GuardedBy annotations refer to the values of the variables or fields
  • mergeCreations: merge the creation points for the same type inside the same class
    This enhances the efficiency of the creation points analysis performed as part of lock analysis but, in general, reduces the precision of the analyzer. However, it can be an important option to select for the analysis of very large applications and in library mode, in the rare cases when the creation points analysis takes too long to complete. This option is automatically selected for large programs
  • noReachability: do not perform reachability analysis
    This option reduces the precision of the analyzer. Only useful for statistics
  • noUnreachable: do not dump information on unreachable code
    By selecting this option, the jaif files become smaller
  • reportDeterministic: annotate the determinacy of methods in the jaif file
    The generated jaif file is a compact report of the program places that are guarded by some lock. This option, when used in conjunction with -jaif, uses also an extra annotation for the methods that always yield the same value when called from the same context
  • reportSideEffects: annotate the side-effect free methods and constructors in the jaif file
    The generated jaif file is a compact report of the program places that are guarded by some lock. This option, when used in conjunction with -jaif, uses also an extra annotation for the methods and constructors that have no side-effect

Annotations understood by this checker

  • @com.juliasoft.julia.checkers.guardedBy.GetsLocked
  • @com.juliasoft.julia.checkers.guardedBy.GetsUnlocked
  • @com.juliasoft.julia.checkers.guardedBy.GuardedBy
  • @com.juliasoft.julia.checkers.guardedBy.Holding


Description

Java uses synchronized statements and methods to guarantee that data is accessed in a sequential way and avoid race conditions in multithreaded applications. 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.

.NET uses statements and methods to guarantee thatdata is accessed in a sequential way and avoid race conditions in multithreaded applications. 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 attributes 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] attributes. If this checker does not accept those attributes, it is likely the case that your program has a synchronization problem.

The [GuardedBy] attribute for fields and parameters and the [Holding] attribute for methods and constructors accepts a string argument, according to the following syntax

  • [GuardedBy/Holding(new string[] { "this" })]: the lock on the receiver of a non-static field or method must be held
  • [GuardedBy(new string[] {"itself")]: the lock on the same parameter or field must be held
  • [GuardedBy/Holding(new string[] { "field-name" })]: the lock on the named field of the receiver of a non-static field or method must be held
  • [GuardedBy/Holding(new string[] { "Class.field-name" })]: the lock on the named static field of the named class must be held
  • [GuardedBy/Holding(new string[] { "Class.class" })]: the lock of the unique class object representing the class named Class must be held
  • [GuardedBy/Holding(new string[] { "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(new string[] { "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 isRegistered() 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] Expression "GuardedByTest.class" does not seem to be always locked when method "decrementCounter3" is called

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: [GuardedBy: UnguardedFieldWarning] is "lock" locked when accessing field "counter"?

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:

using System;
using System.Collections.Generic;

namespace GuardedBy 
{
  	public class GuardedBy
    {
        private readonly HashSet<string> users = new HashSet<string>();
        public void Register(string user)
        {
            lock (users)
            {
                users.Add(user);
            }
        }
        public void Unregister(string user)
        {
            lock (users)
            {
                users.Remove(user);
            }
        }
        public bool IsRegistered(string user)
        {
            return users.Contains(user); 
        }
        public int CountUsers()
        {
            lock (users)
            {
                return users.Count;
            }
        }
    }
}

This checker issues in this case the following warning:

UserRegistry.java:25: [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 lock on the access to field users inside method IsRegistered() as well. We recall that hashsets are not thread-safe in .NET and concurrent access to the same hashset might result in inconsistent behaviors or even deadlock. Another solution, here, would be to use a concurrent set, by exploiting the classes already available in the .NET library. In that case, no lock statement would be needed anymore.

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


Inferring @GuardedBy/@Holding attributes

Consider the following class:

using System;
using System.Runtime.CompilerServices;
using com.juliasoft.julia.checkers.guardedBy;

namespace GuardedByTest 
{
  public class GuardedByTest
    {
        [GuardedBy(new string[] { "lock1" })] private int counter;
        private object lock1 = new object();
        private long counter2;
        private static int counter3;
        private static object lock4 = new object();
        private static int counter4 = 13;
        private readonly object[] locks = new object[10];
        private int next;
        private readonly object lock5 = new object();
        private static readonly object lock6 = new object();
        private int counter5;
        public GuardedByTest()
        {
            counter = 1;
            counter5 = 17;
            counter5 += counter;
        }
        [MethodImpl(MethodImplOptions.Synchronized)]
        public void IncrementCounter()
        {
            counter++;
        }
        public void DecrementCounter()
        {
            lock (this)
            {
                counter--;
            }
        }
        public bool CheckCounterIs0()
        {
            object copy = this;
            lock (copy)
            {
                return counter == 0;
            }
        }
        public void IncrementOtherCounter(GuardedByTest other)
        {
            GuardedByTest copy = other;
            lock (copy)
            {
                IncrementCounterAux(other);
            }
        }
        private void IncrementCounterAux([GuardedBy(new string[] { "this" })] GuardedByTest other)
        {
            other.counter += 2;
        }
        public void IncrementCounter2()
        {
            lock (lock1)
            {
                counter2++;
            }
        }
        public void DecrementCounter2()
        {
            lock (lock1)
            {
                counter2--;
            }
        }
        public bool CheckCounter2Is0()
        {
            object copy = lock1;
            lock (copy)
            {
                return counter2 == 0;
            }
        }
        public void IncrementOtherCounter2(GuardedByTest other)
        {
            GuardedByTest copy = other;
            lock (copy.lock1)
            {
                IncrementCounter2Aux(other);
            }
        }
        private static void IncrementCounter2Aux(GuardedByTest other)
        {
            other.counter2 += 2;
        }
        public void IncrementCounter3()
        {
            lock (typeof(GuardedByTest))
            {
                counter3++;
            }
        }
        [Holding(new string[] { "GuardedByTest.class" })]
        [MethodImpl(MethodImplOptions.Synchronized)]
        public static void DecrementCounter3()
        { // UnguardedMethodOrConstructorWarning
            counter3--;
        }
        public void IncrementCounter4()
        {
            lock (lock4)
            {
                counter4++;
            }
        }
        public static void DecrementCounter4()
        {
            lock (lock4)
            {
                DecrementCounter4Aux();
            }
        }
        [Holding(new string[] { "GuardedByTest.lock4" })]
        private static void DecrementCounter4Aux()
        {
            counter4--;
        }
        private object GetLock()
        {
            return locks[next % locks.Length];
        }
        public void IncrementCounter5()
        {
            lock (GetLock())
            {
                counter5++;
                next++;
            }
        }
        public void DecrementCounter5()
        {
            lock (GetLock())
            {
                DecrementCounter5Aux();
            }
        }
        private void DecrementCounter5Aux()
        {
            counter5--;
        }
        public void AccessLock5()
        {
            lock (lock5)
            {
                lock5.GetHashCode();
            }
        }
        public static void AccessLock6()
        {
            lock (lock6)
            {
                lock6.GetHashCode();
            }
        }
        [MethodImpl(MethodImplOptions.Synchronized)]
        public void ParameterTest1(object o1, string o2, string o3)
        {
            Console.WriteLine(o1);
            lock (lock1)
            {
                Console.WriteLine(o2);
            }
            lock (o3)
            {
                Console.WriteLine(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(LSystem.Object;LSystem.String;LSystem.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 System.Type 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 132 and 133, 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 54). Hence the analyzer issues the following warning:
    GuardedByTest.java:55: [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:102: [GuardedBy: UnguardedMethodOrConstructorWarning] Expression "GuardedByTest.class" does not seem to be always locked when method "DecrementCounter3" is called

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("lock1")
  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: [GuardedBy: UnguardedFieldWarning] is "lock1" locked when accessing field "counter"?