"Even though in reality processes may run in parallel, we do not need to model this parallelism since the only communication between processes is by sending and

"Even though in reality processes may run in parallel, we do not need to model this parallelism since the only communication between processes is by sending and receiving messages, and we can assume that a process finishes processing one event before starting to process the next event. Every parallel execution is therefore equivalent to some linear sequence of execution steps. Other formalisations of distributed systems, such as the TLA+ language, also use such a linear sequence of steps." Ha-hah! Proving that you can treat "processing one event" as globally atomic was the funnest thing in grad school.