Abstract by Seth Poulsen
3M Static Data Race Detection with Abstract Interpretation
In modern computing, processors run multiple sections of code (threads) simultaneously. A data race occurs when the order in which threads access shared data affects the output of the program. Data races are not merely a theoretical problem; they occur in real world programs and cause elusive bugs. We seek to prove absence of data races from structured concurrent programs. Standard data-race detection uses a happens-before relation. We have distilled this relation into a computation graph to greatly reduce the number of schedules that need to be checked to prove data race freedom. Our current model reasons over all possible schedules of a program, but with a fixed input. We seek to expand this, using abstract interpretation, to reason over all schedules of a program with any input.