What linearizability means
An object is linearizable if every concurrent operation appears to take effect instantly at some point between its call and return, and the resulting order matches a legal sequential history.
What a checker does
A linearizability checker records a history of operation calls and returns with timestamps, then searches for a sequential ordering that:
- respects real time, so an operation that returned before another began comes first
- matches a correct sequential specification of the object
If such an ordering exists the history is linearizable.
Why it is hard
The number of candidate orderings grows fast with concurrent operations, so checkers prune aggressively and may limit history length. They confirm violations precisely but get slow on large histories.
Key idea
A linearizability checker proves a concurrent history equivalent to some real time respecting sequential order that obeys the object specification, or reports that none exists.