Article Preview
TopIntroduction
A concurrent program with nondeterminism is intuitively associated with probability. A concurrent program can be nondeterministic in that races may exist in the program, each of which usually arises when separate threads are scheduled to execute sequentially on a single processor. When it happens, the execution steps of threads can be interleaved. Thus using an input to repeatedly execute the program can produce various program paths, each of which represents a sequence of program instructions executed.
A weak assumption is that the frequencies of all potential paths are uniformly distributed. For example, in the sample program shown in Figure 1, the 
thread spawns the threads 
and 
. Note that a data race exists in the program in the sense that after the program is executed, 
can either be 
or 
, and 
can either be 
or 
. Let the two threads 
and 
be executed in an interleaving manner, and each program statement be executed in an atomic manner. Six potential orders of the statements can be enumerated to represent six execution paths, each of which is denoted by using a sequence of pairs. A pair, say 
, is composed of a thread 
and a statement 
.
Figure 1. A simple program of two threads
Let 
be the total number of program paths in the program, and 
be the probability of a path 
. The weak assumption denotes that the frequencies of all execution paths are uniformly distributed, i.e.,
In this example, we have 
. However, the assumption is usually not true in practice. Running of the program for a number of times can inevitably find a fact that some program paths can be executed more frequently than the others.