A provably correct, non-deadlocking parallel event simulation algorithm

This paper first summarizes and then presents a formal proof to a new conservative deadlock-free algorithm, YADDES, for asynchronous discrete event simulation. The proof not only makes the algorithm complete but helps 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 data 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