[Solved]: Is it possible to prove thread safety?

Problem Detail: 

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?

Asked By : Emiswelt

Answered By : Wandering Logic

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/14356