Is it possible to prove thread safety?

Given a program consisting of variables and instructions which modify these variables, and a synchronization primitive (a monitor, mutex, java's synchronized or C#'s lock), is it possible to prove that such a program is thread safe?

Is there even a formal model for describing things like thread safety or racing conditions?

Proving that a program is "thread safe" is hard. It is possible, however, to concretely and formally define the term "data race." And it is possible to determine whether an execution trace of a specific run of a program does or does not have a data race in time proportional to the size of the trace. This type of analysis goes back at least to 1988: Barton P. Miller, Jong-Deok Choi, "A Mechanism for Efficient Debugging of Parallel Programs", Conf. on Prog. Lang. Dsgn. and Impl. (PLDI-1988):135-144.

Given a trace of an execution we first define a happens-before partial-order between events in the trace. Given two events $a$ and $b$ that occur on the same thread then $a ` type) and all other data. The C++11 spec says that the programmer can reason about the data accesses on a trace of a multithreaded program as if it were sequentially consistent if the data accesses are all data-race free.

The Helgrind tool (part of Valgrind) performs this kind of happens-before based data-raced detection as do several commercial tools (e.g., Intel Inspector XE.) The algorithms in modern tools are based on keeping vector clocks associated with every thread and synchronization object. I think this technique of using vector clocks for data-race detection was pioneered by Michiel Ronsse; Koen De Bosschere: "RecPlay: a fully integrated practical record/replay system", ACM Trans. Comput. Syst. 17(2):133-152, 1999.

StackExchange Computer Science Q#14356, answer score: 12