tessl/maven-org-checkerframework--checker-qual
Type qualifier annotations for the Checker Framework static analysis tool
—
Pending
concurrency.mddocs/
Concurrency Annotations
Concurrency annotations provide thread safety analysis and lock-based synchronization checking. These annotations help prevent data races, deadlocks, and other concurrency-related errors by tracking lock states and thread safety properties.
Capabilities
Lock Protection Annotations
Annotations that specify which locks protect shared resources.
/**
* Indicates that the annotated expression is protected by the specified locks
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(GuardedByUnknown.class)
public @interface GuardedBy {
String[] value();
}
/**
* Indicates that the guard is satisfied (lock is held)
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(GuardedBy.class)
public @interface GuardSatisfied {}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(GuardedBy.class)
public @interface GuardedByBottom {}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@DefaultQualifierInHierarchy
public @interface GuardedByUnknown {}
/**
* Polymorphic guard qualifier
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(GuardedByUnknown.class)
public @interface PolyGuardedBy {}Usage Examples:
import org.checkerframework.checker.lock.qual.*;
public class GuardedExample {
private final Object lock = new Object();
private @GuardedBy("lock") int counter = 0;
private @GuardedBy("this") String name;
public synchronized void setName(String newName) {
this.name = newName; // Safe - synchronized method holds "this" lock
}
public void increment() {
synchronized (lock) {
counter++; // Safe - lock is held
}
}
public int getCounter() {
synchronized (lock) {
return counter; // Safe - lock protects read access too
}
}
// Method that works with any guarded value
public @PolyGuardedBy int process(@PolyGuardedBy int value) {
return value * 2; // Preserves guard requirements
}
}Lock State Annotations
Annotations that track whether locks are currently held.
/**
* Indicates that the specified lock is currently held
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface LockHeld {}
/**
* Indicates that the specified lock may or may not be held
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface LockPossiblyHeld {}Usage Examples:
import org.checkerframework.checker.lock.qual.*;
public class LockStateExample {
private final Object lock = new Object();
private @GuardedBy("lock") int value = 0;
@Holding("lock")
public void updateValueWhileHeld(int newValue) {
// This method requires that 'lock' is already held
this.value = newValue; // Safe - precondition ensures lock is held
}
public void safeUpdate(int newValue) {
synchronized (lock) {
updateValueWhileHeld(newValue); // Safe - lock is held here
}
}
}Method-Level Lock Annotations
Annotations that specify lock requirements and effects for methods.
/**
* Method requires that the specified locks are held when called
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
@InheritedAnnotation
public @interface Holding {
String[] value();
}
/**
* Method releases no locks during execution
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface ReleasesNoLocks {}
/**
* Method may release locks during execution
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface MayReleaseLocks {}
/**
* Method performs no locking operations
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface LockingFree {}Usage Examples:
import org.checkerframework.checker.lock.qual.*;
public class MethodLockExample {
private final Object lock1 = new Object();
private final Object lock2 = new Object();
private @GuardedBy("lock1") int value1 = 0;
private @GuardedBy("lock2") int value2 = 0;
@Holding({"lock1", "lock2"})
public void transferValue() {
// Requires both locks to be held
int temp = value1;
value1 = value2;
value2 = temp;
}
@ReleasesNoLocks
public int computeSum() {
// Method promises not to release any locks
synchronized (lock1) {
synchronized (lock2) {
return value1 + value2; // Locks remain held throughout
}
}
}
@MayReleaseLocks
public void processWithCallback(Runnable callback) {
synchronized (lock1) {
callback.run(); // Callback might release locks
}
}
@LockingFree
public int pureComputation(int a, int b) {
// No locking operations performed
return a * b + 42;
}
public void safeTransfer() {
synchronized (lock1) {
synchronized (lock2) {
transferValue(); // Safe - both required locks are held
}
}
}
}Object Creation and Escape Analysis
Annotations for tracking object creation and preventing premature sharing.
/**
* Indicates a newly created object that has not escaped the current thread
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface NewObject {}Usage Examples:
import org.checkerframework.checker.lock.qual.*;
public class ObjectCreationExample {
private final Object lock = new Object();
private @GuardedBy("lock") List<String> items = new ArrayList<>();
public @NewObject List<String> createList() {
// Return value is a new object, not yet shared
return new ArrayList<>();
}
public void addNewItems() {
@NewObject List<String> newItems = createList();
newItems.add("item1"); // Safe - object not yet shared
newItems.add("item2");
// Now share the object safely
synchronized (lock) {
items.addAll(newItems); // Safe - lock protects shared state
}
}
}Lock Contract Annotations
Annotations for specifying lock-related method contracts.
/**
* Method postcondition: ensures the specified locks are held after method execution
*/
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresLockHeld {
String[] value();
}
/**
* Conditional method postcondition: ensures locks are held if method returns specified result
*/
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresLockHeldIf {
String[] expression();
boolean result();
}Usage Examples:
import org.checkerframework.checker.lock.qual.*;
public class LockContractExample {
private final ReentrantLock lock = new ReentrantLock();
private @GuardedBy("lock") String data;
@EnsuresLockHeld("lock")
public void acquireLock() {
lock.lock(); // Postcondition ensures lock is held
}
@EnsuresLockHeldIf(expression = "lock", result = true)
public boolean tryAcquireLock() {
return lock.tryLock(); // If returns true, lock is held
}
public void safeDataAccess() {
acquireLock();
try {
// Safe - postcondition ensures lock is held
data = "new value";
System.out.println(data);
} finally {
lock.unlock();
}
}
public void conditionalAccess() {
if (tryAcquireLock()) {
try {
// Safe - conditional postcondition ensures lock is held
data = "conditional value";
System.out.println(data);
} finally {
lock.unlock();
}
} else {
System.out.println("Could not acquire lock");
}
}
}Advanced Concurrency Patterns
Examples of complex concurrency patterns using the lock annotations.
Producer-Consumer Pattern:
import org.checkerframework.checker.lock.qual.*;
import java.util.concurrent.BlockingQueue;
import java.util.concurrent.LinkedBlockingQueue;
public class ProducerConsumerExample {
private final Object stateLock = new Object();
private @GuardedBy("stateLock") boolean running = true;
private final BlockingQueue<String> queue = new LinkedBlockingQueue<>();
@Holding("stateLock")
private void checkRunning() {
if (!running) {
throw new IllegalStateException("System is stopped");
}
}
public void produce(String item) {
synchronized (stateLock) {
checkRunning(); // Safe - lock is held
}
try {
queue.put(item); // BlockingQueue is thread-safe
} catch (InterruptedException e) {
Thread.currentThread().interrupt();
}
}
public String consume() {
synchronized (stateLock) {
checkRunning(); // Safe - lock is held
}
try {
return queue.take(); // BlockingQueue is thread-safe
} catch (InterruptedException e) {
Thread.currentThread().interrupt();
return null;
}
}
public void stop() {
synchronized (stateLock) {
running = false; // Safe - lock protects shared state
}
}
}Reader-Writer Pattern:
import org.checkerframework.checker.lock.qual.*;
import java.util.concurrent.locks.ReadWriteLock;
import java.util.concurrent.locks.ReentrantReadWriteLock;
public class ReaderWriterExample {
private final ReadWriteLock rwLock = new ReentrantReadWriteLock();
private @GuardedBy("rwLock") String data = "initial";
@Holding("rwLock.readLock()")
public String readData() {
return data; // Safe - read lock protects access
}
@Holding("rwLock.writeLock()")
public void writeData(String newData) {
this.data = newData; // Safe - write lock protects access
}
public String safeRead() {
rwLock.readLock().lock();
try {
return readData(); // Safe - read lock is held
} finally {
rwLock.readLock().unlock();
}
}
public void safeWrite(String newData) {
rwLock.writeLock().lock();
try {
writeData(newData); // Safe - write lock is held
} finally {
rwLock.writeLock().unlock();
}
}
}Install with Tessl CLI
npx tessl i tessl/maven-org-checkerframework--checker-qual