Arpit Saxena

Art of MP Ch 3 - Concurrent Objects

• 6 min read • Last modified

Concurrency and Correctness

Behaviour of concurrent objects is described through their safety and liveness properties, also known as correctness and progress.

All ideas of correctness of concurrent objects involves drawing some equivalence with sequential behaviour, but the relation is different for different objects.

Sequential Objects

Since correctness for concurrent objects relies on some equivalence with sequential objects, let’s look at how we can talk about correctness of sequential objects.

The API documentation of an object describes, for each method, that if the object satisfies so and so condition then after the method it will satisfy some other condition. These are preconditions and postconditons which the doc describes.

This style of documentation is called a sequential specification and it allows us to write a specification that grows linearly with the number of methods of an object. This avoids having to think about interaction of a method with all other possible methods.

This specification style, which talks about state of an object before and after a method call, does not work with concurrent objects. This is because there can be overlapping method calls on the object, and it doesn’t make sense to talk about their order. In a single threaded program, an object assumes meaningful state only between function calls but a concurrent object can be acted upon by methods at all times and there may never be a moment when it’s between function calls.

Sequential Consistency

First we have some definitions:

  • Method call: Interval that starts with an invocation event and ends with a response event, if any.
  • Pending Method Call: A method call whose invocation event has happened but not its response event
  • Register: Read-Write Memory Location
  • Program Order: The order in which a single thread issues method calls

We also define some principles (numbering varies from the book) which we’ll combine to define different correctness properties of concurrent objects:

  • Principle 1: Method calls should appear to happen in a one-at-a-time, sequential order
    • This is because we want the final result to come from some ordering of method calls, and not have partial effects from multiple of them. For example, concurrent writes of -3 and 7 to a register should never result in -7.
  • Principle 2: Method calls should appear to take effect in program order
    • This is because we expect a thread to read it’s own writes. A thread writing -3 followed by 7 to a register should read 7 (in the absence of other threads)

Sequential Consistency is defined as a correctness condition in which both Principle 1 and Principle 2 hold

Note: Only having Principle 1 would say that this situation is also correct: A single thread does W(x) = 1 => W(x) = 2 => R(x) = 0 (x = 0 is the initial value) i.e. the thread always reads from initialisation value, ignoring its own writes.

In other words, Sequential Consistency requires that method calls act as if executed in a sequential order which is consistent with the program order.

Sequential Consistency vs Real Time Order

How to read the above diagram?

q represents a queue with enqueue and dequeue operations. q.enq(x) means that an enqueue happened of item x and q.deq(x) means that a dequeue was executed which returned x

Here we can see that the sequentially consistent order goes against the flow of time, showing that sequential consistency doesn’t have to agree with real time orders.

Sequential Consistency is Nonblocking

Will touch on this later, when defining things formally

Compositionality

A property P is compositional if a system comprised of modules which satisfy property P also satisfies P. This is important since we can look at find the correctness property of the system while only looking at the interface of its components.

When modules with a noncompositional property are combined, we can’t know the property of the system without going into internals of the modules and proving the property for the system again.

The above image shows that Sequential Consistency is not compositional. p and q are concurrent sequentially consistent queues. However, a system combining these 2 is not sequentially consistent. In the above example, there is a cycle formed by Sequentially Consistent order of p & q and program order. Which means that the ordering of the system as a whole is not sequentially consistent — writes cannot appear to take effect in program order.

Linearizability

  • Principle 3 (Linearizability): Evert method call should appear to take effect instantaneously at some moment between its invocation and response.

With linearizability, real time order of method calls is preserved.

Linearization Point

A linearization point of a method is a time between its invocation and response when the method appears to take effect. We say that a method is linearized at its linearization point.

For methods with locks, linearization point can be anywhere within the critical section. For others, it is usally a statement in the function after which its results are visible outside. For example, updating the next value in a function that adds a value to a linked list.

vs Sequential Consistency

Threads that communicate using only one shared object (e.g. shared memory of a SMP processor) cannot distinguish between sequential consistency and linearizabliity. Only an external observer which can see real time order in which operations take effect can make this distinction. This is why sometimes linearizability is called external consistency.

Also, Linearizability is compositional while SC is not.

Quiescent Consistency

  • Principle 4: Method calls separated by a period of quiescence should appear to take place in real-time order

Together, Principle 1 and Principle 4 define Quiescent Consistency. Informally, it says that any time an object becomes quiescent, the execution so far is equivalent to a sequential order of the executed method calls.

A time it can be useful is implementing a concurrent counter. Whenever we call incrementAndGet(), we are not guaranteed to get the index in the exact order of our call. BUT, we’ll get a result that is unique and the numbers returned would be monotonic. The calls which happened concurrently (happened when the object was not quiescent) appear to happen in some sequential order.

Properties

Quiescent Consistency and Sequential Consistency are incomparable:

  1. QC doesn’t necessarily respect program order: Two calls which are executed by the same thread might not be separated by a period of quiescence so they can be reordered.
  2. SC is not affected by periods of quiescence: Two calls separated by a period of quiescence can happen in reverse real time order in a sequentially consistent execution. We have seen that SC doesn’t respect real-time order.

Linearizability is stronger than both QC and SC. A linearizable object is both sequentially and quiescently consistent.

It is nonblocking, same as QC and SC. Meaning and proof in some next section.

Advantage is that QC is compositional. Two objects which are QC can be used together and the resulting system will also be QC. Period of quiescence for the system would mean periods of quiescence for all the objects in the system, hence ordering the calls.

Graph View