Skip to content

Timer, Failure, and Shared Memory

Common: Timer, Failure Injector, and Shared Memory

The tutorials use several reusable P models for common system components. These are located in Tutorial/Common.

Timer

The Timer model captures a system's interaction with an OS timer. It is used in the Two Phase Commit, Espresso Machine, and Failure Detector examples.

Failure Injector

The Failure Injector model allows injecting node failures into the system during model checking. It is used in the Two Phase Commit and Failure Detector examples.

Shared Memory

P is a purely message-passing based programming language and does not support primitives for modeling shared memory concurrency. However, shared memory concurrency can always be modeled using message passing.

The Shared Memory example demonstrates this approach, which has been used when checking the correctness of single-node file systems.