DeadlockScanner: Static Lock-Order Analysis via LLVM IR

DeadlockScanner is an LLVM IR ModulePass that statically detects synchronization bugs (like deadlocks and double-locks) in multithreaded C programs. Currently, the analysis specifically targets POSIX standard mutexes (pthread_mutex_lock and pthread_mutex_unlock). It works by running a forward Data Flow Analysis (DFA) over the Control Flow Graph (CFG) to track mutex states, and builds a lock-order dependency graph to find cycles.

How it works (The Theory)

1. The Dual-Set Lattice

Instead of a simple "locked/unlocked" state machine, DeadlockScanner tracks the state of a thread using two distinct sets at every program point:

• Must-Held Locks: Locks that are held on all possible execution paths reaching the current instruction.
• May-Held Locks: Locks that are held on at least one execution path reaching the current instruction.

This separation is important for avoiding false positives. Definite API violations (like guaranteed double-locks) are checked against the Must-Held set. Potential violations, and the deadlock dependency graph, use the May-Held set to remain conservative.

2. The Join Operator (⊔)

When different control-flow paths merge (e.g., at the end of an if/else block), DeadlockScanner merges the states using the join operator (⊔):

• Must-Held Join: Set Intersection (Greatest Lower Bound). A lock is only must-held if it was must-held on all incoming edges.
• May-Held Join: Set Union. A lock is may-held if it was acquired on any incoming edge.

3. Context-Independent Interprocedural Summaries

To handle function calls without the massive overhead of full context-sensitivity, DeadlockScanner pre-computes a static summary for each function. A function summary records:

• must_acquire_net / may_acquire_net
• must_release_net / may_release_net
• may_acquire_internally (locks acquired at any point inside the function, even if released before returning)

When the DFA hits a call instruction, it simply applies this summary to the caller's current state mathematically.

4. Graph Construction & Cycle Detection

Whenever a lock $L_{target}$ is acquired, a directed edge is drawn from every lock currently in the May-Held set to $L_{target}$. Once the analysis finishes iterating through the module, DeadlockScanner runs a Depth-First Search (DFS) over this graph to find back-edges (cycles). Any cycle is reported as a potential deadlock, along with the source code lines that created each edge.

Repository Structure

• lib/DeadlockScanner/DeadlockScanner.cpp: The core implementation of the ModulePass.
• benchmarks/: A suite of C programs designed to evaluate intra-procedural, inter-procedural, and CFG-branching anomalies.
• build.sh: Wrapper script to configure and compile the LLVM plugin.
• evaluate.sh: Script to compile the benchmark suite into LLVM IR and execute the analysis.

Usage

1. Build the Plugin

./build.sh

2. Evaluate Benchmarks

./evaluate.sh

3. Manual Execution To run DeadlockScanner on a custom C file:

# Compile to IR with debug info (-g)
clang -g -S -emit-llvm -O0 -Xclang -disable-O0-optnone -fno-discard-value-names target.c -o target.ll

# Execute the pass
opt -load-pass-plugin=./build/DeadlockScanner.so -passes=deadlockscanner -disable-output target.ll

---

Disclaimer: The documentation for this repository was assisted by Large Language Models.