MTA MSli

MTA-MSli

SVF's MTA module provides sparse flow-sensitive pointer analysis for multithreaded programs, as described in Sparse Flow-Sensitive Pointer Analysis for Multithreaded Programs by Yulei Sui, Peng Di, and Jingling Xue, published at CGO 2016. Building on MTA, MSli computes separate on-demand slices for interleaving/lock analysis (ILA) and flow-sensitive pointer analysis (FSPTA), then runs the main analysis over the retained program state. MSli is presented in Multi-Stage On-Demand Program Slicing for Modular Analysis of Multi-Threaded Programs by Jiawei Yang, Xiao Cheng, Jiawei Wang, Xiapu Luo, and Yulei Sui, published at ISSTA 2026.

Benchmarks

Ready-to-run LLVM bitcode inputs for MTA analysis are available in the MTA-Benchmarks repository. Clone the repository alongside SVF:

git clone https://github.com/JoelYYoung/MTA-Benchmarks.git

Build MTA

Clone and build SVF from its official repository:

git clone https://github.com/SVF-tools/SVF.git
cd SVF
bash ./build.sh

After modifying the MTA implementation, rebuild only the analyzer:

cmake --build Release-build --target mta -j

The resulting executable is Release-build/bin/mta.

Large inputs may require a high-memory server and several hours to finish.

Run MTA

Run MSli on an LLVM bitcode file:

Release-build/bin/mta \
  -mta-enable-slicing=true -max-cxt=3 \
  ../MTA-Benchmarks/benchmarks/gvmd.bc

To run the analysis without slicing:

Release-build/bin/mta \
  -mta-enable-slicing=false -max-cxt=3 \
  ../MTA-Benchmarks/benchmarks/gvmd.bc

Add -stat to print phase timing, slice statistics, and the machine-readable result digest.