Concurrent Objects

1. FIFO Queues

A FIFO queue stores a head and tail pointer, with fields protected by a single shared lock. A basic implementation:

1class LockBasedQueue[T: ClassTag](val capacity: Int) {
2  private var head, tail: Int = 0 // Initially, head = tail
3  private val items = new Array[T](capacity)
4  private val lock = new ReentrantLock()
5
6  def enq(x: T): Unit = {
7    lock.lock()
8    try {
9      if ((tail - head) == items.length) throw FullException()
10      items(tail % items.length) = x
11      tail += 1
12    } finally {
13      lock.unlock()
14    }
15  }
16
17  def deq(): T = {
18    lock.lock()
19    try {
20      if (head == tail) throw EmptyException()
21      val x = items(head % items.length)
22      head += 1
23      x
24    } finally {
25      lock.unlock()
26    }
27  }
28}

1.1 Wait-Free Queue

If there would be two threads, one doing enq and one doing deq, we don't need mutual exclusion, so no lock is needed. This is a wait-free implementation.

1class LockFreeQueue[T: ClassTag](val capacity: Int) {
2
3  @volatile
4  private var head, tail: Int = 0
5  private val items = new Array[T](capacity)
6
7  def enq(x: T): Unit = {
8    if ((tail - head) == items.length) throw FullException()
9    items(tail % items.length) = x
10    tail += 1
11  }
12
13  def deq(): T = {
14    if (head == tail) throw EmptyException()
15    val x = items(head % items.length)
16    head += 1
17    x
18  }
19}

This time, it is a lot more difficult to tell that this implementation is correct.

2. Formal Specification

We must specify the safety and liveness properties of the object. A sequential object has state given by its fields, and methods defining how to manipulate state.

Sequential specification states that given a precondition on the state, a method will produce a postcondition on the state and return value. We can describe meaningful state only between method calls and and each method can be described in isolation.

In a concurrent specification, methods overlap, so an object may never be between method calls. We must characterise all possible interactions with concurrent calls. Additionally, adding new methods may invalidate existing specifications.

2.1 Linearizability

A history is a sequence of invocation and response events. By assuming SC, we can project a concurrent history to a sequential one by only looking at the non-overlapping method calls (the bits protected by the locks). Assume each method takes effect instantaneously at some point between its invocation and response, if this is possible, the object is linearizable.

We can prove an execution is linearizable by finding a linearization point for each method call, such that the sequential history formed by these points satisfies the sequential specification. If we cannot find such points, the object is not linearizable. In a history, we can pick any point between invocation and response as the linearization point.

We can't specify the linearization point without the execution, because a method may have multiple linearization points which depend on the execution.

A history is linearizable if it can be extended to by appending zero or more responses to pending invocations or discarding other pending invocations such that is equivalent to a legal sequential history where .

2.2 Histories

A history is a sequence of invocation and response events. It is sequential if there are no overlapping histories - each invocation is immediately followed by its response. For it to be legal, it must be sequential per thread and respect the sequential specification of the object.

Histories are equivalent if their per-thread projections (sets of events for each thread) are the same.

2.3 Precedence

A method call precedes another if the response of the first occurs before the invocation of the second. This defines a partial order on method calls. Methods that do not precede each other are overlapping. Given a history and method executions and in :

2.4 Composability Theorem

History is linearizable if and only if for each object , the subhistory (the projection of onto ) is linearizable.

2.5 Sequential Consistency

A history is sequentially consistent if it can be extended to by appending zero or more responses to pending invocations or discarding other pending invocations such that is equivalent to a legal sequential history . With SC, we do not need to preserve real-time order, and can reorder non-overlapping operations done by different threads arbitrarily.

SC is not composable.

2.6 Progress Conditions

There are main progress conditions for concurrent objects:

Back to Home