Race analysis of traces of asynchronous message-passing programs

An execution of a message-passing program is nondeterministic if message races exist. In this paper, a formal definition of a message race for asynchronous communication is presented. The trace of an execution of a message-passing program is a sequence of send and receive events. For a receive event r in a trace T, its race set is the set of messages in T that have a race with the message received at r and can be received at r during some possible executions of the same program with the same input. A race analysis algorithm analyzes a trace to determine the race set for each receive event in the trace. Three race analysis algorithms are given for three different types of sequences of send and receive events. It is shown that these race analysis algorithms can be used to solve a number of problems in testing and debugging message-passing programs