Distributed Simulation: A Case Study in Design and Verification of Distributed Programs

TLDR

System simulation is typically performed sequentially because all components share many variables. The authors propose a distributed simulation approach in which processes communicate only via messages with their neighbors, eliminating shared variables and central routing or scheduling. The distributed design uses message passing between neighboring processes, avoids deadlock without global control, requires only limited memory per process, and establishes correctness by proving each component and applying inductive reasoning. Empirical studies show the approach is efficient, and the paper provides formal, detailed proofs of correctness.

Abstract

The problem of system simulation is typically solved in a sequential manner due to the wide and intensive sharing of variables by all parts of the system. We propose a distributed solution where processes communicate only through messages with their neighbors; there are no shared variables and there is no central process for message routing or process scheduling. Deadlock is avoided in this system despite the absence of global control. Each process in the solution requires only a limited amount of memory. The correctness of a distributed system is proven by proving the correctness of each of its component processes and then using inductive arguments. The proposed solution has been empirically found to be efficient in preliminary studies. The paper presents formal, detailed proofs of correctness.