Execution replay of parallel procedural programs

This article describes an execution model for the parallel procedural progr amming paradigm, which combines multithreading and communications. The mode l is used to prove sufficient conditions to guarantee the equivalence betwe en two executions of the same program. An efficient mechanism for recording and replaying deterministically parallel procedural programs is derived fr om the model and implemented in a prototype. Performed on the prototype, sy stematic measurements of the time overhead of recording traces for replayin g various program models indicate that this overhead remains very low. (C) 2000 Elsevier Science B.V. All rights reserved.