0
# Concurrency Annotations
1

2
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.
3

4
## Capabilities
5

6
### Lock Protection Annotations
7

8
Annotations that specify which locks protect shared resources.
9

10
```java { .api }
11
/**
12
 * Indicates that the annotated expression is protected by the specified locks
13
 */
14
@Documented
15
@Retention(RetentionPolicy.RUNTIME)
16
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
17
@SubtypeOf(GuardedByUnknown.class)
18
public @interface GuardedBy {
19
    String[] value();
20
}
21

22
/**
23
 * Indicates that the guard is satisfied (lock is held)
24
 */
25
@Documented
26
@Retention(RetentionPolicy.RUNTIME)
27
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
28
@SubtypeOf(GuardedBy.class)
29
public @interface GuardSatisfied {}
30

31
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
32
@SubtypeOf(GuardedBy.class)
33
public @interface GuardedByBottom {}
34

35
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
36
@DefaultQualifierInHierarchy
37
public @interface GuardedByUnknown {}
38

39
/**
40
 * Polymorphic guard qualifier
41
 */
42
@Documented
43
@Retention(RetentionPolicy.RUNTIME)
44
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
45
@PolymorphicQualifier(GuardedByUnknown.class)
46
public @interface PolyGuardedBy {}
47
```
48

49
**Usage Examples:**
50

51
```java
52
import org.checkerframework.checker.lock.qual.*;
53

54
public class GuardedExample {
55
    private final Object lock = new Object();
56
    private @GuardedBy("lock") int counter = 0;
57
    private @GuardedBy("this") String name;
58
    
59
    public synchronized void setName(String newName) {
60
        this.name = newName; // Safe - synchronized method holds "this" lock
61
    }
62
    
63
    public void increment() {
64
        synchronized (lock) {
65
            counter++; // Safe - lock is held
66
        }
67
    }
68
    
69
    public int getCounter() {
70
        synchronized (lock) {
71
            return counter; // Safe - lock protects read access too
72
        }
73
    }
74
    
75
    // Method that works with any guarded value
76
    public @PolyGuardedBy int process(@PolyGuardedBy int value) {
77
        return value * 2; // Preserves guard requirements
78
    }
79
}
80
```
81

82
### Lock State Annotations
83

84
Annotations that track whether locks are currently held.
85

86
```java { .api }
87
/**
88
 * Indicates that the specified lock is currently held
89
 */
90
@Documented
91
@Retention(RetentionPolicy.RUNTIME)
92
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
93
public @interface LockHeld {}
94

95
/**
96
 * Indicates that the specified lock may or may not be held
97
 */
98
@Documented
99
@Retention(RetentionPolicy.RUNTIME)
100
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
101
public @interface LockPossiblyHeld {}
102
```
103

104
**Usage Examples:**
105

106
```java
107
import org.checkerframework.checker.lock.qual.*;
108

109
public class LockStateExample {
110
    private final Object lock = new Object();
111
    private @GuardedBy("lock") int value = 0;
112
    
113
    @Holding("lock")
114
    public void updateValueWhileHeld(int newValue) {
115
        // This method requires that 'lock' is already held
116
        this.value = newValue; // Safe - precondition ensures lock is held
117
    }
118
    
119
    public void safeUpdate(int newValue) {
120
        synchronized (lock) {
121
            updateValueWhileHeld(newValue); // Safe - lock is held here
122
        }
123
    }
124
}
125
```
126

127
### Method-Level Lock Annotations
128

129
Annotations that specify lock requirements and effects for methods.
130

131
```java { .api }
132
/**
133
 * Method requires that the specified locks are held when called
134
 */
135
@Documented
136
@Retention(RetentionPolicy.RUNTIME)
137
@Target(ElementType.METHOD)
138
@InheritedAnnotation
139
public @interface Holding {
140
    String[] value();
141
}
142

143
/**
144
 * Method releases no locks during execution
145
 */
146
@Documented
147
@Retention(RetentionPolicy.RUNTIME)
148
@Target(ElementType.METHOD)
149
public @interface ReleasesNoLocks {}
150

151
/**
152
 * Method may release locks during execution
153
 */
154
@Documented
155
@Retention(RetentionPolicy.RUNTIME)
156
@Target(ElementType.METHOD)
157
public @interface MayReleaseLocks {}
158

159
/**
160
 * Method performs no locking operations
161
 */
162
@Documented
163
@Retention(RetentionPolicy.RUNTIME)
164
@Target(ElementType.METHOD)
165
public @interface LockingFree {}
166
```
167

168
**Usage Examples:**
169

170
```java
171
import org.checkerframework.checker.lock.qual.*;
172

173
public class MethodLockExample {
174
    private final Object lock1 = new Object();
175
    private final Object lock2 = new Object();
176
    private @GuardedBy("lock1") int value1 = 0;
177
    private @GuardedBy("lock2") int value2 = 0;
178
    
179
    @Holding({"lock1", "lock2"})
180
    public void transferValue() {
181
        // Requires both locks to be held
182
        int temp = value1;
183
        value1 = value2;
184
        value2 = temp;
185
    }
186
    
187
    @ReleasesNoLocks
188
    public int computeSum() {
189
        // Method promises not to release any locks
190
        synchronized (lock1) {
191
            synchronized (lock2) {
192
                return value1 + value2; // Locks remain held throughout
193
            }
194
        }
195
    }
196
    
197
    @MayReleaseLocks
198
    public void processWithCallback(Runnable callback) {
199
        synchronized (lock1) {
200
            callback.run(); // Callback might release locks
201
        }
202
    }
203
    
204
    @LockingFree
205
    public int pureComputation(int a, int b) {
206
        // No locking operations performed
207
        return a * b + 42;
208
    }
209
    
210
    public void safeTransfer() {
211
        synchronized (lock1) {
212
            synchronized (lock2) {
213
                transferValue(); // Safe - both required locks are held
214
            }
215
        }
216
    }
217
}
218
```
219

220
### Object Creation and Escape Analysis
221

222
Annotations for tracking object creation and preventing premature sharing.
223

224
```java { .api }
225
/**
226
 * Indicates a newly created object that has not escaped the current thread
227
 */
228
@Documented
229
@Retention(RetentionPolicy.RUNTIME)
230
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
231
public @interface NewObject {}
232
```
233

234
**Usage Examples:**
235

236
```java
237
import org.checkerframework.checker.lock.qual.*;
238

239
public class ObjectCreationExample {
240
    private final Object lock = new Object();
241
    private @GuardedBy("lock") List<String> items = new ArrayList<>();
242
    
243
    public @NewObject List<String> createList() {
244
        // Return value is a new object, not yet shared
245
        return new ArrayList<>();
246
    }
247
    
248
    public void addNewItems() {
249
        @NewObject List<String> newItems = createList();
250
        newItems.add("item1"); // Safe - object not yet shared
251
        newItems.add("item2");
252
        
253
        // Now share the object safely
254
        synchronized (lock) {
255
            items.addAll(newItems); // Safe - lock protects shared state
256
        }
257
    }
258
}
259
```
260

261
### Lock Contract Annotations
262

263
Annotations for specifying lock-related method contracts.
264

265
```java { .api }
266
/**
267
 * Method postcondition: ensures the specified locks are held after method execution
268
 */
269
@Target(ElementType.METHOD)
270
@Retention(RetentionPolicy.RUNTIME)
271
@InheritedAnnotation
272
public @interface EnsuresLockHeld {
273
    String[] value();
274
}
275

276
/**
277
 * Conditional method postcondition: ensures locks are held if method returns specified result
278
 */
279
@Target(ElementType.METHOD)
280
@Retention(RetentionPolicy.RUNTIME)
281
@InheritedAnnotation
282
public @interface EnsuresLockHeldIf {
283
    String[] expression();
284
    boolean result();
285
}
286
```
287

288
**Usage Examples:**
289

290
```java
291
import org.checkerframework.checker.lock.qual.*;
292

293
public class LockContractExample {
294
    private final ReentrantLock lock = new ReentrantLock();
295
    private @GuardedBy("lock") String data;
296
    
297
    @EnsuresLockHeld("lock")
298
    public void acquireLock() {
299
        lock.lock(); // Postcondition ensures lock is held
300
    }
301
    
302
    @EnsuresLockHeldIf(expression = "lock", result = true)
303
    public boolean tryAcquireLock() {
304
        return lock.tryLock(); // If returns true, lock is held
305
    }
306
    
307
    public void safeDataAccess() {
308
        acquireLock();
309
        try {
310
            // Safe - postcondition ensures lock is held
311
            data = "new value";
312
            System.out.println(data);
313
        } finally {
314
            lock.unlock();
315
        }
316
    }
317
    
318
    public void conditionalAccess() {
319
        if (tryAcquireLock()) {
320
            try {
321
                // Safe - conditional postcondition ensures lock is held
322
                data = "conditional value";
323
                System.out.println(data);
324
            } finally {
325
                lock.unlock();
326
            }
327
        } else {
328
            System.out.println("Could not acquire lock");
329
        }
330
    }
331
}
332
```
333

334
### Advanced Concurrency Patterns
335

336
Examples of complex concurrency patterns using the lock annotations.
337

338
**Producer-Consumer Pattern:**
339

340
```java
341
import org.checkerframework.checker.lock.qual.*;
342
import java.util.concurrent.BlockingQueue;
343
import java.util.concurrent.LinkedBlockingQueue;
344

345
public class ProducerConsumerExample {
346
    private final Object stateLock = new Object();
347
    private @GuardedBy("stateLock") boolean running = true;
348
    private final BlockingQueue<String> queue = new LinkedBlockingQueue<>();
349
    
350
    @Holding("stateLock")
351
    private void checkRunning() {
352
        if (!running) {
353
            throw new IllegalStateException("System is stopped");
354
        }
355
    }
356
    
357
    public void produce(String item) {
358
        synchronized (stateLock) {
359
            checkRunning(); // Safe - lock is held
360
        }
361
        
362
        try {
363
            queue.put(item); // BlockingQueue is thread-safe
364
        } catch (InterruptedException e) {
365
            Thread.currentThread().interrupt();
366
        }
367
    }
368
    
369
    public String consume() {
370
        synchronized (stateLock) {
371
            checkRunning(); // Safe - lock is held
372
        }
373
        
374
        try {
375
            return queue.take(); // BlockingQueue is thread-safe
376
        } catch (InterruptedException e) {
377
            Thread.currentThread().interrupt();
378
            return null;
379
        }
380
    }
381
    
382
    public void stop() {
383
        synchronized (stateLock) {
384
            running = false; // Safe - lock protects shared state
385
        }
386
    }
387
}
388
```
389

390
**Reader-Writer Pattern:**
391

392
```java
393
import org.checkerframework.checker.lock.qual.*;
394
import java.util.concurrent.locks.ReadWriteLock;
395
import java.util.concurrent.locks.ReentrantReadWriteLock;
396

397
public class ReaderWriterExample {
398
    private final ReadWriteLock rwLock = new ReentrantReadWriteLock();
399
    private @GuardedBy("rwLock") String data = "initial";
400
    
401
    @Holding("rwLock.readLock()")
402
    public String readData() {
403
        return data; // Safe - read lock protects access
404
    }
405
    
406
    @Holding("rwLock.writeLock()")
407
    public void writeData(String newData) {
408
        this.data = newData; // Safe - write lock protects access
409
    }
410
    
411
    public String safeRead() {
412
        rwLock.readLock().lock();
413
        try {
414
            return readData(); // Safe - read lock is held
415
        } finally {
416
            rwLock.readLock().unlock();
417
        }
418
    }
419
    
420
    public void safeWrite(String newData) {
421
        rwLock.writeLock().lock();
422
        try {
423
            writeData(newData); // Safe - write lock is held
424
        } finally {
425
            rwLock.writeLock().unlock();
426
        }
427
    }
428
}
429
```