Timer, Failure, and Shared Memory

We also describe how to model system's interaction with an OS Timer Timer, and how to model injecting node failures in the system Failure Injector. These models are used in the Two Phase Commit, Espresso Machine, and Failure Detector models.

P is a purely messaging passing based programming language and hence does not support primitives for modeling shared memory based concurrency. But one can always model shared memory concurrency using message passing. We have used this style of modeling when checking the correctness of single node file systems. Please check out shared memory project on how to model shared memory concurrency using P.