How can we judge if the concurrent execution is correct? the schematics of concurrent consistency.

Consistency properties of concurrent objects:

Quiescent Consistency, Sequential Consistency and Linearizability

For concurrent objects, the two things we care about the most:

• Safety (Correctness): is the result what we expect?
• Liveness (Progress): will the program keep working?

For the former, there are three major correctness conditions namely

• Quiescent Consistency
• Sequential Consistency
• Linearizability

THE IDEA is to define formal verification of correctness by mapping the behaviours of a concurrent object to the behaviours of the corresponding abstract (sequential) data structure.

Definitions

Quiescent Consistency

• Method calls should appear to happen in a one-at-a-time, sequential order
• Method calls separated by a period of quiescence should appear to take effect in their real-time order

Sequential Consistency

• Method calls should appear to happen in a one-at-a-time, sequential order
• Method calls should appear to take effect in program order

Requires that the operations should appear to take effect in the order they are specified in each program

Linearizability

• Each method call should appear to take effect instantaneously at some moment between its invocation and response

Formal definitions

• Notations of invocations and responses
  • Invocation <x.m(a*) A>
  • Response <x:t(r*) A>
  • x for object, m for method, t is either Ok or an exception, a* for a sequence of arguments, r* for a sequence of result values. A for thread History models an execution of a concurrent system. History is a finite sequence of method invocation and response events.
• A SubHistory of a history H is a subsequence of the events of H.
• thread subhistory H|A and Object subhistoryH|x
• A Method call in a history H is a pair consisting of an invocation and the next matching response in H.
• An invocation is pending in H if no matching response follows.
• An extension of H is a history constructed by appending responses to zero or more pending invocation of H.
• complete(H) is the subsequence of H consisting of all matching invocations and responses (ignore pending invocations)
• A history H is sequential if the first event is an invocation and each invocation except possibly the last, is immediately followed by a matching response.
• two histories H and H’ are equivalent if for every thread A, H|A = H'|A
• A history H is well-formed if each thread subhistory is sequential (one thread can not start a new invocation while another is still pending)
• A sequential history is legal if each object subhistory is legal for that object.
• a mthod call m0 precedes a method call m1 in history H if m0 finished before m1 started (m0s response event occurs before m1’s invocation event), noted by m0 ->H m1

Define linearizability with history notations

A history H is linearizable if it has an extension H’ and there is a legal (sequential) subhistory S such that

• complete(H’) is equivalent to S and
• if method call m0 precedes method call m1 in H, then the same is true in S.

S is referred to as a linearization of H (there can be many).
the idea of extending H: invocations may have taken effects before the response event.

notes:

• First appending events to H, getting H’, then take a complete subsequence out of H’. The idea is that, if there is pending invocations in H, we can assume none or some them have taken effect, and discard those that haven’t.
• Finding a linearization S: reorder the overlapping method calls to map the execution to a sequential one that meets sequential specification.
• the precedence constrains catch the idea that, if two invocations are not overlapping, then they must preserve the real time order!

Remarks of the three correctness conditions:

Quiescent Consistency is, if there is a point where no method call is pending, then what happens before this point and what happens after should keep strict real-time order.

• Weakest constrains
• Appropriate for high performance applications
• Non-Blocking
• Compositional

Sequential Consistency is, if the program code writes A happen before B, then it should.

• Stronger constrains
• useful for low-level systems e.g. hardware memory interfaces
• Non-Blocking
• NOT Compositional

Linearizability is, method calls take effect atomically at some point between its invocation and return event. Overlapping calls can be reorered in the scope of their intervals, but precedence orders must be preserved

• Strongest constrains
• for high-level (compositional) systems
• Non-Blocking
• Compositional

De-Confusion

Q1.Quiescent consistency and sequential consistency are incomparable

There are some executions that are quiescently consistent but not sequentially consistent, and vice versa.

Q1A. Give an example

for a FIFO queue

A ---q.enq(x)--------q.deq(y)--
B ---------------q.enq(y)------

A deq(y) is not acceptable by quiescent consistency because q.enq(x) and q.enq(y) are separated by a quiescence and they must take effect in a real-time order. Thus y cannot be dequeued before x.

However this is acceptable by sequential consistency. Because 1) there is at least one sequential execution that can explain: q.enq(y), q.enq(x) , q.deq(y) 2) From each process’s perspective the execution doesn’t violate program order.

Q1B. Give a vice versa example?
see Q3.

Q2.What do you mean by " Method calls should appear to happen in a one-at-a-time, sequential order" ?

For example we have 2 method calls r.write(7) and r.write(-3), we expect the register to have either value 7 or -3, it should be neither anything else, nor a mixture of both (e.g. -7)

If we have multiple concurrent method calls, we don’t need to care about the exact order they take effects, but they should at least take effect one-after-another.

Q3. I feel like quiescent consistency and linearizability are all the same.

Quiescent consistency is WEAKER than linearizability. for example concurrnet method calls:

<----A-----> <-----B------>
    <------C-------->

in linearizability A and B can not be reordered since the precedence order must be preserved. However in quiescent consistency B can be placed before A because there is no quiescent point between A and B (C is pending)

Q4. We can’t expect sequential consistency to be preserved by default:

modern hardware(cpus) may reorder operations. To guarantee sequential consistency, programmers must explicitly ask for it (e.g. memory barriers and fences)

Q4A. why is even sequential consistency too strong/expensive for hardware ?

for example if you write to a register then read from it, to respect sequential consistency you must read the value that you have written. BUT the hardware can’t guarantee that by default (because write cache, because of delay, etc.). Even for something as basic as write-read consistency you have to ASK FOR IT

Q5. These 3 consistency are not the only ones defined

furthermore there are notions (weaker then linearizability) such as eventual consistency, quasi linearizability, k-linearizability etc.