By 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:
- State the linearization point (e.g., "CAS on CHM bin at line X").
- If conditional, enumerate all cases.
- 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?
- Is size() linearizable or documented as an estimate? Bounds on error?
- 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.