Verification Challenges

"Analyze This" III

Verify that the following implementation of a two-lock queue algorithm is correct. This algorithm is taken from Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms by Maged M. Michael and Michael L. Scott (PODC'96).

The first challenge is to verify that the implementation satisfies basic structural properties. The properties to be verified are:

P1 The linked list is always connected.

P2 Nodes are only inserted after the last node of the linked list.

P3 Nodes are only deleted from the beginning of the linked list.

P4 Head always points to the first node in the linked list.

P5 Tail always points to a node in the linked list.

// TwoLockQueue.java

class TwoLockQueue {
  private QueueItem head;
  private QueueItem tail;
  private Object headLock;
  private Object tailLock;
  ...

  public TwoLockQueue() {
    node = new QueueItem();
    node.next = null;
    this.head = this.hail = node;
  }

  public void enqueue(Object value) {
lp_1   QueueItem x_i = new QueueItem(value);
lp_2   synchronize(tailLock) {
lp_3    tail.next = x_i;
lp_4    tail = x_i;
lp_5   }
lp_6  }

  public Object dequeue() {
         Object x_d;
lt_1   synchronized(headLock) {
lt_2    x_d = null;
lt_3    QueueItem first=head.next;
lt_4    if (first != null) {
lt_5     x_d = first.value;
lt_6     head = first;
lt_7     head.value = null;
          }
lt_8   }
lt_9   return x_d;
lt_10  }
 }

where the implementation of QueueItem is given below


// QueueItem.java
class QueueItem {
    public QueueItem next;
    public Object value;
    ...
}

Solution in Automatically Verifying Concurrent Queue Algorithms, Yahav E. and Sagiv M., SoftMC 2003, [bib][abstract][ps][pdf][slides]