audit-linearizability

---
name: audit-linearizability
description: Analyze the cache for linearizability violations across all public methods
context: fork
agent: auditor
disable-model-invocation: true
---

Analyze the cache for linearizability violations. For each public method below,
identify its LINEARIZATION POINT — the single atomic step at which the operation
appears to take effect.

Methods to analyze:

Single-key operations:
- get(key), getIfPresent(key)
- put(key, value), putIfAbsent(key, value)
- remove(key), remove(key, value)
- replace(key, value), replace(key, oldValue, newValue)
- computeIfAbsent(key, function), compute(key, function), merge(key, value, function)

Bulk / aggregate operations:
- getAll(keys) / getAllPresent(keys)
- putAll(map)
- invalidateAll(keys) / invalidateAll()
- size(), containsKey(key), containsValue(value)

Note: Bulk operations are typically NOT linearizable as a unit. State whether each
provides any atomicity beyond per-element linearizability.

For each method:
1. State the linearization point (e.g., "CAS on CHM bin at line X").
2. If conditional, enumerate all cases.
3. Construct a 2-thread scenario confirming the linearization point.

Then attempt to construct violations:
4. Can two threads observe operations in an inconsistent order?
   - put(k, v1) / put(k, v2) / get(k): Can C see v2 then v1?
   - computeIfAbsent(k, f): Can f execute twice concurrently?
   - remove(k) / get(k): Can get return a value after remove linearized?
5. Is size() linearizable or documented as an estimate? Bounds on error?
6. For async cache variants: is the linearization point the future insertion
   or completion? Can get() return an already-replaced future?

For each candidate violation:
- Provide the full interleaving
- Show the sequential history it violates
- Verify the interleaving is JMM-legal

Do not analyze internal consistency, only external observability.