Concurrency Bug Checker

Static analysis tool for detecting concurrency bugs in multithreaded programs, including shared-memory threading bugs plus dedicated OpenMP and MPI protocol checks.

Library Location: lib/Checker/Concurrency/

Headers: include/Checker/Concurrency/

Tool Location: tools/checker/lotus-check-concur.cpp

Frontend: lotus-check --engine=concur

Overview

The concurrency checker analyzes LLVM IR to detect thread safety issues using:

  • MHP (May Happen in Parallel) Analysis – Determines which instructions can execute concurrently

  • Lock Set Analysis – Tracks which locks protect shared memory accesses

  • Happens-Before Analysis – Builds synchronization relationships between threads

  • OpenMP Task Analysis – Tracks task creation, taskgroup/taskwait boundaries, and depend relations

  • MPI Communication Analysis – Tracks point-to-point operations, collectives, requests, and RMA synchronization

Concurrency findings go through the shared BugReportMgr, so they land in the same JSON and SARIF reports as other engines.

Components

ConcurrencyChecker (ConcurrencyChecker.cpp, ConcurrencyChecker.h):

  • Main coordinator that orchestrates all concurrency checks

  • Manages statistics and analysis configuration

  • Integrates with BugReportMgr for centralized reporting

DataRaceChecker (DataRaceChecker.cpp, DataRaceChecker.h):

  • Detects data races using MHP analysis

  • Identifies concurrent memory accesses without proper synchronization

  • Reports bug type: BUG_DATARACE (CWE-362, HIGH importance, ERROR classification)

DeadlockChecker (DeadlockChecker.cpp, DeadlockChecker.h):

  • Detects potential deadlocks using lock set analysis

  • Identifies circular lock dependencies between threads

  • Analyzes lock acquisition order to find cycles

AtomicityChecker (AtomicityChecker.cpp, AtomicityChecker.h):

  • Detects atomicity violations

  • Identifies non-atomic sequences of operations that should be atomic

  • Checks for interleaving of critical sections

OpenMPChecker (OpenMPChecker.cpp, OpenMPChecker.h):

  • Dedicated checker for OpenMP-specific bug patterns

  • Reports unbalanced taskgroup regions

  • Reports unbalanced atomic runtime regions

  • Warns about partial task synchronization through __kmpc_omp_wait_deps

MPIChecker (MPIChecker.cpp, MPIChecker.h):

  • Dedicated checker for MPI-specific protocol and synchronization bugs

  • Reports orphaned non-blocking requests

  • Reports simple blocking communication deadlocks

  • Reports collective mismatches and conditional collectives

  • Reports unsynchronized RMA operations, RMA races, and leaked windows

ConditionVariableChecker (ConditionVariableChecker.cpp):

  • Detects condition variable misuse, such as missing associated locks or lost signals

LockMismatchChecker (LockMismatchChecker.cpp):

  • Detects mismatched lock/unlock operations and conflicting lock types

CUDAChecker (CUDAChecker.cpp):

  • Analyzes CUDA kernel launches, shared memory synchronization, and host-device race conditions

StarvationChecker (StarvationChecker.cpp):

  • Flags potential thread starvation patterns and asymmetric lock acquisition biases

Usage

Basic Usage:

./build/bin/lotus-check --engine=concur input.bc

Enable Specific Checks:

./build/bin/lotus-check --engine=concur input.bc --checks=data-race
./build/bin/lotus-check --engine=concur input.bc --checks=deadlock
./build/bin/lotus-check --engine=concur input.bc --checks=atomicity
./build/bin/lotus-check --engine=concur input.bc --checks=openmp
./build/bin/lotus-check --engine=concur input.bc --checks=mpi

Select Checks with a Comma-Separated List:

./build/bin/lotus-check --engine=concur input.bc --checks=data-race,deadlock,openmp
./build/bin/lotus-check --engine=concur input.bc --checks=mpi

Enable Multiple Checks:

./build/bin/lotus-check --engine=concur input.bc --checks=data-race,deadlock,atomicity

Generate JSON Report:

./build/bin/lotus-check --engine=concur input.bc --report-json=report.json

Generate SARIF Report:

./build/bin/lotus-check --engine=concur input.bc --report-sarif=report.sarif

Command-Line Options

  • --checks=<id[,id...]> – Select data-race, deadlock, atomicity, condvar, lock-mismatch, starvation, openmp, mpi, or cuda. Omitting this option, or passing --checks=all, enables all checks.

  • --concur.mode=<check|analysis> – Run analyses and bug checkers (default: check) or emit analysis facts (analysis)

  • --concur.output=<file> – Write analysis facts to a file in analysis mode

  • --concur.output-format=<text|json> – Select the analysis-fact format (default: text)

  • --concur.sparse-flow-sensitive – Refine data-race alias pairs with a thread-aware sparse flow-sensitive solve

  • --concur.msli – Run multi-stage synchronization and points-to slicing before sparse race refinement

  • --concur.memory-partition=<distinct|intra-disjoint|inter-disjoint> – Sparse MemorySSA region policy (default: inter-disjoint)

  • --concur.thread-context=<depth> – Maximum call-string depth in thread creation tree (default: 2)

  • --concur.points-to-sets=<mutable|hash-consed> – Sparse solver points-to set backend (default: mutable)

  • --concur.starvation-blocking-functions=<fn1,fn2...> – Additional blocking function names for starvation checking

  • --report-json=<file> – Output JSON report to file

  • --report-sarif=<file> – Output SARIF report to file

  • --report-min-score=<n> – Minimum confidence score for reporting (0-100)

Starvation

The Infer-inspired Starvation checker summarizes critical pairs: a potentially blocking operation, arbitrary callback, or lock acquisition together with the locks held at that event. Summaries propagate events, lock acquisitions and definite releases through direct calls, with formal-to-actual lock projection and call traces. It reports blocking calls and unresolved indirect callbacks while locks may be held. Condition-variable waits release their associated mutex during the wait, so holding only that mutex does not produce a finding. Recognized RAII destructors release their underlying locks, and local try-lock failure paths use the lockset service’s branch refinement. Try-lock acquisition itself is treated as nonblocking on UI-thread entry points.

./build/bin/lotus-check --engine=concur --checks=starvation input.bc
./build/bin/lotus-check --engine=concur --checks=starvation,deadlock \
  --concur.starvation-blocking-functions=wait_for_reply,blocking_io input.bc

Built-in blocking models include sleep, socket receive/accept, read, polling, semaphore wait and thread join APIs. Clients may add models through ConcurrencyChecker::addStarvationBlockingFunction(). LLVM function attributes provide additional contracts:

  • "lotus.may-block" marks a blocking callee.

  • "lotus.arbitrary-code" marks a callee that may execute callbacks.

  • "lotus.ui-thread" marks a UI-thread entry point, where blocking calls and blocking lock acquisitions are reported.

  • "lotus.lockless" marks an entry point that must not acquire locks.

UI-thread and lockless contracts propagate into callee events. Source-level annotations need a frontend to preserve these contracts as LLVM attributes. Deadlock cycles remain available through the existing deadlock check.

This is an experimental LLVM adaptation. Summary construction uses at most 32 whole-module iterations and retains call traces of up to 16 frames. Branch joins approximate possible held locks, so reports are potential violations. Lock recursion, arbitrary executor scheduling, Android strict-mode semantics and unresolved indirect-callee summaries are not modeled. Exceptional lock effects are approximated using the same summary as normal return. Custom blocking models should describe operations that can actually wait; calls known to be nonblocking can otherwise produce unnecessary findings.

Scope

concur is the dedicated engine for shared-memory, OpenMP, and MPI concurrency errors. Its --checks option selects only concurrency checker families; it does not enable memory-safety, numerical, or taint engines. See Choosing a Checker for the complete checker guide.

Bug Types

Data Races (BUG_DATARACE):

  • Description: Concurrent access to shared memory without proper synchronization

  • CWE: CWE-362

  • Importance: HIGH

  • Classification: ERROR

  • Detection: MHP analysis identifies instructions that may execute in parallel and access the same memory location without locks

Deadlocks:

  • Description: Circular lock dependencies between threads that can cause threads to wait indefinitely

  • Detection: Lock set analysis identifies cycles in lock acquisition order

  • Analysis: Tracks lock acquisition sequences across threads

Atomicity Violations:

  • Description: Non-atomic sequences of operations that should be atomic

  • Detection: Identifies critical sections that can be interleaved incorrectly

  • Analysis: Checks for proper synchronization around related operations

OpenMP Bugs:

  • Taskgroup mismatch: Detects __kmpc_taskgroup / __kmpc_end_taskgroup imbalance

  • Atomic region mismatch: Detects __kmpc_atomic_start / __kmpc_atomic_end imbalance

  • Partial task synchronization: Warns when __kmpc_omp_wait_deps may leave sibling tasks unsynchronized

MPI Bugs:

  • Orphaned request: Non-blocking request without a matching Wait/Test/Request_free/Cancel

  • Blocking deadlock: Simple cycles involving blocking send/receive pairs

  • Collective mismatch: Incompatible collective operations across ranks

  • Conditional collective: Collectives that may execute only on a subset of ranks

  • Unsynchronized RMA / RMA race: One-sided accesses without proven synchronization

  • Leaked window: Window created but not freed

Analysis Process

  1. Parse LLVM IR: Load module and identify concurrency primitives (threads, locks, synchronization)

  2. Build MHP Graph: Determine which instructions may happen in parallel

  3. Lock Set Analysis: Track which locks protect each memory access

  4. Happens-Before Analysis: Build synchronization relationships (mutexes, barriers, etc.)

  5. Pattern Detection: Identify shared-memory, OpenMP, and MPI-specific bug patterns

  6. Report Generation: Generate reports through centralized BugReportMgr

Programmatic Usage

#include "Checker/Concurrency/ConcurrencyChecker.h"
#include "Checker/Framework/BugReportMgr.h"

using namespace concurrency;

// Create checker
ConcurrencyChecker checker(*module);

// Configure checks
checker.enableDataRaceCheck(true);
checker.enableDeadlockCheck(true);
checker.enableAtomicityCheck(true);
checker.enableOpenMPCheck(true);
checker.enableMPICheck(true);

checker.runAnalyses();

// Run checks (automatically reports to BugReportMgr)
checker.runChecks();

// Get statistics
auto stats = checker.getStatistics();
outs() << "Data Races Found: " << stats.dataRacesFound << "\n";
outs() << "Deadlocks Found: " << stats.deadlocksFound << "\n";
outs() << "Atomicity Violations Found: " << stats.atomicityViolationsFound << "\n";
outs() << "OpenMP Bugs Found: " << stats.openMPBugsFound << "\n";
outs() << "MPI Bugs Found: " << stats.mpiBugsFound << "\n";

// Access centralized reports
BugReportMgr& mgr = BugReportMgr::get_instance();
mgr.print_summary(outs());

Statistics

The checker provides detailed analysis statistics:

  • totalInstructions – Total number of instructions analyzed

  • mhpPairs – Number of instruction pairs that may happen in parallel

  • locksAnalyzed – Number of lock operations analyzed

  • dataRacesFound – Number of data races detected

  • deadlocksFound – Number of deadlocks detected

  • atomicityViolationsFound – Number of atomicity violations detected

  • condVarBugsFound – Number of condition-variable misuse bugs detected

  • lockMismatchesFound – Number of lock mismatch bugs detected

  • openMPBugsFound – Number of OpenMP bugs detected

  • mpiBugsFound – Number of MPI bugs detected

  • starvationBugsFound – Number of blocking/context violations detected

Limitations

  • Conservative Analysis: May report false positives due to over-approximation

  • Protocol Coverage: OpenMP and MPI support focuses on statically recognizable runtime patterns, not full semantic verification

  • Context-Insensitive: Does not distinguish between different call contexts

  • No Dynamic Analysis: Static analysis only, cannot detect runtime-specific issues

Performance

  • Cost is dominated by MHP graph construction, which grows with the number of threads and of shared-memory accesses

  • Lock-set analysis carries the set of locks held at each access, so deeply nested locking increases the per-access state

  • --concur.mode=analysis with --concur.output dumps the analysis facts without running the report path

Integration

The concurrency checker integrates with:

  • BugReportMgr: Centralized bug reporting system

  • LLVM IR: Standard LLVM intermediate representation

  • Sparrow / Dyck Alias Analysis: Pointer analysis for memory access tracking (defaults to context-insensitive SparrowAA)

See Also