A race condition graph for concurrent program behavior

There are race conditions in concurrent programs if the accesses to a sharing resource are not properly synchronized. Because the races can cause the program to behave in unexpected ways, detecting them is an important aspect of debugging and program verification. Many approaches have been used to detect race conditions, but there still is no effective formal model to visualize the race conditions and program interactions. In this paper, we present a formal graph, named race condition graph (RCG), to represent race conditions in concurrent programs. Some characteristics of RCG are presented and the potential RCG (PRCG) as well as the data structure is discussed. Finally, a dining philosopher program is used as a case study.