Checking Race Freedom Via Linear Programming

The authors present a new static analysis for race freedom and race detection. The analysis checks race freedom by reducing the problem to (rational) linear programming. Unlike conventional static analyses for race freedom or race detection, their analysis avoids explicit computation of locksets and lock linearity/must-aliasness. Their analysis can handle a variety of synchronization idioms that more conventional approaches often have difficulties with, such as thread joining, semaphores, and signals. They achieve efficiency by utilizing modern linear programming solvers that can quickly solve large linear programming instances.