Linearizability: Explicit Memory Management ABA (NuSMV)¶

Description of the Case Study¶

This case study models the Treiber stack [Tre86] under explicit memory management (EMM). Two threads share a stack implemented over a pair of reusable nodes. Once a pop returns a node to the free list, it becomes immediately available for the next push, recreating the classical ABA scenario. Linearizability [HW90] requires that every concurrent history of push and pop operations can be matched by some sequential execution that preserves invocation and response order.

The concurrent NuSMV model explicitly tracks when each thread invokes, completes, and succeeds at push or pop, while the sequential specification executes the same operations one at a time. Under pessimistic semantics, a bounded counterexample is sufficient to disprove linearizability. HyperQB flags the model as SAT within the given bound, producing a witness where a thread observes a recycled node whose value no longer matches a valid sequential history, exposing the ABA bug that arises without reclamation safeguards.

The NuSMV model(s)¶

-- Two-thread Treiber stack over 2 nodes; free1/free2 work as a free-pool stack emulating (EMM)
-- with an explicit chosen mechanic for selecting which free node to push

MODULE main
VAR
  -- Shared stack top: 0=NULL, 1=NODE1, 2=NODE2
  top         : 0..2;

  -- Free-pool flags: TRUE = node free; FALSE = allocated
  free1       : boolean;
  free2       : boolean;

  -- Each node's next pointer (valid if allocated)
  next1       : 0..2;
  next2       : 0..2;

  -- Node payloads (1 or 2)
  val1        : 1..2;    -- NODE1 payload, initially 1; on reallocate becomes 2
  val2        : 1..2;    -- NODE2 payload, initially 2; on reallocate becomes 1

  --delay

  -- Thread 1 control & locals (with two extra pop steps)
  p1_pc       : 0..7;
  p1_op      : 0..2;    -- operation type {PUSH=0, POP=1, NONE=2}
  p1_old_top  : 0..2;-- Cas variables
  p1_old_next : 0..2;
  p1_ret      : 0..2;
  p1_ret_push : boolean; -- return value for T1 push operation (TRUE=success, FALSE=failure)
  p1_chosen   : 0..2;    -- which node T1 will allocate on its next push (0=none,1 or 2)

  -- Thread 2 control & locals
  p2_pc       : 0..6;    -- 0-start_pop,1-pop,2-return,3-start_push,4-push,5-return_push(done)
  p2_old_top  : 0..2;
  p2_old_next : 0..2;
  p2_ret      : 0..2;    -- return value for T2 pop operation
  p2_ret_push : boolean; -- return value for T2 push operation (TRUE=success, FALSE=failure)
  p2_chosen   : 0..2;    -- which node T2 will allocate on its next push (0=none,1 or 2)

ASSIGN
  -- Initial state: stack = [1->2->NULL]
  init(top)        := 1;
  init(next1)      := 2;
  init(next2)      := 0;
  init(free1)      := FALSE;
  init(free2)      := FALSE;
  init(val1)       := 1;
  init(val2)       := 2;

  init(p1_pc)      := 0;
  init(p1_op)      := 2; -- NONE
  init(p1_old_top) := 0;
  init(p1_old_next):= 0;
  init(p1_ret)     := 0;
  init(p1_ret_push):= FALSE;
  init(p1_chosen)  := 0;

  init(p2_pc)      := 0;
  init(p2_old_top) := 0;
  init(p2_old_next):= 0;
  init(p2_ret)     := 0;
  init(p2_ret_push):= FALSE;
  init(p2_chosen)  := 0;

  -- Update val1 on T2's push CAS; and val2 on T1's push CAS
  next(val1) := case
    p2_pc = 4 & p2_chosen = 1 : {1, 2};
    TRUE                      : val1;
  esac;
  next(val2) := case
    p1_pc = 6 & p1_chosen = 2 : {1, 2};
    TRUE                      : val2;
  esac;

  -- Update shared top
  next(top) := case
    p1_pc = 2 & top = p1_old_top : p1_old_next;
    p1_pc = 2                    : top;
    p2_pc = 1 & top = p2_old_top : p2_old_next;
    p2_pc = 1                    : top;
    p1_pc = 6 & p1_chosen != 0   : p1_chosen;
    p2_pc = 4 & p2_chosen != 0   : p2_chosen;
    TRUE                         : top;
  esac;

  -- Update next1
  next(next1) := case
    p1_pc = 2 & p1_old_top = 1 & top = p1_old_top : 0;
    p2_pc = 1 & p2_old_top = 1 & top = p2_old_top : 0;
    p1_pc = 5 & p1_chosen = 1                     : top;
    p2_pc = 3 & free1                             : top;
    TRUE                                          : next1;
  esac;

  -- Update next2
  next(next2) := case
    p1_pc = 2 & p1_old_top = 2 & top = p1_old_top : 0;
    p2_pc = 1 & p2_old_top = 2 & top = p2_old_top : 0;
    p1_pc = 5 & p1_chosen = 2                     : top;
    p2_pc = 3 & free2                             : top;
    TRUE                                          : next2;
  esac;

  -- Update free1
  next(free1) := case
    p1_pc = 2 & p1_old_top = 1 & top = p1_old_top : TRUE;
    p2_pc = 1 & p2_old_top = 1 & top = p2_old_top : TRUE;
    p1_pc = 6 & p1_chosen = 1                     : FALSE;
    p2_pc = 4 & p2_chosen = 1                     : FALSE;
    TRUE                                          : free1;
  esac;

  -- Update free2
  next(free2) := case
    p1_pc = 2 & p1_old_top = 2 & top = p1_old_top : TRUE;
    p2_pc = 1 & p2_old_top = 2 & top = p2_old_top : TRUE;
    p1_pc = 6 & p1_chosen = 2                     : FALSE;
    p2_pc = 4 & p2_chosen = 2                     : FALSE;
    TRUE                                          : free2;
  esac;

  -- Thread 1 control flow (pop goes through two extra steps before done; push unchanged)
  next(p1_pc) := case
    p1_pc = 0 : {1, 5};
    p1_pc = 1 : {1, 2};  
    p1_pc = 2 : 3;       
    p1_pc = 3 : 4;
    (p1_pc = 4) & (p2_pc = 4) : 4;
    p1_pc = 4 & p2_pc != 4 : 7;       
    p1_pc = 5 & (p2_pc != 5) : 5;
    p1_pc = 5 & (p2_pc = 5) : 6;     
    p1_pc = 6 : 7;      
    TRUE      : 0;       
  esac;

  next(p1_op) := case
    p1_pc = 1 : 1; -- choose PUSH or POP
    p1_pc = 5 : 0; -- choose PUSH or POP
    p1_pc = 7 : 2; -- done
    TRUE      : p1_op;
  esac;

  -- Snapshot for pop (T1)
  next(p1_old_top) := case
    p1_pc = 1                   : top;
    TRUE                        : p1_old_top;
  esac;
  next(p1_old_next) := case
    p1_pc = 1 & top = 1 : next1;
    p1_pc = 1 & top = 2 : next2;
    TRUE                : p1_old_next;
  esac;

  -- Record return (T1) after the two extra pop steps
  next(p1_ret) := case
    p1_pc = 4 & top = p1_old_top & free1  : val2;
    p1_pc = 4 & top = p1_old_top & free2  : 0;
    p1_pc = 4 & top = p1_old_top & !free1 : val1;
    p1_pc = 4 & top != p1_old_top         : 0;
    TRUE                                  : p1_ret;
  esac;

  -- Record return (T1) push operation
  next(p1_ret_push) := case
    p1_pc = 6 & p1_chosen != 0 : TRUE;   -- push succeeds if node was chosen
    p1_pc = 6 & p1_chosen = 0  : FALSE;  -- push fails if no node available
    TRUE                       : p1_ret_push;
  esac;

  -- Choose which node T1 will push at push_load
  next(p1_chosen) := case
    p1_pc = 5 & free2 : 2;
    p1_pc = 5 & free1 : 1;
    TRUE      : p1_chosen;
  esac;

  -- Thread 2 control flow (unchanged)
  next(p2_pc) := case
    p2_pc = 0 : 1;
    p2_pc = 1 : 2;
    p2_pc = 2 : 3;
    p2_pc = 3 : 4;
    p2_pc = 4 : 5;
    TRUE      : 0;
  esac;

  -- Snapshot for pop (T2)
  next(p2_old_top) := case
    p2_pc = 0 : top;
    TRUE      : p2_old_top;
  esac;
  next(p2_old_next) := case
    p2_pc = 0 & top = 1 : next1;
    p2_pc = 0 & top = 2 : next2;
    TRUE : p2_old_next;
  esac;

  -- Record return (T2) after pop cas
  next(p2_ret) := case
    p2_pc = 1 & top = p2_old_top & p2_old_top = 1 & !free1 : val1;
    p2_pc = 1 & top = p2_old_top & p2_old_top = 2 & !free2 : val2;
    p2_pc = 1 & top = p2_old_top & p2_old_top = 1 & free1  : 0;
    p2_pc = 1 & top = p2_old_top & p2_old_top = 2 & free2  : 0;
    p2_pc = 1 & top != p2_old_top                          : 0;
    TRUE                                                   : p2_ret;
  esac;

  -- Record return (T2) push operation
  next(p2_ret_push) := case
    p2_pc = 4 & p2_chosen != 0 : TRUE;   -- push succeeds if node was chosen
    p2_pc = 4 & p2_chosen = 0  : FALSE;  -- push fails if no node available
    TRUE                       : p2_ret_push;
  esac;

  -- Choose which node T2 will push at push_load
  next(p2_chosen) := case
    p2_pc = 3 & free2 : 2;
    p2_pc = 3 & free1 : 1;
    TRUE              : p2_chosen;
  esac;

DEFINE
  -- Thread 1 operation predicates
  p1_push_invoked := (p1_pc = 5) | (p1_pc = 6);  -- push_load or push_cas
  p1_pop_invoked  := (p1_pc = 1) | (p1_pc = 2) | (p1_pc = 3) | (p1_pc = 4);  -- pop_load, pop_cas, pop_extra1, pop_extra2

  -- Thread 2 operation predicates  
  p2_push_invoked := (p2_pc = 3) | (p2_pc = 4);  -- push_load or push_cas
  p2_pop_invoked  := (p2_pc = 0) | (p2_pc = 1);  -- pop_load or pop_cas

  -- Combined operation predicates
  invoked_push := (p1_push_invoked | p2_push_invoked);
  invoked_pop  := (p1_pop_invoked | p2_pop_invoked);

  -- Return predicates
  returning_push := (p1_pc = 7 & p1_op = 0) | (p2_pc = 5);
  returning_pop  := (p1_pc = 7 & p1_op = 1) | (p2_pc = 2);

  -- Success return predicates
  push_return := (p1_ret_push) | (p2_ret_push);
  pop_return  := (p1_ret != 0) | (p2_ret != 0);

-- Sequential Treiber stack with 2 elements matching concurrent version
-- Processes execute sequentially using busy flag and stutter mechanism
MODULE main
VAR
  -- Simple stack state (matching concurrent version)
  val1        : 1..2;    -- node 1 value
  val2        : 1..2;    -- node 2 value
  top_pointer : 0..2;    -- stack top: 0=empty, 1=val1, 2=val2
  busy     : boolean; -- busy flag (TRUE=busy, FALSE=free)

  -- Process 1 control & locals
  p1_pc      : 0..2;    -- 0=idle, 1=execute, 2=done
  p1_op      : 0..2;    -- operation type {PUSH=0, POP=1, NONE=2}
  p1_value   : 1..2;    -- value to push
  p1_ret     : 0..2;    -- return value (0=empty, 1,2=popped value)
  p1_ret_push: boolean; -- return value for push operation
  p1_modified: boolean; -- indicates if process 1 modified the stack

  -- Process 2 control & locals  
  p2_pc      : 0..2;    -- 0=idle, 1=execute, 2=done
  p2_op      : 0..2;    -- operation type {PUSH=0, POP=1, NONE=2}
  p2_value   : 1..2;    -- value to push
  p2_ret     : 0..2;    -- return value (0=empty, 1,2=popped value)
  p2_ret_push: boolean; -- return value for push operation
  p2_modified: boolean; -- indicates if process 2 modified the stack

ASSIGN
  -- initial state: stack = [val1->val2->NULL] (matching concurrent model)
  init(val1)        := 1;
  init(val2)        := 2;
  init(top_pointer) := 1;  -- stack starts with val1 on top
  init(busy)        := TRUE; -- stack is initially free
  next(busy) := case
    p2_pc = 2 : TRUE; -- busy when process 2 is done
    p1_pc = 2 : TRUE;
    TRUE : FALSE; -- free otherwise
  esac;

  -- Process 1 initial state
  init(p1_pc)      := 0;
  init(p1_op)      := 2; -- NONE
  init(p1_value)   := 1;
  init(p1_ret)     := 0;
  init(p1_ret_push):= FALSE;
  init(p1_modified):= FALSE; -- initially not modified

  -- Process 2 initial state
  init(p2_pc)      := 1;
  init(p2_op)      := 1; -- remove
  init(p2_value)   := 2;
  init(p2_ret)     := 0;
  init(p2_ret_push):= FALSE;
  init(p2_modified) := FALSE; -- initially not modified
  next(p2_modified) := case
    p2_pc = 2 : TRUE; -- modified when process 2 is done
    p1_pc = 2 : FALSE; -- not modified otherwise
    TRUE : p2_modified; -- keep current state
  esac;

  next(p1_modified) := case
    p1_pc = 2 : TRUE; -- modified when process 1 is done
    p2_pc = 2 : FALSE; -- not modified otherwise
    TRUE : p1_modified; -- keep current state
  esac;

  -- Process 1 operation selection
  next(p1_op) := case
    p1_pc = 0 : {0, 1}; -- choose PUSH or POP
    TRUE : p1_op;
  esac;

  -- Process 2 operation selection  
  next(p2_op) := case
    p2_pc = 0 : {0, 1}; -- choose PUSH or POP
    TRUE : p2_op;
  esac;

  -- Process 1 value selection for push
  next(p1_value) := case
    p1_pc = 0 : {1, 2}; -- choose value to push
    TRUE : p1_value;
  esac;

  -- Process 2 value selection for push
  next(p2_value) := case
    p2_pc = 0 : {1, 2}; -- choose value to push
    TRUE : p2_value;
  esac;

  -- Process 1 control flow
  next(p1_pc) := case
    p1_pc = 0 : 1; -- idle -> execute
    p1_pc = 1 & busy : 1;
    p1_pc = 1 : {1, 2}; -- execute -> done
    p1_pc = 2 : 0; -- done -> idle
    TRUE : p1_pc;
  esac;

  -- Process 2 control flow
  next(p2_pc) := case
    p2_pc = 0 : 1; -- idle -> execute
    p2_pc = 1 : {1, 2}; -- execute -> done
    p2_pc = 2 : 0; -- done -> idle
    TRUE : p2_pc;
  esac;

  -- Update val1 and val2 when pushed
  next(val1) := case
    p1_pc = 2 & p1_op = 0 & p1_value = 1 & top_pointer = 0 : p1_value; -- P1 pushes to val1
    p2_pc = 2 & p2_op = 0 & p2_value = 1 & top_pointer = 0 : p2_value; -- P2 pushes to val1
    TRUE : val1;
  esac;
  
  next(val2) := case
    p1_pc = 2 & p1_op = 0 & p1_value = 2 & top_pointer = 0 : p1_value; -- P1 pushes to val2
    p2_pc = 2 & p2_op = 0 & p2_value = 2 & top_pointer = 0 : p2_value; -- P2 pushes to val2
    TRUE : val2;
  esac;

  -- update stack on push or pop
  next(top_pointer) := case
    -- Push operations: set top_pointer to the node being pushed
    p1_pc = 2 & p1_op = 0 & p1_value = 1 & top_pointer = 0 : 1;  -- P1 push val1 to empty
    p1_pc = 2 & p1_op = 0 & p1_value = 2 & top_pointer = 0 : 2;  -- P1 push val2 to empty
    p2_pc = 2 & p2_op = 0 & p2_value = 1 & top_pointer = 0 : 1;  -- P2 push val1 to empty
    p2_pc = 2 & p2_op = 0 & p2_value = 2 & top_pointer = 0 : 2;  -- P2 push val2 to empty
    -- Pop operations: set top_pointer to 0 (empty)
    p1_pc = 2 & p1_op = 1 & top_pointer > 0 : 0;  -- P1 pop: empty stack
    p2_pc = 2 & p2_op = 1 & top_pointer > 0 : 0;  -- P2 pop: empty stack
    TRUE : top_pointer;
  esac;

  -- Process 1 return value on pop
  next(p1_ret) := case
    p2_modified : 0; -- if process 2 modified, return empty
    p1_pc = 1 & p1_op = 1 & top_pointer = 1 : val1; -- return val1
    p1_pc = 1 & p1_op = 1 & top_pointer = 2 : val2; -- return val2
    p1_pc = 1 & p1_op = 1 & top_pointer = 0 : 0;    -- return empty
    TRUE : p1_ret;
  esac;

  -- Process 2 return value on pop
  next(p2_ret) := case
    p1_modified : 0; -- if process 1 modified, return empty
    p2_pc = 2 & p2_op = 1 & top_pointer = 1 : val1; -- return val1
    p2_pc = 2 & p2_op = 1 & top_pointer = 2 : val2; -- return val2
    p2_pc = 2 & p2_op = 1 & top_pointer = 0 : 0;    -- return empty
    TRUE : p2_ret;
  esac;

  -- Process 1 push return value
  next(p1_ret_push) := case
    p2_modified : FALSE; -- if process 2 modified, push failed
    p1_pc = 1 & p1_op = 0 & top_pointer = 0 : TRUE;  -- push succeeded (to empty stack)
    p1_pc = 1 & p1_op = 0 & top_pointer > 0 : FALSE; -- push failed (stack not empty)
    TRUE : p1_ret_push;
  esac;

  -- Process 2 push return value
  next(p2_ret_push) := case
    p1_modified : FALSE; -- if process 1 modified, push failed
    p2_pc = 2 & p2_op = 0 & top_pointer = 0 : TRUE;  -- push succeeded (to empty stack)
    p2_pc = 2 & p2_op = 0 & top_pointer > 0 : FALSE; -- push failed (stack not empty)
    TRUE : p2_ret_push;
  esac;

DEFINE
  -- Thread 1 operation predicates
  p1_push_invoked := (p1_op = 0) & (p1_pc = 1);  -- executing push
  p1_pop_invoked  := (p1_op = 1) & (p1_pc = 1);  -- executing pop

  -- Thread 2 operation predicates  
  p2_push_invoked := (p2_op = 0) & (p2_pc = 1 | p2_pc = 2);  -- executing push
  p2_pop_invoked  := (p2_op = 1) & (p2_pc = 1 | p2_pc = 2);  -- executing pop

  -- Combined operation predicates
  invoked_push := (p1_push_invoked | p2_push_invoked);
  invoked_pop  := (p1_pop_invoked | p2_pop_invoked);

  -- Return predicates
  returning_push := (p1_op = 0 & p1_pc = 0) | (p2_op = 0 & p2_pc = 0);
  returning_pop  := (p1_op = 1 & p1_pc = 0) | (p2_op = 1 & p2_pc = 0);

  -- Success return predicates
  push_return := (p1_ret_push) | (p2_ret_push);
  pop_return  := (p1_ret != 0) | (p2_ret != 0);

The HyperLTL formula(s)¶

Linearizability compares the operation histories of a concurrent execution with those of a sequential witness. If every step of the histories aligns, the concurrent execution is considered correct; any divergence reveals a violation.

\[\varphi_{\text{lin}} = \forall \pi_A.\exists \pi_B.\ \Box\left( \mathit{history}_{\pi_A} \leftrightarrow \mathit{history}_{\pi_B} \right)\]

Forall A . Exists B .
G((invoked_pop[A]=invoked_pop[B])&(returning_pop[A]=returning_pop[B])&(pop_return[A]=pop_return[B])&
(invoked_push[A]=invoked_push[B])&(returning_push[A]=returning_push[B])&(push_return[A]=push_return[B]))

References¶

[Tre86] R. K. Treiber. Systems programming: Coping with parallelism. IBM Technical Report RJ 5118, 1986.

[HW90] M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 12(3):463–492, 1990.