A provably correct, non-deadlocking parallel event simulation algorithm

mechanisms to communicate with each other. This paper first summerizes and then presents a formal proof t o a new conservative deadlock-free algorithm, YADDES [l], for asynchronous discrete event simulation. The proof not only makes the algorithm complete but helps us better understand the seemingly complicated algorithm. YADDES constructs a special acyclic data-flow network from the network of simulation models to keep track of the run time da ta dependencies, which permits a model to be correctly executed as far ahead in time as possible. The data-flow network also uses the asynchronous parallel discrete event driven technique and runs concurrently with the network of simulation models. This paper also reports a preliminary implementation of the algorithm and discusses the algorithm’s limitations.