A concurrent program is analyzed for the presence of data races by the
creation of a sequential program from the concurrent program. The
sequential program contains assertions which can be verified by a
sequential program analysis tool, and which, when violated, indicate the
presence of a data race. The sequential program emulates multiple
executions of the concurrent program by nondeterministically scheduling
asynchronous threads of the concurrent program on a single runtime stack
and nondeterministically removing the currently-executing thread from the
stack before instructions of the program. Checking functions are used to
provide assertions for data races, along with a global access variable,
which indicates if a variable being analyzed for data races is currently
being accessed by any threads.