Execution replay of parallel procedural programs

This article describes an execution model for the parallel procedural programming paradigm, which combines multithreading and communications. The model is used to prove sufficient conditions to guarantee the equivalence between two executions of the same program. An efficient mechanism for recording and replaying deterministically parallel procedural programs is derived from the model and implemented in a prototype. Performed on the prototype, systematic measurements of the time overhead of recording traces for replaying various program models indicate that this overhead remains very low.