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 < b$ or $b < a$. (The events on the same thread form a total order given by the sequential semantics of the programming language.) Synchronization events (these could be mutex acquires and releases, for example), give an additional inter-thread happens-before partial order. (If thread $S$ releases a mutex and then thread $T$ acquires that mutex we say that the release happens-before the acquire.)
Then given two data accesses (reads or writes to variables that are not synchronization variables) $a$ and $b$ that are to the same memory location, but by different threads and where either $a$ or $b$ is a write operation we say that there is a data-race between $a$ and $b$ if neither $a < b$ nor $b < a$.
The C++11 standard is a good example. (The relevant section is 1.10 in the draft specs that are available online.) C++11 distinguishes between synchronization objects (mutexes, and variables declared with an
atomic<> 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.