The Checker Framework Manual:
Custom pluggable types for Java

Chapter 10 Lock Checker

The Lock Checker prevents certain concurrency errors by enforcing a locking discipline. A locking discipline indicates which locks must be held when a given operation occurs. You express the locking discipline by declaring a variable’s type to have the qualifier @GuardedBy("lockexpr"). This indicates that the variable’s value may be dereferenced only if the given lock is held.

To run the Lock Checker, supply the -processor org.checkerframework.checker.lock.LockChecker command-line option to javac. The -AconcurrentSemantics command-line option is always enabled for the Lock Checker (see Section 40.4.6).

10.1 What the Lock Checker guarantees

The Lock Checker gives the following guarantee. Suppose that expression e has type @GuardedBy({"x", "y.z"}). Then the value computed for e is only dereferenced by a thread when the thread holds locks x and y.z. Dereferencing a value is reading or writing one of its fields. The guarantee about e’s value holds not only if the expression e is dereferenced directly, but also if the value was first copied into a variable, returned as the result of a method call, etc. Copying a reference is always permitted by the Lock Checker, regardless of which locks are held.

A lock is held if it has been acquired but not yet released. Java has two types of locks. A monitor lock is acquired upon entry to a synchronized method or block, and is released on exit from that method or block. An explicit lock is acquired by a method call such as Lock.lock(), and is released by another method call such as Lock.unlock(). The Lock Checker enforces that any expression whose type implements Lock is used as an explicit lock, and all other expressions are used as monitor locks.

Ensuring that your program obeys its locking discipline is an easy and effective way to eliminate a common and important class of errors. If the Lock Checker issues no warnings, then your program obeys its locking discipline. However, your program might still have other types of concurrency errors. For example, you might have specified an inadequate locking discipline because you forgot some @GuardedBy annotations. Your program might release and re-acquire a lock when correctness requires holding it throughout a computation. And, there are other concurrency errors that cannot, or should not, be solved with locks.

10.2 Lock annotations

This section describes the lock annotations you can write on types and methods.

10.2.1 Type qualifiers

@GuardedBy(exprSet)

If a variable x has type @GuardedBy("expr"), then a thread may dereference the value referred to by x only when the thread holds the lock that expr currently evaluates to.

The @GuardedBy annotation can list multiple expressions, as in @GuardedBy({"expr1", "expr2"}), in which case the dereference is permitted only if the thread holds all the locks.

Section 33.8 explains which expressions the Lock Checker is able to analyze as lock expressions. These include <self>, the value of the annotated reference (non-primitive) variable. For example, @GuardedBy("<self>") Object o indicates that the value referenced by o is guarded by the intrinsic (monitor) lock of the value referenced by o.

@GuardedBy({}), which means the value is always allowed to be dereferenced, is the default type qualifier that is used for all locations where the programmer does not write an explicit locking type qualifier (except all CLIMB-to-top locations other than upper bounds and exception parameters — see Section 33.5.3). (Section 10.5.4 discusses this choice.) It is also the conservative default type qualifier for method parameters in unannotated libraries (see Chapter 36).

@GuardedByUnknown

If a variable x has type @GuardedByUnknown, then it is not known which locks protect x’s value. Those locks might even be out of scope (inaccessible) and therefore unable to be written in the annotation. The practical consequence is that the value referred to by x can never be dereferenced.

Any value can be assigned to a variable of type @GuardedByUnknown. In particular, if it is written on a formal parameter, then any value, including one whose locks are not currently held, may be passed as an argument.

@GuardedByUnknown is the conservative default type qualifier for method receivers in unannotated libraries (see Chapter 36).

@NewObject

This type represents a newly-constructed value, such as the result of calling a constructor or factory method. The client can use the value as any @GuardedBy type.

@GuardedByBottom

If a variable x has type @GuardedByBottom, then the value referred to by x is null and can never be dereferenced.

Figure 10.1 shows the type hierarchy of these qualifiers. All @GuardedBy annotations are incomparable: if exprSet1 ≠ exprSet2, then @GuardedBy(exprSet1) and @GuardedBy(exprSet2) are siblings in the type hierarchy. You might expect that @GuardedBy({"x", "y"}) T is a subtype of @GuardedBy({"x"}) T. The first type requires two locks to be held, and the second requires only one lock to be held and so could be used in any situation where both locks are held. The type system conservatively prohibits this in order to prevent type-checking loopholes that would result from aliasing and side effects — that is, from having two mutable references, of different types, to the same data. See Section 10.4.2 for an example of a problem that would occur if this rule were relaxed.

Polymorphic type qualifiers

@GuardSatisfied(index)

If a variable x has type @GuardSatisfied, then all lock expressions for x’s value are held.

As with other qualifier-polymorphism annotations (Section 32.2), the index argument indicates when two values are guarded by the same (unknown) set of locks.

@GuardSatisfied is only allowed in method signatures: on formal parameters (including the receiver) and return types. It may not be written on fields. Also, it is a limitation of the current design that @GuardSatisfied may not be written on array elements or on local variables.

A return type can only be annotated with @GuardSatisfied(index), not @GuardSatisfied.

See Section 10.4.6 for an example of a use of @GuardSatisfied.

10.2.2 Declaration annotations

The Lock Checker supports several annotations that specify method behavior. These are declaration annotations, not type annotations: they apply to the method itself rather than to some particular type.

Method pre-conditions and post-conditions

@Holding(String[] value)

All the given lock expressions are held at the method call site.

@EnsuresLockHeld(String[] value)

The given lock expressions are locked upon method return if the method terminates successfully. This is useful for annotating a method that acquires a lock such as ReentrantLock.lock().

@EnsuresLockHeldIf(String[] expression, boolean result)

If the annotated method returns the given boolean value (true or false), the given lock expressions are locked upon method return if the method terminates successfully. This is useful for annotating a method that conditionally acquires a lock. See Section 10.4.4 for examples.

Side effect specifications

@LockingFree

The method does not acquire or release locks, directly or indirectly. The method is not synchronized, it contains no synchronized blocks, it contains no calls to lock or unlock methods, and it contains no calls to methods that are not themselves @LockingFree.

Since @SideEffectFree implies @LockingFree, if both are applicable then you only need to write @SideEffectFree.

@ReleasesNoLocks

The method maintains a strictly nondecreasing lock hold count on the current thread for any locks that were held prior to the method call. The method might acquire locks but then release them, or might acquire locks but not release them (in which case it should also be annotated with @EnsuresLockHeld or @EnsuresLockHeldIf).

This is the default for methods being type-checked that have no @LockingFree, @MayReleaseLocks, @SideEffectFree, or @Pure annotation.

@MayReleaseLocks

The method may release locks that were held prior to the method being called. You can write this when you are certain the method releases locks, or when you don’t know whether the method releases locks. This is the conservative default for methods in unannotated libraries (see Chapter 36).

10.3 Type-checking rules

In addition to the standard subtyping rules enforcing the subtyping relationship described in Figure 10.1, the Lock Checker enforces the following additional rules.

10.3.1 Polymorphic qualifiers

@GuardSatisfied

The overall rules for polymorphic qualifiers are given in Section 32.2.

Here are additional constraints for (pseudo-)assignments:

• If the left-hand side has type @GuardSatisfied (with or without an index), then all locks mentioned in the right-hand side’s @GuardedBy type must be currently held.
• A formal parameter with type qualifier @GuardSatisfied without an index cannot be assigned to.
• If the left-hand side is a formal parameter with type @GuardSatisfied(index), the right-hand side must have an identical @GuardSatisfied(index) type.

If a formal parameter type is annotated with @GuardSatisfied without an index, then that formal parameter type is unrelated to every other type in the @GuardedBy hierarchy, including other occurrences of @GuardSatisfied without an index.

@GuardSatisfied may not be used on formal parameters, receivers, or return types of a method annotated with @MayReleaseLocks.

10.3.2 Dereferences

@GuardedBy

An expression of type @GuardedBy(eset) may be dereferenced only if all locks in eset are held.

@GuardSatisfied

An expression of type @GuardSatisfied may be dereferenced.

Not @GuardedBy or @GuardSatisfied

An expression whose type is not annotated with @GuardedBy or @GuardSatisfied may not be dereferenced.

10.3.3 Primitive types, boxed primitive types, and Strings

Primitive types, boxed primitive types (such as java.lang.Integer), and type java.lang.String are annotated with @GuardedBy({}). It is an error for the programmer to annotate any of these types with an annotation from the @GuardedBy type hierarchy, including @GuardedBy({}).

10.3.4 Overriding

Overriding methods annotated with @Holding

If class B overrides method m from class A, then the expressions in B’s @Holding annotation must be a subset of those in A’s @Holding annotation.

Overriding methods annotated with side effect annotations

If class B overrides method m from class A, then the side effect annotation on B’s declaration of m must be at least as strong as that in A’s declaration of m. From weakest to strongest, the side effect annotations processed by the Lock Checker are:

 @MayReleaseLocks
 @ReleasesNoLocks
 @LockingFree
 @SideEffectFree
 @Pure

10.3.5 Side effects

Releasing explicit locks

Any method that releases an explicit lock must be annotated with @MayReleaseLocks. The Lock Checker issues a warning if it encounters a method declaration annotated with @MayReleaseLocks and having a formal parameter or receiver annotated with @GuardSatisfied. This is because the Lock Checker cannot guarantee that the guard will be satisfied throughout the body of a method if that method may release a lock.

No side effects on lock expressions

If expression expr is used to acquire a lock, then expr must evaluate to the same value, starting from when expr is used to acquire a lock until expr is used to release the lock. An expression is used to acquire a lock if it is the receiver at a call site of a synchronized method, is the expression in a synchronized block, or is the argument to a lock method.

Locks are released after possible side effects

After a call to a method annotated with @LockingFree, @ReleasesNoLocks, @SideEffectFree, or @Pure, the Lock Checker’s estimate of held locks is the same as that prior to the method call. After a call to a method annotated with @MayReleaseLocks, the estimate of held locks is conservatively reset to the empty set, except for those locks specified to be held after the call by an @EnsuresLockHeld or @EnsuresLockHeldIf annotation on the method. Assignments to variables also cause the estimate of held locks to be conservatively reduced to a smaller set if the Checker Framework determines that the assignment might have side-effected a lock expression. For more information on side effects, please refer to Section 33.7.5.

10.4 Examples

The Lock Checker guarantees that a value that was computed from an expression of @GuardedBy type is dereferenced only when the current thread holds all the locks named in the @GuardedBy annotation.

10.4.1 Examples of @GuardedBy

The following example demonstrates the basic type-checking rules.

class MyClass {
  final ReentrantLock lock; // Initialized in the constructor

    @GuardedBy("lock") Object x = new Object();
    @GuardedBy("lock") Object y = x; // OK, since dereferences of y will require "lock" to be held.
    @GuardedBy({}) Object z = x; // ILLEGAL since dereferences of z don't require "lock" to be held.
    @GuardedBy("lock") Object myMethod() { // myMethod is implicitly annotated with @ReleasesNoLocks.
       return x; // OK because the return type is annotated with @GuardedBy("lock")
    }

    [...]

    void exampleMethod() {
       x.toString(); // ILLEGAL because the lock is not known to be held
       y.toString(); // ILLEGAL because the lock is not known to be held
       myMethod().toString(); // ILLEGAL because the lock is not known to be held
       lock.lock();
       x.toString(); // OK: the lock is known to be held
       y.toString(); // OK: the lock is known to be held, and toString() is annotated with @SideEffectFree.
       myMethod().toString(); // OK: the lock is known to be held, since myMethod
                              // is implicitly annotated with @ReleasesNoLocks.
    }
}

Note that the expression new Object() is inferred to have type @GuardedBy("lock") because it is immediately assigned to a newly-declared variable having type annotation @GuardedBy("lock"). You could explicitly write new @GuardedBy("lock") Object() but it is not required.

The following example demonstrates that using <self> as a lock expression allows a guarded value to be dereferenced even when the variable to which the value was originally assigned falls out of scope.

class MyClass {
  private final @GuardedBy("<self>") Object x = new Object();
  void method() {
    x.toString(); // ILLEGAL because x is not known to be held.
    synchronized(x) {
      x.toString(); // OK: x is known to be held.
    }
  }

    public @GuardedBy("<self>") Object get_x() {
      return x; // OK, since the return type is @GuardedBy("<self>").
    }
}

class MyOtherClass {
  void method() {
    MyClass m = new MyClass();
    final @GuardedBy("<self>") Object o = m.get_x();
    o.toString(); // ILLEGAL because o is not known to be held.
    synchronized(o) {
      o.toString(); // OK: o is known to be held.
    }
  }
}

10.4.2 @GuardedBy({“a”, “b”}) is not a subtype of @GuardedBy({“a”})

@GuardedBy(exprSet)

The following example demonstrates the reason the Lock Checker enforces this rule: if exprSet1 ≠ exprSet2, then @GuardedBy(exprSet1) and @GuardedBy(exprSet2) are siblings in the type hierarchy.

class MyClass {
    final Object lockA = new Object();
    final Object lockB = new Object();
    @GuardedBy("lockA") Object x = new Object();
    @GuardedBy({"lockA", "lockB"}) Object y = new Object();
    void myMethod() {
        y = x;      // ILLEGAL; if legal, later statement x.toString() would cause trouble
        synchronized(lockA) {
          x.toString(); // dereferences y's value without holding lock lockB
        }
    }
}

If the Lock Checker permitted the assignment y = x;, then the undesired dereference would be possible.

10.4.3 Examples of @Holding

The following example shows the interaction between @GuardedBy and @Holding:

    void helper1(@GuardedBy("myLock") Object a) {
      a.toString(); // ILLEGAL: the lock is not held
      synchronized(myLock) {
        a.toString(); // OK: the lock is held
      }
    }
    @Holding("myLock")
    void helper2(@GuardedBy("myLock") Object b) {
      b.toString(); // OK: the lock is held
    }
    void helper3(@GuardedBy("myLock") Object d) {
      d.toString(); // ILLEGAL: the lock is not held
    }
    void myMethod2(@GuardedBy("myLock") Object e) {
      helper1(e); // OK to pass to another routine without holding the lock
                   // (but helper1's body has an error)
      e.toString(); // ILLEGAL: the lock is not held
      synchronized (myLock) {
        helper2(e); // OK: the lock is held
        helper3(e); // OK, but helper3's body has an error
      }
    }

10.4.4 Examples of @EnsuresLockHeld and @EnsuresLockHeldIf

@EnsuresLockHeld and @EnsuresLockHeldIf are primarily intended for annotating JDK locking methods, as in:

package java.util.concurrent.locks;

class ReentrantLock {

    @EnsuresLockHeld("this")
    public void lock();

    @EnsuresLockHeldIf(expression="this", result=true)
    public boolean tryLock();

    ...
}

They can also be used to annotate user methods, particularly for higher-level lock constructs such as a Monitor, as in this simplified example:

public class Monitor {

    private final ReentrantLock lock; // Initialized in the constructor

    ...

    @EnsuresLockHeld("lock")
    public void enter() {
       lock.lock();
    }

    ...
}

10.4.5 Example of @LockingFree, @ReleasesNoLocks, and @MayReleaseLocks

@LockingFree is useful when a method does not make any use of synchronization or locks but causes other side effects (hence @SideEffectFree is not appropriate). @SideEffectFree implies @LockingFree; therefore, if both are applicable, you should only write @SideEffectFree. @ReleasesNoLocks has a weaker guarantee than @LockingFree, and @MayReleaseLocks provides no guarantees.

private Object myField;
private final ReentrantLock lock; // Initialized in the constructor
private @GuardedBy("lock") Object x; // Initialized in the constructor

[...]

// This method does not use locks or synchronization, but it cannot
// be annotated as @SideEffectFree since it alters myField.
@LockingFree
void myMethod() {
  myField = new Object();
}

@SideEffectFree
int mySideEffectFreeMethod() {
  return 0;
}

@MayReleaseLocks
void myUnlockingMethod() {
  lock.unlock();
}

@ReleasesNoLocks
void myLockingMethod() {
  lock.lock();
}

@MayReleaseLocks
void clientMethod() {
  if (lock.tryLock()) {
    x.toString(); // OK: the lock is held
    myMethod();
    x.toString(); // OK: the lock is still held since myMethod is locking-free
    mySideEffectFreeMethod();
    x.toString(); // OK: the lock is still held since mySideEffectFreeMethod is side-effect-free
    myUnlockingMethod();
    x.toString(); // ILLEGAL: myUnlockingMethod may have released a lock
  }
  if (lock.tryLock()) {
    x.toString(); // OK: the lock is held
    myLockingMethod();
    x.toString(); // OK: the lock is held
  }
  if (lock.isHeldByCurrentThread()) {
    x.toString(); // OK: the lock is known to be held
  }
}

10.4.6 Polymorphism and method formal parameters with unknown guards

The polymorphic @GuardSatisfied type annotation allows a method body to dereference the method’s formal parameters even if the @GuardedBy annotations on the actual parameters are unknown at the method declaration site.

The declaration of StringBuffer.append(String str) is annotated as:

@LockingFree
public @GuardSatisfied(1) StringBuffer append(@GuardSatisfied(1) StringBuffer this,
                                              @GuardSatisfied(2) String str)

The method manipulates the values of its arguments, so all their locks must be held. However, the declaration does not know what those locks are, and they might not even be in scope at the declaration. Therefore, the declaration cannot use @GuardedBy and must use @GuardSatisfied. The arguments to @GuardSatisfied indicate that the receiver and result (which are the same value) are guarded by the same (unknown, possibly empty) set of locks, and the str parameter may be guarded by a different set of locks.

The @LockingFree annotation indicates that this method makes no use of locks or synchronization.

Given these annotations on append, the following code type-checks:

final ReentrantLock lock1, lock2; // Initialized in the constructor
@GuardedBy("lock1") StringBuffer filename;
@GuardedBy("lock2") StringBuffer extension;
...
lock1.lock();
lock2.lock();
filename = filename.append(extension);

10.5 More locking details

This section gives some details that are helpful for understanding how Java locking and the Lock Checker work.

The paper “Locking discipline inference and checking” [ELM⁺16] (ICSE 2016, https://homes.cs.washington.edu/~mernst/pubs/locking-inference-checking-icse2016-abstract.html) gives additional details.

10.5.1 Two types of locking: monitor locks and explicit locks

Java provides two types of locking: monitor locks and explicit locks.

• A synchronized(E) block acquires the lock on the value of E; similarly, a method declared using the synchronized method modifier acquires the lock on the method receiver when called. (More precisely, the current thread locks the monitor associated with the value of E; see JLS §17.1.) The lock is automatically released when execution exits the block or the method body, respectively. We use the term “monitor lock” for a lock acquired using a synchronized block or synchronized method modifier.
• A method call, such as Lock.lock(), acquires a lock that implements the Lock interface. The lock is released by another method call, such as Lock.unlock(). We use the term “explicit lock” for a lock acquired in this way.

You should not mix the two varieties of locking, and the Lock Checker enforces this. To prevent an object from being used both as a monitor and an explicit lock, the Lock Checker issues a warning if a synchronized(E) block’s expression E has a type that implements Lock.

10.5.2 Held locks and held expressions; aliasing

Whereas Java locking is defined in terms of values, Java programs are written in terms of expressions. We say that a lock expression is held if the value to which the expression currently evaluates is held.

The Lock Checker conservatively estimates the expressions that are held at each point in a program. The Lock Checker does not track aliasing (different expressions that evaluate to the same value); it only considers the exact expression used to acquire a lock to be held. After any statement that might side-effect a held expression or a lock expression, the Lock Checker conservatively considers the expression to be no longer held.

Section 33.8 explains which Java expressions the Lock Checker is able to analyze as lock expressions.

The @LockHeld and @LockPossiblyHeld type qualifiers are used internally by the Lock Checker and should never be written by the programmer. If you see a warning mentioning @LockHeld or @LockPossiblyHeld, please contact the Checker Framework developers, as it is likely to indicate a bug in the Checker Framework.

10.5.3 Run-time checks for locking

When you perform a run-time check for locking, such as if (explicitLock.isHeldByCurrentThread()){...} or if (Thread.holdsLock(monitorLock)){...}, then the Lock Checker considers the lock expression to be held within the scope of the test. For more details, see Section 33.7.

10.5.4 Discussion of default qualifier

The default qualifier for unannotated types is @GuardedBy({}). This default forces you to write explicit @GuardSatisfied in method signatures in the common case that clients ensure that all locks are held.

It might seem that @GuardSatisfied would be a better default for method signatures, but such a default would require even more annotations. The reason is that @GuardSatisfied cannot be used on fields. If @GuardedBy({}) is the default for fields but @GuardSatisfied is the default for parameters and return types, then getters, setters, and many other types of methods do not type-check without explicit lock qualifiers.

10.5.5 Discussion of `@Holding`

A programmer might choose to use the @Holding method annotation in two different ways: to specify correctness constraints for a synchronization protocol, or to summarize intended usage. Both of these approaches are useful, and the Lock Checker supports both.

Synchronization protocol

@Holding can specify a synchronization protocol that is not expressible as locks over the parameters to a method. For example, a global lock or a lock on a different object might need to be held. By requiring locks to be held, you can create protocol primitives without giving up the benefits of the annotations and of checking them.

Method summary that simplifies reasoning

@Holding can be a method summary that simplifies reasoning. In this case, the @Holding annotation doesn’t necessarily introduce a new correctness constraint; the program might be correct even if the lock were not already acquired.

Rather, here @Holding expresses a fact about execution: when execution reaches this point, the given locks are known to be already held. This fact enables people and tools to reason intra- rather than inter-procedurally.

In Java, it is always legal to re-acquire a lock that is already held, and the re-acquisition always works. Thus, whenever you write

    @Holding("myLock")
    void myMethod() {
      ...
    }

it would be equivalent, from the point of view of which locks are held during the body, to write

    void myMethod() {
      synchronized (myLock) {     // no-op:   re-acquire a lock that is already held
        ...
      }
    }

It is better to write a @Holding annotation than to write the extra synchronized block. Here are the reasons:

• The annotation documents the fact that the lock is intended to already be held; that is, the method’s contract requires that the lock be held when the method is called.
• The Lock Checker enforces that the lock is held when the method is called, rather than masking a programmer error by silently re-acquiring the lock.
• The version with a synchronized statement can deadlock if, due to a programmer error, the lock is not already held. The Lock Checker prevents this type of error.
• The annotation has no run-time overhead. The lock re-acquisition consumes time, even when it succeeds.

10.6 Other lock annotations

The Checker Framework’s lock annotations are similar to annotations used elsewhere.

If your code is already annotated with a different lock annotation, the Checker Framework can type-check your code. It treats annotations from other tools as if you had written the corresponding annotation from the Lock Checker, as described in Figure 10.2. If the other annotation is a declaration annotation, it may be moved; see Section 40.6.10.

net.jcip.annotations.GuardedBy

javax.annotation.concurrent.GuardedBy

⇒

org.checkerframework.checker.lock.qual.GuardedBy (for fields), or

org.checkerframework.checker.lock.qual.Holding (for methods)

Figure 10.2: Correspondence between other lock annotations and the Checker Framework’s annotations.

10.6.1 Relationship to annotations in Java Concurrency in Practice

The book Java Concurrency in Practice [GPB⁺06] defines a @GuardedBy annotation that is the inspiration for ours. The book’s @GuardedBy serves two related but distinct purposes:

• When applied to a field, it means that the given lock must be held when accessing the field. The lock acquisition and the field access may occur arbitrarily far in the future.
• When applied to a method, it means that the given lock must be held by the caller at the time that the method is called — in other words, at the time that execution passes the @GuardedBy annotation.

The Lock Checker renames the method annotation to @Holding, and it generalizes the @GuardedBy annotation into a type annotation that can apply not just to a field but to an arbitrary type (including the type of a parameter, return value, local variable, generic type parameter, etc.). Another important distinction is that the Lock Checker’s annotations express and enforce a locking discipline over values, just as the JLS expresses Java’s locking semantics; by contrast, JCIP’s annotations express a locking discipline that protects variable names and does not prevent race conditions. This makes the annotations more expressive and also more amenable to automated checking. It also accommodates the distinct meanings of the two annotations, and resolves ambiguity when @GuardedBy is written in a location that might apply to either the method or the return type.

(The JCIP book gives some rationales for reusing the annotation name for two purposes. One rationale is that there are fewer annotations to learn. Another rationale is that both variables and methods are “members” that can be “accessed” and @GuardedBy creates preconditions for doing so. Variables can be accessed by reading or writing them (putfield, getfield), and methods can be accessed by calling them (invokevirtual, invokeinterface). This informal intuition is inappropriate for a tool that requires precise semantics.)

10.7 Possible extensions

The Lock Checker validates some uses of locks, but not all. It would be possible to enrich it with additional annotations. This would increase the programmer annotation burden, but would provide additional guarantees.

Lock ordering: Specify that one lock must be acquired before or after another, or specify a global ordering for all locks. This would prevent deadlock.

Not-holding: Specify that a method must not be called if any of the listed locks are held.

These features are supported by Clang’s thread-safety analysis.

The Checker Framework Manual: Custom pluggable types for Java