Datalog-based Scalable Semantic Diffing of Concurrent Programs

TL;DR

This paper introduces a fast, approximate static analysis method based on Datalog for detecting synchronization differences in multithreaded programs, significantly reducing analysis time compared to traditional model checking.

Contribution

It presents a novel Datalog-based analysis framework that efficiently computes synchronization differences, enabling rapid and accurate comparison of concurrent program behaviors.

Findings

Analysis often completes within seconds

Method matches differences identified by humans

Outperforms model checking by 10x to 1000x in speed

Abstract

When an evolving program is modified to address issues related to thread synchronization, there is a need to confirm the change is correct, i.e., it does not introduce unexpected behavior. However, manually comparing two programs to identify the semantic difference is labor intensive and error prone, whereas techniques based on model checking are computationally expensive. To fill the gap, we develop a fast and approximate static analysis for computing synchronization differences of two programs. The method is fast because, instead of relying on heavy-weight model checking techniques, it leverages a polynomial-time Datalog-based program analysis framework to compute differentiating data-flow edges, i.e., edges allowed by one program but not the other. Although approximation is used our method is sufficiently accurate due to careful design of the Datalog inference rules and iterative increase of the required data-flow edges for representing a difference. We have implemented our method and evaluated it on a large number of multithreaded C programs to confirm its ability to produce, often within seconds, the same differences obtained by human; in contrast, prior techniques based on model checking take minutes or even hours and thus can be 10x to 1000x slower.