Linearizability: Simple Queue (NuSMV)

Description of the Case Study

This benchmark captures a bounded first-in first-out queue built as a circular buffer with five slots [HS08]. Two threads interleave enqueue and dequeue operations by reading and updating shared head and tail indices as well as the array cells that hold queued values. The queue is designed so that successful operations mimic a linearizable FIFO behavior, but concurrent schedules may reorder the value that is ultimately dequeued.

The concurrent NuSMV model steps both threads through their enqueue/dequeue phases and records the value removed from the queue on each execution. The sequential specification executes the same operations atomically, producing a canonical removal value.

The NuSMV model(s)

MODULE main

VAR
  step : 0..10;

  Q0 : 0..9;
  Q1 : 0..9;
  Q2 : 0..9;
  Q3 : 0..9;
  Q4 : 0..9;

  back : 0..5;        
  removed : 0..9;

  T1_state : 0..3;     
  T2_state : 0..3;

ASSIGN

  init(step) := 0;
  next(step) := case
    step < 10 : step + 1;
    TRUE : step;
  esac;

  init(Q0) := 0; init(Q1) := 0; init(Q2) := 0;
  init(Q3) := 0; init(Q4) := 0;
  init(back) := 0;
  init(removed) := 0;
  init(T1_state) := 0;
  init(T2_state) := 0;


  next(T1_state) := case
    step = 1 | step = 5 : 1;
    step = 3 | step = 7 : 2;
    step = 4 | step = 8 : 3;
    TRUE : T1_state;
  esac;

  next(T2_state) := case
    step = 1 | step = 5 : 1;
    step = 3 | step = 7 : 2;
    step = 9 : 3;
    TRUE : T2_state;
  esac;


  next(back) := case
    (T1_state = 1 | T2_state = 1) & back < 5 : back + 1;
    (T1_state = 2 | T2_state = 2) & back > 0 : back - 1;
    TRUE : back;
  esac;


  next(removed) := case
    T1_state = 2 & T2_state = 2 & back > 1 : Q1;
    (T1_state = 2 | T2_state = 2) & back > 0 : Q0;
    TRUE : removed;
  esac;


  next(Q0) := case
    (T1_state = 2 | T2_state = 2) & back > 1 : Q1;
    (T1_state = 2 | T2_state = 2) & back = 1 : 0;
    back = 0 & T1_state = 1 : 1;
    back = 0 & T2_state = 1 : 2;
    TRUE : Q0;
  esac;


  next(Q1) := case
    (T1_state = 2 | T2_state = 2) & back > 2 : Q2;
    (T1_state = 2 | T2_state = 2) & back = 2 : 0;
    back = 1 & T1_state = 1 : 3;
    back = 1 & T2_state = 1 : 4;
    TRUE : Q1;
  esac;


  next(Q2) := case
    (T1_state = 2 | T2_state = 2) & back > 3 : Q3;
    (T1_state = 2 | T2_state = 2) & back = 3 : 0;
    back = 2 & T1_state = 1 : 5;
    back = 2 & T2_state = 1 : 6;
    TRUE : Q2;
  esac;


  next(Q3) := case
    (T1_state = 2 | T2_state = 2) & back > 4 : Q4;
    (T1_state = 2 | T2_state = 2) & back = 4 : 0;
    back = 3 & T1_state = 1 : 7;
    back = 3 & T2_state = 1 : 8;
    TRUE : Q3;
  esac;


  next(Q4) := case
    (T1_state = 2 | T2_state = 2) : 0;
    back = 4 & T1_state = 1 : 9;
    back = 4 & T2_state = 1 : 1;
    TRUE : Q4;
  esac;

The HyperLTL formula(s)

The observational-determinism requirement demands that all executions remove identical values at every step, regardless of the interleaving. HyperQB discovers a counterexample where two traces disagree on the dequeued value, demonstrating the queue’s non-linearizable behaviour.

\[\varphi_{\text{det}} = \forall \pi_A.\forall \pi_B.\ \Box \left( \mathit{removed}_{\pi_A} = \mathit{removed}_{\pi_B} \right)\]
Forall A . Forall B .
    G(
        (removed[A] = removed[B])
    )

References

  • [HS08] M. Herlihy and N. Shavit. *The Art of Multiprocessor Programming*. Morgan Kaufmann, 2008.