This document describes annotations for lock-based concurrency only. Annotations for non-lock threading, API compliance, and other assurances are described elsewhere.

The Basic Lock Model

The canonical Java model whereby an object protects itself is declared by annotating a class with:

  /**
   * @lock Lock is this protects Instance
   */
  public class C { ... }

This

1. Declares a new lock named Lock
2. Identifies that lock with instances of the class (this)
3. Protects all the fields in instances of the class (the region Instance)

In other words, all accesses to instance variables of objects of class C must be within blocks synchronized on the instance. The lock name enables consistent reference to the lock object in other annotations.

Extending the Model: Caller Locking

The programmer can declare that it is the caller’s responsibility to acquire a lock by annotating a method with:

  /** @requiresLock Lock */
  protected void M { ... }

Analysis assumes that lock Lock is held when analyzing the method, but requires that the method be invoked from within a block synchronized on Lock.

Extending the Model: Aggregating Arrays

An array in Java is a separate object from the object that refers to the array. Protecting an array-typed field thus protects the reference to the array only. It is not sufficient to extend the protection to the elements of the array; we also need to know that the array object is not aliased. If it were, then it would be possible to concurrently access the array even though individual references to the array are protected. Much of the time, however, it is not intended that an array is aliased; in these cases, the array can be incorporated into the state of the object that references it. We call this aggregating state. An array is aggregated into the object that references it by adding a pair of annotations to the field that references the array:

  /**
   * @unshared
   * @aggregate [] into Instance
   */
  private Object[] myArray;

This does two things:

1. Declares the programmer’s intent that the field is unaliased. A separate set of analyses is used to assure that the field is never aliased.
2. Extends the state of the referencing object to include the elements of the array.

Constructors

Constructors cannot be declared synchronized in Java, but our assurance requires that fields protected by a lock only be accessed when that lock is held. So how do we keep are assurance from failing when analyzing a constructor? We rely on the fact that during object construction, an object is almost always accessed by a single thread only—the thread that invoked the constructor. When this is the case, we can proceed as if the locks for the object’s state are already held. The programmer can declare this single threaded intent by annotating the constructor:

  /**
   * @singleThreaded
   * @borrowed this
   */
  public Constructor() { ... }

One way that analysis can assure the single-threadedness of the constructor is to leverage the assurance that the constructor "borrows" the constructed object—that is, that it does not create an alias to it. (The @borrowed annotation is further described below.) In particular, because it does not create an alias, no other thread can obtain a reference to the object under construction during the constructor’s execution.

Note: Annotating a constructor as being @singleThreaded requires that the super-constructor it invokes is also @singleThreaded.

Field/instance Initializers and Implicit Constructors

Field initializers are considered to be part of the object construction process, and fields that have initializers are considered to be written to. Instance initializer blocks are also part of the object construction process and need to be assured accordingly. This can be become problematic when a class doesn't have an explicit constructor:

/**
 * @lock L is this protects Instance 
 */
public class C {
  private int f = 1;
  private int g;

  {
    g = 2;
  }

  public synchronized int getF() {
    return f;
  }

  public synchronized void incG() {
    g += 1;
  }
}

The lock assurance would fail to assure the correct use of lock L because the accesses to f and g during construction is not protected. One way to fix this is to simply to make the constructor explicit and annotate it:

/**
 * @lock L is this protects Instance 
 */
public class C {
  private int f = 1;
  private int g;

  {
    g = 2;
  }
  
  /**
   * @singleThreaded
   * @borrowed this
   */
  public C() {}

  public synchronized int getF() {
    return f;
  }

  public synchronized void incG() {
    g += 1;
  }
}

Alternatively, if it is undesirable to insert the constructor explicitly, the constructor can still be annotated using a scoped promise. These are described in more detail below, but for the case of annotating an implicit constructor, we would annotate the class as follows:

/**
 * @lock L is this protects Instance 
 * @promise "@singleThreaded" for new()
 * @promise "@borrowed this" for new()
 */
public class C {
  ...
}

Advanced Models of Locked State

Our lock assurance actually associates locks with regions. A region is a named, hierarchical abstraction of state. All fields are regions, and thus a region is a named, extensible set of fields. All instance fields are by default children of the region Instance. The general form of the @lock annotation is

  /**
   * @lock LockName is Lock protects Region
   */

where LockName is a programmer-declared name for the lock, Lock is a final field or this, and Region is the name of a region. The reference to the lock object (the clause between is and protects) may be one of the following:

• this, meaning the object itself is acquired to protect the state.
• A field declared in the class being annotated or an ancestor of the class being annotated that is visible within the class (i.e, a protected field from an ancestor). The field must refer to an object (i.e., the field cannot be of type int). The field must be final, otherwise the lock object could change. The field may be static or instance.
• class, meaning the unique Class object referenced by the static pseudo-field class. (This is the object that is locked by static synchronized methods.)
• A field of an "outer" class. If the class is declared inside class Outer, and wants to declare that the field f of the instance that is the container for the inner class's instance protects a region of the inner class, then the lock reference is given by "Outer.this#f". Note: While the tool supports declaring locks that are the fields of outer classes, it is not presently possible to assure their correct use. This is because of deficiencies in both our internal representation and with Java syntax (i.e., given an a variable v that refers to an instance of a non-static inner class, there is no syntactic expression that evaluates to the "outer" object of that instance, that is, the object referenced by o in the expression o. new Inner()). We allow the declaration of such locks, even though they cannot be assured, because we have encountered them in real code and it is nice to be able to document the design intent.

A region may only be associated with a lock declared in a class C if the region doesn't contain any fields from superclasses of C. This is trivially true if the region is declared in C. The region may have abstract sub-regions, but they also cannot contain any fields. Specifically, the region (and any of its subregions) cannot contain any fields, when considered from the point of view of the class in which the lock declaration appears. (Indeed, otherwise you could never associate a lock with a region.) This restriction exists to prevent unsoundness. Suppose a class C declared a region R and populated it with field f. Suppose D extends C, adds field g to region R, and also associates R with a lock. The problem is, in contexts where a D object is viewed as a C (like, for example, if a D reference is cast to a C reference, or in methods that take C parameters) analysis cannot enforce D's locking policy. Thus, fields in R that should be protected might not be, and analysis wouldn't complain. We allow the protection of empty regions to be delayed because (tautologically) they contain no state and therefore there is no real state that can be accessed through that region by "unprotected" superclasses. ANy actual code that access es state in that region must access the region through a subclass that does know about the protection, and therefore analysis can enforce the protection.

New regions are declared by annotating a class with

  /** @region [static] Region [extends Parent] */

which declares a new region Region which is a subregion of Parent. If no parent region is specified, Instance is used. A region may be declared to be static. Static regions must extend static regions; non-static regions may extend static regions.

A field may be placed in a user-declared region by annotating the field declaration:

  /** @mapInto Region */
  private int f;

A static field must only be mapped into a static region. Non-static fields may be mapped into either static or non-static regions.

A static region must be protected by a static field or by class.

Thus, the state of an object may be partitioned into multiple abstract regions, each protected by a different lock, enabling concurrent access to different segments of the object’s state.

Alternatively, we can map multiple fields into a given region using the @mapFields class annotation:

/**
 * @region public Region
 * @mapFields f, g, o into Region
 */
public class C {
  private int f, g;
  private Object o;
  ...
}

Returning Locks

A method may be declared to return a particular lock using the @returnsLock annotation. This allows an implementation to provide access to a lock object without revealing how that lock is "implemented." That is, the identity of the field that refers to the lock is kept hidden by the implementation, although the lock object is made accessable to clients. The @returnsLock annotation is fully checked: it is checked that the method actually returns the object representing the lock it says it returns. The following code fragment shows an example use of the @returnsLock annotation.

/**
 * @lock DataLock is lock protects DataRegion
 * ...
 */
public class C {
  // NOTE: Field is private
  private final Object lock = new Object();

  /** @returnsLock DataLock */
  protected Object getDataLock() { return lock; }

  ...

  public void doSomething() {
    synchronized (getDataLock()) {
      // Access DataRegion ...
    }
  }
}

The only example of this type of thing we have encountered in "the wild" is the method getTreeLock() in class java.awt.Container.

Policy Locks

Sometimes there isn't any obvious state to associate with a lock. That is, a lock is being used to enforce some "higher level" invariant that requires a section of code to execute atomically with respect to some other section of code. We call locks used for such a purpose policy locks. They can be declared using the annotation

  /**
   * @policyLock LockName is Lock 
   */

This annotation is basically the same as the @lock annotation except that it doesn't associate the lock with any particular region of state. The tool does not provide any assurance about the uses of policy locks. The annotation is primarily used to document the intent behind the lock, and to suppress tool warnings about a particular lock object being an unknown lock.

Policy locks are typically used to enforce an "initalize once" invariant. Here is an example from java.util.logging.Logger:

public static synchronized Logger getLogger(String name) {
  LogManager manager = LogManager.getLogManager();
  Logger result = manager.getLogger(name);
  if (result == null) {
    result = new Logger(name, null);
    manager.addLogger(result);
    result = manager.getLogger(name);
  }
  return result;
}

First, note the static method doesn't change any state directly. It's difficult so say what state the lock Logger.class is protecting. This is because the lock is ensuring that the method getLogger executes atomically with respect to itself. For if two threads were allowed to simultaneous exeucte the method it would be possible to create new Logger objects with the same name, but only one of them would be registered in the global log registry. This would cause problems later on during the use of the loggers. The synchronization ensures that only one Logger object is ever created for any given name.

Method Effects

Regions provide an abstract way to name the state of an object. The effects of a method—the state read and written during the execution of that method—may be expressed in terms of regions. Effects are useful when determining whether code can be reordered by a refactoring, and are also necessary to support the analyses that assure @unshared and @lock annotations. An unannotated method is assumed to have the annotation "@writes Object.All" which declares that the method could read from or write to anything in the heap. In particular,

• If only a @writes (respectively, @reads) clause is present, the @reads (respectively, @writes) clause is assumed to be empty (nothing).
• Write effects include read effects.
• The region All is a static region declared in class Object and is the parent of the region Instance.

A @reads/@writes annotation takes a list of targets that desribe the segments of state read or written by the method. Targets can be

• nothing, the empty target.
• this.Region, where Region is a region of the class containing the method. This target says the method affects the named region of the receiver.
• Region, which is that same as this.Region.
• param.Region, where param is a parameter of the method that references an object, and Region is a region of the class of param's type. This target indicates that the method affects the named region of the object referenced by param at the start of the method's execution. Note that the syntax changes a bit when writing standoff annotations for library code, because there are no parameter names in class files. For this case, refer to the parameters as arg0, arg1, etc.
• pkg.C.this.Region, where pkg.C is an "outer class" of the class that contains the annotated method. That is, the method being annotated is in class D, and D is an inner class of C. Region is a region of class pkg.C. This target indicates that the method affects the named region of the given outer class receiver.
• any(C).Region, where C is a class name and Region is a region of C. This target indicates that the method affects the given region of any object of class C.
• C.Region, where Region is a static region of class C. This target indicates that the method affects the given static region.

Assurance checks that the actual effects of the method implementation are no greater than the declared effects. There are several fine points to this: uses of final fields produce no effects, effects on local variables are not visible outside of a method, effects on objects created within a method are not visible outside of a method, constructors do not have to report effects on the Instance region of the newly constructed object, and region aggregation (described below) is taken into account.

Here is a simple "variable" class with effects annotations.

/** @region public Value */
public class Var {
  /** @mapInto Value */
  private int value;

  /** @writes nothing */
  public Value(int v) { value = v; }

  /** @reads Value */
  public int getValue() { return value; }

  /** @writes Value */
  public void setValue(int v) { value = v; }
}  

Incomplete Effects Assurance for Anonymous Class Expressions

Note: Effects analysis does not yet take into account all the effects of constructing an anonymous class expression. For example, in the expression

  D d = new D() {
          private int f = m();
 
          {
            n();
          }
          
          protected int doStuff() { ... }
        }; 

The effects should include

• The effects of invoking the super constructor D()
• The effects of initializing f, i.e., the effects of invoking m()
• The effects of the instance initializer, i.e., the effects of invoking n()

But right now the analysis is only including the effects of the super constructor.

Effects and @singleThreaded Constructors

A @singleThreaded constructor may also be assured by checking whether the declared effects of the constructor are included in the effect @writes Instance and (if you read outside state) @reads Object.All. You must also ensure you don't start any threads by promising @starts nothing. Because the constructor may only affect its own state, it cannot write a reference to itself to anyplace readable from another thread, and thus no other thread will be able to access the object during the execution of the constructor. Of, course, as @starts nothing promises this safe only if the constructor starts no threads. Here's the most common case, which was used to assure much of Doug Lea's util.concurrent library (for which @borrowed this did not work due to aliasing of this into a private field):

  /**
   * @singleThreaded
   * @writes nothing
   * @starts nothing
   */
  public Constructor() { ... }

More on Unshared Fields

Any reference-typed field, not just arrays, can be declared to be @unshared. Furthermore, state aggregation allows any region of the uniquely referenced object to be aggregated into a region of the referring object (subject to certain well-formedness rules that make sure the region hierarchy is preserved). In particular, in the case of arrays, [] is merely the name of the region used to represent arrays elements. Thus, if objects of class C had regions R1 and R2, then they could be separately aggregated into distinct regions of class D as follows:

  /** 
   * @region P1
   * @region P2
   * @region P3
   * @lock Lock1 is this protects P1
   * @lock Lock2 is l2 protects P2
   * @lock Lock3 is l3 protects P3
   */
  public class D {
    private final Object l2 = new Object();
    private final Object l3 = new Object();

    /**
     * @mapInto P1
     * @unshared
     * @aggregate R1 into P2, R2 into P3
     */
    private C myC;
    ...
  }

Here, class D declares three regions. It locates the field myC in the first region, P1, and aggregates the regions of myC, R1 and R2, into regions P2 and P3, respectively. Each region in D is associated with a different lock. Thus, the reference to the C object, myC, is protected by synchronizing on this, while access to the regions of R1 and R2 of the C object are protected by synchronizing on l2 and l3, respectively, because they are the locks associated with D’s regions P2 and P3. We emphasize that access to region R1 of the object referenced by myC is protected by synchronizing on the lock of the object referenced by L2.

Self-protected Objects

Region aggregation, described above, is one technique that can be used to deal with the fact that fields reference objects. But it is not always possible to use region aggregation to simplify reasoning about protected state because a field may be aliased. In such cases, the tool may produce warnings that a reference of the form e.f.g, where f is field protected by a lock, is a “possibly unsafe reference to protected shared state.” The message is meant to remind the programmer that although the field f is protected by a lock, this lock doesn't also protect the field g. (If field f is of class C and class C declares that g is protected by a lock then this warning is not produced—the tool instead attempts to assure that the appropriate lock for g is held.) There are situations where invoking a method via e.f.m will also produce a the above warning.

Region aggregation and lock declaration (as described above) can be used to suppress these warnings. In general, we can suppress this warning for fields f that refernece objects of class C by annotating class C with @selfProtected. This unchecked annotation declares that instances of the class/interface are meant to be “thread safe.” Exactly what is meant by this is presently unspecified but the annotation is intended to encompass non–lock -based protections schemes such as single-threadedness and immutability. No analysis is performed on classes annotated with @selfProtected to assure that the implementation is thread safe.

As an example, let's consider the simple rational numbers class below.

public class Rational {
  private final int numerator;
  private final int denominator;

  public Rational(int n, int d) {
    numerator = n;
    denominator = d;
  }

  public int getNumerator() { return n; }
  public int getDenominator() { return d; }
}

Suppose we have a client class that has a lock-protected reference to a Rational object:

/**
 * @lock L is this protects Instance
 */
public class C {
  ...
  private Rational r;

  public synchronized doStuff() {
    int n = r.getNumerator();  // (*)
    ...
  }
}

The Fluid tool is going to complain on line (*) that “Receiver r may be a shared unprotected object.” That is, we may be doing something unsafe: accessing the state of the rational object in multiple threads without protection. But in this case, we know that Rational objects are immutable, and thus thread safe, so we can suppress this warning by annotating the Rational class as follows

/**
 * @selfProtected
 */
public class Rational { ... }

Borrowed References

When an object is passed as a parameter to a method, an alias to that object is created. Thus, if strictly enforced, an @unshared field can never be passed as a parameter to a method, even as the receiver! But if a method is known to not create any additional aliases to the object, then an @unshared field may safely be passed as a parameter because it is guaranteed that the method will restore the uniqueness of the field. However, the method is not allowed to directly or indirectly make use of the @unshared field used as the parameter because the field is not unshared within the dynamic scope of the method. A parameter (including the receiver) is declared to be borrowed by annotating the method:

  /** @borrowed this, array */
  public void copyInternalArray( Object[] array ) {
    for( int i = 0; i < array.length; i++ ) {
      array[i] = this.myArray[i];
    }
  }

If this method belongs to class C, then it may be invoked on @unshared references to C objects; it may also be passed @unshared references to arrays. Here it is easy to see that no aliases to this or to array are created, but, in general, this is a property that is easily violated, and a separate set of analyses from those used to assure locking are used to assure that @unshared and @borrowed variables are used correctly.

Borrowed parameters and method effects

As stated above, the purpose of the @borrowed parameter is to allow a uniquely referenced object to be passed as a parameter, temporarily creating an alias to the object. We must assure that the object is only referenced via the @borrowed parameter during the execution of the method, otherwise the uniqueness constraint will not hold during the dynamic lifetime of the method. This is enforced through the analysis of method call sites. When a method call passes an @unshared field to a @borrowed parameter, we check whether the effects of the method call include reading from that @unshared field. If they do, the method call is invalid because it would result in the object being referenced from (at least) two different references during the execution of the method: (1) the @borrowed parameter and (2) the field itself.

Thus, it is often the case that when a parameter (including the receiver this) is annotated as @borrwoed, the method must also be annoted with its effects. If the method is invoked using @unshared fields then the effects will need to be declared so that the call sites can be positively assured.

Consider the example:

class Var {
  private int value = 0;

  /** @borrowed this */
  public void set(int v) { value = v; }

  /** @borrowed this */
  public int get() { return v; }
}

It's pretty obvious that we can declare the receiver to be @borrowed for the accessor methods. If we never actually use an @unshared field as the receiver then we do not need to declare the effects of the accessor methods:

class VarClient {
  private Var v1 = new Var();
  private Var v2 = new Var();

  public void doStuff() {
    v1.set(1);
    v2.set(2);
    ...
    v1.set(v2.get()+3);
  }
}

But, if we do the following

class VarClient2 {
  /** @unshared */
  private Var v1 = new Var();
  private Var v2 = new Var();

  public void doStuff() {
    v1.set(1);
    v2.set(2);
    ...
    v1.set(v2.get()+3);
  }
}

we need to know that set isn't going to read the field v1. Here it is obviously that it doesn't, but in cases where the invoked method retrieves objects from collections or other global objects pools, it is n't so obvious. We must explicitly declare the effects of set to allow the uniqueness analysis to assure the call (we also decalre the effecst of set for completeness):

class Var {
  private int value = 0;

  /**
   * @borrowed this
   * @writes this.Instance
   */
  public void set(int v) { value = v; }

  /**
   * @borrowed this
   * @reads this.Instance
   */
  public int get() { return v; }
}

Structure

(Under development) In some cases it is intended that program structure be more restrictive than can be expressed within the Java programming language. Two structural annotations can be used to limit subtyping and type use within a software system.
Limiting subtyping. The @subtypedBy annotation limits subtypes of an annotated class to only a specified set.

/** @subtypedBy S1, edu.cmu.S2 */
class S { ... }

In the above example the types S1 and S2 can extend S but no other types may (i.e., class Rogue extends S would cause a violation).
Limiting type use The @usedBy annotation limits direct type use to only a specified set.

/** @usedBy S1, S2 */
class S { ... }

In the above example the types S1 and S2 can use S but no other types may.

Thread effects

Thread effects can be used to assure that code does not start any threads the @starts nothing promise can be used. For example,

/** @assume "@starts nothing" for Exception:new() */
class C {
  /** @starts nothing */
  public C() { m(); ... new Exception();... }
  /** @starts nothing */
  private void m() { ... }

Not the modular nature of this promise, because the constructor promises @starts nothing so must the m() method as well as the constructor for java.lang.Exception. We assume the promise on the constructor of java.lang.Exception (note for @assume a : is used rather than a . to separate package from class from method or constructor or field. This is because wildcards are allowed and . would be ambigious).

Scoped promises

In the case where design intent applies to most or all of a class, annotation tedium can be reduced using a scoped promise. Consider a class, S, with a large number of constructors and methods. We can annotate S as follows:

/** 
 * @lock L is this protects Instance
 * @promise "@borrowed this"
 * @promise "@singleThreaded"
 */
public class S { ... }

Here the second and third annotation are scoped promises that specify that @borrowed this is intended on all methods and constructors of S and that @singleThreaded is intended on all constructors of S. The @promise annotation creates virtual annotations on all locations in the class where the promise is allowed. Subsets can be specified using a pattern language, for example:

@promise "@borrowed this" for new(**)

The for-clause above limits the target for @borrowed this to only S’s constructors.

Annotation Summary

Regions

@region Region extends Parent
@mapInto Region
@aggregate Region into Region

Locks

@lock LockName is Lock protects Region
@requiresLock LockName
@singleThreaded

Unshared Fields

@unshared
@borrowed param_1, ..., param_n

Structure (under development)

@usedBy type_1, ..., type_n
@subtypedBy type_1, ..., type_n

Scoped promises

@promise “promise”
@promise “promise” for target-pattern
@assume "promise" for target-pattern

Important! Class names are separated from package names and method names using a “:”. So the pattern a.b.c:d:m() refers to method m() in class d in package a.b.c. Inner classes are separated from their outer class using “.”. Thus a.b.c:d.e:m() refers to method m() in class e nested in class d in package a.b.c.

Futhermore, wildcards are allowed for method parameters: “*” means any type for a specific parameter position; “**” means any number of parameters of any type. So m(*) matches all methods m with one parameter; m(*, int) matches all methods m with two parameters, where the first is anything, and the 2nd parameter is int; and m(**) is all methods m regardless of the number of parameters and their types.

Also, constructors are matched with the name new: e.g., java.lang:ArrayList:new(**).

Modules (under development)

@module outer.middle.inner
@vis (outer.middle.inner)?

Conceptually, this is what packages should have been. We use the dotted notation to imply that a module outer and a module outer.middle exist. @module applies to compilation units. @vis annotates types, methods and fields and optionally names a module as the limit of that Java element's visibility, e.g., it will be made visible to users of that module.

Module evolution (under development)

@module outer contains inner
@export (outer)?

Ideally, we would use the dotted module notation to design our module structure, but if we have already annotated our code to create some modules and want to wrap those into a larger module, we can use these annotations to do so. This variant of @module should only appear in package-info.java or package promise XML files. @export has the same syntax as @vis and a similar meaning, except it boosts the visibility of an existing @vis to an immediately enclosing module. Usually, @export will not directly appear in the source code, but will be used as part of a scoped promise

Scoped modules

@module outer.middle.inner for target-pattern

This should appear in package-info.java or package promise XML files, and uses the same target syntax for types as usual scoped promises, although it applies the @module annotation to the enclosing compilation units.