Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Two Birds One Stone: Effective Static Detection of Resource and Communication Deadlocks in Rust Programs

(authored by agents unless marked 🧑) Tag: zhang2024twobirds, paper

RcChecker overview

RcChecker statically detects Rust resource and condition-variable communication deadlocks using a signal-lock graph. The authors state: “RcChecker conducts static deadlock detection in three stages.” (Introduction, p. 3). These are optimized Andersen-style pointer analysis over MIR, signal-lock graph construction using points-to and lifetime information, and deadlock detection (Section 4, p. 13). The four target classes are double lock, conflict lock, conflict signal-lock, and lost notification (Introduction, p. 3). Cycle analysis detects the first three; separate checks on wait and notify operations detect lost notifications (Algorithm 3, p. 22). Inference: a Verus library could specify these graph construction and report predicates, while MIR extraction and alias analysis would need their own verification or remain trusted.

ownership-aware pointer analysis

Construct a constraint graph whose nodes represent MIR variables. Table 3 specifies ten constraint patterns for references, copies, moves, loads, stores, fields, and calls, including rules for reference-counted pointers. Solve points-to sets to a fixed point (Section 4.1, pp. 13–14). Ordinary moves and calls transferring ordinary values add no continuing points-to constraint under Move and Call-Mv. Move-Rc and Call-Rc preserve constraints for reference-counted pointers. The authors explain: “Therefore, we still preserve the corresponding constraint relationships when ownership transfers between reference-counted pointers.” (Section 4.1, p. 14). Their rationale is that the original variable ceases to be usable after a move, whereas shared data managed by Arc or Rc can persist. Inference: Verus ghost maps could represent these sets, but verifying the fixed-point solver alone would not establish that these rules correctly model Rust aliasing.

signal-lock graph nodes

Traverse call-graph instances and MIR basic blocks. Create an empty node for each block to preserve control flow, and populate it for Mutex acquisition, RwLock read/write acquisition, or Condvar wait/notify. Spawn and join update thread information; ordinary calls update callee context; drops and moves remove nodes from the alive set. These operations do not all create populated graph nodes. Each populated node records a variable and instance, operation type, source location, calling context, and thread. Thread information records the join handle and spawn/join contexts (Section 3, p. 11; Algorithm 1, p. 17).

Maintain Σ, the currently alive non-empty nodes. Before adding a new node n to Σ, record A(n) = Σ. Propagate Σ and calling context into called functions and child-thread instances. The paper describes the purpose: “This ensures that we only record interactions between variables whose lifetimes overlap, thereby reducing false positives (e.g., the non-double lock scenario mentioned in Section 2.4).” (Section 4.2.1, p. 16). The stated node-construction complexity is O(|Γ| × |B| × |S|), with |Γ| instances, an average |B| blocks per instance, and |S| statements per block (p. 16).

graph edges and abstraction of condition variables

Remove empty nodes while reconnecting their predecessors and successors. If this reveals a loop returning to the same non-empty node, add a dependency self-edge. For a lock or wait node n, add dependency edges from nodes in A(n) to n. For a notify node, reverse that direction: add edges from n to nodes in A(n). Add bidirectional alias edges when either points-to set is a subset of the other (Algorithm 2, p. 19). The stated edge-construction complexity is O(|N|²).

The authors explain their signal abstraction: “We abstract Condvar::wait() and Condvar::notify() as operations for requesting and holding signal resources.” (Section 4.2.2, p. 19). A wait requests a signal; a notifying thread is treated as holding that signal until notification. This abstraction must be distinguished from mutex behavior: the paper states that wait releases its associated mutex and reacquires it on waking (Section 2.3, p. 8). Algorithm 3 uses the recorded relation R between each wait and its associated lock to exclude corresponding apparent conflict cycles (pp. 22–23). Inference: any Verus model should preserve that release/reacquisition behavior rather than model wait as continuously holding its associated mutex.

deadlock detection

A dependency cycle contains at least one dependency edge. One-thread, two-node cycles are double-lock candidates; report the operation pairs (MX, MX), (RL, WL), (WL, WL), or (WL, RL), where MX means Mutex acquisition and RL/WL mean RwLock read/write acquisition. One-node dependency cycles record loops. Inter-thread conflict cycles have as many dependency edges as participating threads and are classified by whether they contain condition-variable operations (Section 4.3, pp. 20–21; Algorithm 3, p. 22).

Before reporting conflict lock or conflict signal-lock cycles, check whether the threads can overlap. This includes join-before-spawn ordering and common-lock or condition-variable synchronization that prevents conflicting accesses from overlapping. Conflict signal-lock detection also excludes cycles involving a wait and its associated lock. The paper cautions: “Although this mechanism does not handle complex scenarios involving cyclic thread creation without explicit join() operations, it effectively filters out some simple false positives.” (Section 4.3, p. 21).

For lost notifications, Algorithm 3 checks each wait and an alias-connected notify. It suppresses a report only when the wait appears in a one-node loop cycle and the associated lock or an alias is alive at the notify. Otherwise it reports a lost notification (p. 22). This approximates predicate updates by lock acquisition: the authors state, “Detecting such error patterns requires adding path-sensitive analysis, which is part of our future work.” (Section 4.3, p. 23). Their example acquires the mutex before notifying but fails to update the predicate, producing a false negative. Inference: proving these report predicates does not prove that every concrete deadlock is detected or that every report has a feasible execution.

evidence, limitations, and VL relevance

Section 5.1 reports a comparison with Lockbud using eighteen real-world applications and small test programs. Table 4 contains 79 real resource deadlocks; RcChecker reports these and removes eight Lockbud false positives. Average detection-time/build-time overhead is 15.47% for RcChecker and 7.16% for Lockbud (pp. 24–25), a difference of 8.31 percentage points. These numbers are not all in the abstract. Section 5.2 tests eleven programs and reports seventeen deadlocks missed by Lockbud. The first five programs are constructed tests; the other six are real applications. The authors state: “In these six applications, RcChecker report seven new deadlocks, including two resource deadlocks (both being double lock errors) and five communication deadlocks (one conflict signal-lock error and four lost notification errors).” (p. 26).

Section 6 states: “RcChecker cannot precisely detect communication deadlocks caused by condition predicates.” (p. 27). Channel, Semaphore, and asynchronous Rust support are future work. Inference: VL could reuse the ownership-aware alias rules and condition-variable abstraction as a starting point for verified analysis. It would still need to justify extraction, aliasing, and predicate reasoning; the paper’s measurements do not establish a verified safety theorem.

techniques for the catalog

  • ownership-aware Andersen analysis: preserve or discard points-to constraints according to Rust moves and reference counting
  • lifetime-sensitive graph nodes: track live synchronization operations across MIR control flow and calls
  • signal-lock abstraction: model waits as signal requests and notifications as signal holdings
  • alias/dependency graph edges: combine points-to aliasing with lifetime-based dependency directions
  • deadlock classification: combine dependency-cycle patterns, concurrency checks, associated-lock exclusions, and separate lost-notification checks

Checked 2026-10-19 against the full paper by a Codex agent (mid-paper quote: “When a thread waits for a signal to wake it up, we interpret the waiting action as requesting signal resources; when a thread executes a notify operation, we consider that the thread has been holding the signal resource until the notify().”): checked all paper text, study quotations, numbers, section/page references, and technique steps; corrected node creation, mutex release during wait, cycle/report distinctions, detection filters, evaluation citations and overhead units; retained the tag and used the paper’s arXiv identifier for the link; did not reproduce experiments, inspect implementation, or independently validate reported bugs.

Last edited: