audit-linearizability

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
• For a time-based violation (an entry expiring early or late), include a thread that observes the key inside the window. Without one, the operation can linearize anywhere in its interval, including at its own clock read, and the history is legal. Exclude the configurations that allow other removals (a size bound, weak or soft references), since they also explain a miss.

Do not analyze internal consistency, only external observability.