  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.
