Modern mainstream programming languages like Java and C# support multi- threading as an essential feature of the language. In these languages multiple threads can access shared objects. Moreover, synchronization mechanisms exist for controlling access to shared objects by threads. If every access to a shared object by any thread requires prior acquisition of a common lock, then the program is guaranteed to be “properly synchronized”. On the other hand, if there are two accesses to a shared object/variable v by two different threads, at least one of them is a write, and they are not ordered by synchronization — the program is then said to contain a data race, that is, the program is improperly synchronized. Improperly synchronized programs are common for more than one reason — (a) programmers may want to avoid synchronization overheads for low-level program fragments which are executed frequently, (b) programmers may forget to add certain synchronization operations in the program, or (c) programmers forget to maintain a common lock guarding accesses to some shared variable v since there are often many lock variables in a real-life program.

Problem Statement The work in this paper deals with formal verification (and subsequent debugging) of multi-threaded C# programs which are improperly synchronized. As a simple example consider the following schematic program fragment, and suppose initially x = y = 0. Moreover l1, l2 are thread-local variables while x, y are shared variables.
x = 1;
y = 1;
l1 = y;
l2 = x;
If this program is executed on a uni-processor platform, we cannot have l1 = 1, l2 = 0 at the end of the program. However, on a multiprocessor platform which allows reordering of writes to different memory locations this is possible. On such a platform, the writes to x, y may be completed out-of-order. As a result, the following completion order is possible ?y = 1, l1 = y, l2 = x, x = 1?.

Download pdf A Memory Model Sensitive Checker for C#