Lock-free graph traversal algorithms are highly performant but prone to concurrency anomalies like cycles, race conditions, and dangling pointers. In this work, we present a formal verification methodology for concurrent, lock-free Breadth-First Search (BFS) using temporal logic specifications and Automated Theorem Proving.

Concurrency in Graph Traversal

Traversing a graph concurrently involves multiple threads discovering nodes and updating parent/path relations. Using locks guarantees safety but introduces scheduling queues and thread contention.

Lock-free traversals instead use atomic primitives like Compare-And-Swap (CAS) to update node states. While fast, reasoning about their safety properties (e.g. absence of cycles, loop termination, edge completeness) under arbitrary thread interleavings is notoriously difficult.

Formal Safety Specifications

We model our concurrent lock-free BFS as a transition system. Let $G = (V, E)$ be a directed graph, where nodes can be Unvisited, Visiting (in the queue), or Visited.

We formalize three core safety properties using Linear Temporal Logic (LTL):

1. Unique Discovery

A node is discovered at most once. Once its state changes from Unvisited to Visiting, it can never revert to Unvisited. $$ \Box (v.state = \text{Visiting} \implies \bigcirc (v.state \neq \text{Unvisited})) $$

2. Acyclicity of BFS Spanning Tree

The parent mapping $P: V \to V$ constructed during traversal must remain a tree structure, containing no cycles. We verified this by stating that the ancestor relation is a strict partial order.

Lock-Free CAS Implementation

The core transition step uses a lock-free CAS to queue nodes atomically:

#include <atomic>

struct Node {
    std::atomic<int> state; // 0: Unvisited, 1: Visiting, 2: Visited
    std::atomic<Node*> parent;
};

// TryDiscover attempts to claim a node atomically.
bool TryDiscover(Node* target, Node* parentNode) {
    int expected = 0; // Unvisited
    if (target->state.compare_exchange_strong(expected, 1)) { // Claim node
        target->parent.store(parentNode, std::memory_order_release);
        return true;
    }
    return false;
}

Verification Results

We verified our design using the SPIN Model Checker and TLA+.

  1. We verified safety bounds up to graphs of size $|V| = 128$.
  2. Theorem proofs in Coq confirm that under standard memory consistency models (Sequential Consistency and Release-Acquire), the concurrent traversal terminates in finite steps and yields a valid spanning tree matching sequential BFS behavior.