# Thread-Modular Static Analysis for Relaxed Memory Models

arXiv: https://arxiv.org/abs/1709.10077 · HTML: https://mlsanity.com/paper/1709.10077/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Sep 2017.

## Built on by (most cited first, 1 of 1)

- [Certifying the Fairness of KNN in the Presence of Dataset Bias](https://mlsanity.com/paper/2307.08722/) (2023)

## Abstract (arXiv)

We propose a memory-model-aware static program analysis method for accurately analyzing the behavior of concurrent software running on processors with weak consistency models such as x86-TSO, SPARC-PSO, and SPARC-RMO. At the center of our method is a unified framework for deciding the feasibility of inter-thread interferences to avoid propagating spurious data flows during static analysis and thus boost the performance of the static analyzer. We formulate the checking of interference feasibility as a set of Datalog rules which are both efficiently solvable and general enough to capture a range of hardware-level memory models. Compared to existing techniques, our method can significantly reduce the number of bogus alarms as well as unsound proofs. We implemented the method and evaluated it on a large set of multithreaded C programs. Our experiments showthe method significantly outperforms state-of-the-art techniques in terms of accuracy with only moderate run-time overhead.