Editing Linearizability (section)

== Definition ==
A concurrent system consists of a collection of processes communicating through shared data structures or objects. Linearizability is important in these concurrent systems where objects may be accessed by multiple processes at the same time and a programmer needs to be able to reason about the expected results. An execution of a concurrent system results in a ''history'', an ordered sequence of completed operations.

A ''history'' is a sequence of ''invocations'' and ''responses'' made of an object by a set of [[Thread (computer science)|threads]] or processes. An invocation can be thought of as the start of an operation, and the response being the signaled end of that operation. Each invocation of a function will have a subsequent response. This can be used to model any use of an object. Suppose, for example, that two threads, A and B, both attempt to grab a lock, backing off if it's already taken. This would be modeled as both threads invoking the lock operation, then both threads receiving a response, one successful, one not.

{| border="1" cellspacing="0"
| A invokes ''lock''
| B invokes ''lock''
| A gets "failed" response
| B gets "successful" response
|}

A ''sequential'' history is one in which all invocations have immediate responses; that is the invocation and response are considered to take place instantaneously. A sequential history should be trivial to reason about, as it has no real concurrency; the previous example was not sequential, and thus is hard to reason about. This is where linearizability comes in.

A history is ''linearizable'' if there is a linear order <math>\sigma</math> of the completed operations such that:
# For every completed operation in <math>\sigma</math>, the operation returns the same result in the execution as the operation would return if every operation was completed one by one in order <math>\sigma</math>.
# If an operation op<sub>1</sub> completes (gets a response) before op<sub>2</sub> begins (invokes), then op<sub>1</sub> precedes op<sub>2</sub> in <math>\sigma</math>.<ref name=":0">{{Cite journal|author1=Herlihy, Maurice P.  |author2=Wing, Jeannette M.|year=1990|title=Linearizability: A Correctness Condition for Concurrent Objects|journal=ACM Transactions on Programming Languages and Systems|volume=12| issue = 3|pages=463–492|doi=10.1145/78969.78972|citeseerx=10.1.1.142.5315|s2cid=228785}}</ref>
In other words:
* its invocations and responses can be reordered to yield a sequential history;
* that sequential history is correct according to the sequential definition of the object;
* if a response preceded an invocation in the original history, it must still precede it in the sequential reordering.

Note that the first two bullet points here match [[serializability]]: the operations appear to happen in some order. It is the last point which is unique to linearizability, and is thus the major contribution of Herlihy and Wing.<ref name=":0" />

Consider two ways of reordering the locking example above.

{| border="1" cellspacing="0"
| A invokes ''lock''
| A gets "failed" response
| B invokes ''lock''
| B gets "successful" response
|}

Reordering B's invocation after A's response yields a sequential history. This is easy to reason about, as all operations now happen in an obvious order. However, it does not match the sequential definition of the object (it doesn't match the semantics of the program): A should have successfully obtained the lock, and B should have subsequently aborted.

{| border="1" cellspacing="0"
| B invokes ''lock''
| B gets "successful" response
| A invokes ''lock''
| A gets "failed" response
|}

This is another correct sequential history. It is also a linearization since it matches the sequential definition. Note that the definition of linearizability only precludes responses that precede invocations from being reordered; since the original history had no responses before invocations, they can be reordered. Hence the original history is indeed linearizable.

An object (as opposed to a history) is linearizable if all valid histories of its use can be linearized. This is a much harder assertion to prove.

=== Linearizability versus serializability ===
Consider the following history, again of two objects interacting with a lock:

{| border="1" cellspacing="0"
| A invokes lock
| A successfully locks
| B invokes unlock
| B successfully unlocks
| A invokes unlock
| A successfully unlocks
|}

This history is not valid because there is a point at which both A and B hold the lock; moreover, it cannot be reordered to a valid sequential history without violating the ordering rule. Therefore, it is not linearizable. However, under serializability, B's unlock operation may be moved to ''before'' A's original lock, which is a valid history (assuming the object begins the history in a locked state):

{| border="1" cellspacing="0"
| B invokes unlock
| B successfully unlocks
| A invokes lock
| A successfully locks
| A invokes unlock
| A successfully unlocks
|}

This reordering is sensible provided there is no alternative means of communicating between A and B. Linearizability is better when considering individual objects separately, as the reordering restrictions ensure that multiple linearizable objects are, considered as a whole, still linearizable.

=== Linearization points ===
This definition of linearizability is equivalent to the following:
* All function calls have a ''linearization point'' at some instant between their invocation and their response.
* All functions appear to occur instantly at their linearization point, behaving as specified by the sequential definition.

This alternative is usually much easier to prove. It is also much easier to reason about as a user, largely due to its intuitiveness. This property of occurring instantaneously, or indivisibly, leads to the use of the term ''atomic'' as an alternative to the longer "linearizable".<ref name=":0" />

In the examples below, the linearization point of the counter built on compare-and-swap is the linearization point of the first (and only) successful compare-and-swap update. The counter built using locking can be considered to linearize at any moment while the locks are held, since any potentially conflicting operations are excluded from running during that period.