History
Linearizability was first introduced as a consistency model by Herlihy andDefinition
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 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. 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 of the completed operations such that: # For every completed operation in , the operation returns the same result in the execution as the operation would return if every operation was completed one by one in order . # If an operation op1 completes (gets a response) before op2 begins (invokes), then op1 precedes op2 in . 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. Consider two ways of reordering the locking example above. 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. 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: 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): 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". 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.Primitive atomic instructions
Processors have instructions that can be used to implement locking and lock-free and wait-free algorithms. The ability to temporarily inhibitsig_atomic_t
for simple atomic reads and writes; incrementing or decrementing is not guaranteed to be atomic. More complex atomic operations are available in C11, which provides stdatomic.h
. Compilers use the hardware features or more complex methods to implement the operations; an example is libatomic of GCC.
The ARM instruction set provides LDREX
and STREX
instructions which can be used to implement atomic memory access by using exclusive monitors implemented in the processor to track memory accesses for a specific address. However, if a context switch occurs between calls to LDREX
and STREX
, the documentation notes that STREX
will fail, indicating the operation should be retried. In the case of 64-bit ARMv8-A architecture, it provides LDXR
and STXR
instructions for byte, half-word, word, and double-word size.
High-level atomic operations
The easiest way to achieve linearizability is running groups of primitive operations in a critical section. Strictly, independent operations can then be carefully permitted to overlap their critical sections, provided this does not violate linearizability. Such an approach must balance the cost of large numbers of locks against the benefits of increased parallelism. Another approach, favoured by researchers (but not yet widely used in the software industry), is to design a linearizable object using the native atomic primitives provided by the hardware. This has the potential to maximise available parallelism and minimise synchronisation costs, but requires mathematical proofs which show that the objects behave correctly. A promising hybrid of these two is to provide aExamples
Counters
To demonstrate the power and necessity of linearizability we will consider a simple counter which different processes can increment. We would like to implement a counter object which multiple processes can access. Many common systems make use of counters to keep track of the number of times an event has occurred. The counter object can be accessed by multiple processes and has two available operations. # Increment - adds 1 to the value stored in the counter, return acknowledgement # Read - returns the current value stored in the counter without changing it. We will attempt to implement this counter object using shared registers. Our first attempt which we will see is non-linearizable has the following implementation using one shared register among the processes.Non-atomic
The naive, non-atomic implementation: Increment: # Read the value in the register R # Add one to the value # Writes the new value back into register R Read: Read register R This simple implementation is not linearizable, as is demonstrated by the following example. Imagine two processes are running accessing the single counter object initialized to have value 0: # The first process reads the value in the register as 0. # The first process adds one to the value, the counter's value should be 1, but before it has finished writing the new value back to the register it may become suspended, meanwhile the second process is running: # The second process reads the value in the register, which is still equal to 0; # The second process adds one to the value; # The second process writes the new value into the register, the register now has value 1. The second process is finished running and the first process continues running from where it left off: # The first process writes 1 into the register, unaware that the other process has already updated the value in the register to 1. In the above example, two processes invoked an increment command, however the value of the object only increased from 0 to 1, instead of 2 as it should have. One of the increment operations was lost as a result of the system not being linearizable. The above example shows the need for carefully thinking through implementations of data structures and how linearizability can have an effect on the correctness of the system.Atomic
To implement a linearizable or atomic counter object we will modify our previous implementation so each process Pi will use its own register Ri Each process increments and reads according to the following algorithm: Increment: # Read value in register Ri. # Add one to the value. # Write new value back into Ri Read: # Read registers R1, R2, ... Rn. # Return the sum of all registers. This implementation solves the problem with our original implementation. In this system the increment operations are linearized at the write step. The linearization point of an increment operation is when that operation writes the new value in its register Ri. The read operations are linearized to a point in the system when the value returned by the read is equal to the sum of all the values stored in each register Ri. This is a trivial example. In a real system, the operations can be more complex and the errors introduced extremely subtle. For example, reading a 64-bit value from memory may actually be implemented as two sequential reads of twoCompare-and-swap
Most systems provide an atomic compare-and-swap instruction that reads from a memory location, compares the value with an "expected" one provided by the user, and writes out a "new" value if the two match, returning whether the update succeeded. We can use this to fix the non-atomic counter algorithm as follows: :# Read the value in the memory location; :# add one to the value; :# use compare-and-swap to write the incremented value back; :# retry if the value read in by the compare-and-swap did not match the value we originally read. Since the compare-and-swap occurs (or appears to occur) instantaneously, if another process updates the location while we are in-progress, the compare-and-swap is guaranteed to fail.Fetch-and-increment
Many systems provide an atomic fetch-and-increment instruction that reads from a memory location, unconditionally writes a new value (the old value plus one), and returns the old value. We can use this to fix the non-atomic counter algorithm as follows: :# Use fetch-and-increment to read the old value and write the incremented value back. Using fetch-and increment is always better (requires fewer memory references) for some algorithms—such as the one shown here—than compare-and-swap, even though Herlihy earlier proved that compare-and-swap is better for certain other algorithms that can't be implemented at all using only fetch-and-increment. So CPU designs with both fetch-and-increment and compare-and-swap (or equivalent instructions) may be a better choice than ones with only one or the other.Locking
Another approach is to turn the naive algorithm into a critical section, preventing other threads from disrupting it, using aSee also
* Atomic transaction * Consistency model *References
Further reading
* * * * {{cite web, author=Aphyr, title=Strong Consistency Models, url=https://aphyr.com/posts/313-strong-consistency-models, website=aphyr.com, publisher=Aphyr, access-date=13 April 2018 Consistency models Transaction processing Concurrency control