Audit the following subsystem for correctness defects: $ARGUMENTS
Subsystem scopes (if no argument given, audit ALL subsystems one at a time):
- Eviction path: evictFromMain, evictFromWindow, evictEntry, makeDead, resurrection
- Refresh path: refreshIfNeeded, tryRefresh, doRefreshIfNeeded, afterRefreshCompletion
- Write buffer: afterWrite, AddTask, UpdateTask, RemovalTask, drainWriteBuffer
- Compute path: doComputeIfAbsent, remap, and their interaction with CHM compute lambdas
- Expiration path: expireEntries, hasExpired, timer wheel scheduling, Pacer
- Reference collection: referenceKey, referenceValue, cleanUpReferences
- Read path: getIfPresent, afterRead, read buffer, frequency sketch updates
DO NOT analyze code outside your scope unless it is directly called by your scoped methods.
Key cross-cutting invariants your subsystem must preserve:
- Node lifecycle is unidirectional: alive -> retired -> dead (never reversed)
- Weight accounting: weightedSize must converge to the sum of weights of
live entries, regardless of task ordering in the write buffer
- Lock ordering: evictionLock -> CHM bin lock -> synchronized(node)
- The value field on a node uses acquire/release semantics; the key
reference is immutable after construction (plain read is safe)
For each method in your scope:
- List every shared mutable field it reads or writes, and the access mode
(plain, opaque, acquire, release, volatile, synchronized, CAS).
- List every lock held at each access point.
- For every pair of (write in method A, read in method B) within your scope,
state whether a happens-before edge exists. If it depends on a condition,
state the condition.
- Attempt to construct a 2-thread or 3-thread interleaving that violates
a postcondition of any method in your scope. Pay particular attention
to interleavings where a node transitions between lifecycle states
(e.g., retirement during an in-progress update).
For each candidate defect:
- Provide the concrete interleaving (thread actions interleaved step-by-step)
- State the invariant violated
- State the observable incorrect behavior
- Verify your interleaving is legal under the JMM (not just sequentially consistent)
If no defects are found, output the invariants that are preserved and WHY
(which synchronization mechanism protects each one).
Do not provide praise, style suggestions, or performance observations.
1---2name: audit-subsystem-safety3description: Audit one cache subsystem for concurrency correctness defects4---56Audit the following subsystem for correctness defects: $ARGUMENTS78Subsystem scopes (if no argument given, audit ALL subsystems one at a time):9- Eviction path: evictFromMain, evictFromWindow, evictEntry, makeDead, resurrection10- Refresh path: refreshIfNeeded, tryRefresh, doRefreshIfNeeded, afterRefreshCompletion11- Write buffer: afterWrite, AddTask, UpdateTask, RemovalTask, drainWriteBuffer12- Compute path: doComputeIfAbsent, remap, and their interaction with CHM compute lambdas13- Expiration path: expireEntries, hasExpired, timer wheel scheduling, Pacer14- Reference collection: referenceKey, referenceValue, cleanUpReferences15- Read path: getIfPresent, afterRead, read buffer, frequency sketch updates1617DO NOT analyze code outside your scope unless it is directly called by your scoped methods.1819Key cross-cutting invariants your subsystem must preserve:20- Node lifecycle is unidirectional: alive -> retired -> dead (never reversed)21- Weight accounting: weightedSize must converge to the sum of weights of22 live entries, regardless of task ordering in the write buffer23- Lock ordering: evictionLock -> CHM bin lock -> synchronized(node)24- The value field on a node uses acquire/release semantics; the key25 reference is immutable after construction (plain read is safe)2627For each method in your scope:28291. List every shared mutable field it reads or writes, and the access mode30 (plain, opaque, acquire, release, volatile, synchronized, CAS).312. List every lock held at each access point.323. For every pair of (write in method A, read in method B) within your scope,33 state whether a happens-before edge exists. If it depends on a condition,34 state the condition.354. Attempt to construct a 2-thread or 3-thread interleaving that violates36 a postcondition of any method in your scope. Pay particular attention37 to interleavings where a node transitions between lifecycle states38 (e.g., retirement during an in-progress update).3940For each candidate defect:41- Provide the concrete interleaving (thread actions interleaved step-by-step)42- State the invariant violated43- State the observable incorrect behavior44- Verify your interleaving is legal under the JMM (not just sequentially consistent)4546If no defects are found, output the invariants that are preserved and WHY47(which synchronization mechanism protects each one).4849Do not provide praise, style suggestions, or performance observations.
ben-manes