P Semantics

Before getting started with the tutorials, we provide a quick informal overview of the P language semantics so that the readers can keep it at the back of their mind as they walk through the tutorials and the language manual.

P is a programming language. P is a state machine based programming language and hence, just like any other imperative programming language it supports basic data types, expressions, and statements that enable programmers to capture complex distributed systems protocol logic as a collection of event-handlers or functions (in P state machines).

P State machines. The underlying model of computation for P state machines is similar to that of Gul Agha's Actor-model-of-computation (wiki). A P program is a collection of concurrently executing state machines that communicate with eachother by sending events (or messages) asynchronously. Each P state machine has an unbounded FIFO buffer associated with it. Sends are asynchronous, i.e., executing a send operation send t,e,v; adds event e with payload value v into the FIFO buffer of the target machine t. Each state in the P state machine has an entry function associated with it which gets executed when the state machine enters that state. After executing the entry function, the machine tries to dequeue an event from the input buffer or blocks if the buffer is empty. Upon dequeuing an event from the input queue of the machine, the attached handler is executed which might transition the machine to a different state. We will provide more details about the P state machines in tutorials as well as the language manual. For detailed formal semantics of P state machines, we refer the readers to the original P paper and the more recent paper with updated semantics.

There are two main distinctions with actor model of computation: (1) P adds the syntactic sugar of state machines to actors, and (2) each state machine in P has an unbounded FIFO buffer associated with it instead of an unbounded bag in actors (semantic difference).

[Important] Send semantics in P

Sends are reliable, buffered, non-blocking, and directed (not broadcast). Sends are reliable i.e., executing a send operation in P adds an event into the target machines buffer. Hence, if one wants to model message loss it has to be modeled explicitly (discussed in the Failure Detector example in the tutorial). Similarly, as P state machine buffers are FIFO, events are dequeued at the state machine in the causal order in which they were sent. Note that events that are sent by two different concurrent machines will be interleaved by the checker and hence, will appear in different order at the target machine but the events sent by the same machine will always appear in the same order at the target state machine. So, just like message loss, arbitrary message re-ordering also has to be explicitly modeled in P (explained in the Paxos example in the tutorials). In general, we find that re-ordering messages/events coming from the same machine is not important and does not lead to any interesting behaviors. More interesting behaviors happen because of interleaving of messages across different state machines which the P checker explores automatically.

Summary, by default, the communication between state machines using send operation follows the above semantics. If you would like to check your system correctness against an arbitrarily network then one would have to model the corresponding send semantics in P explicitly. One can then make the arbitrarily network behave as expected with message duplicates, loss, re-order, etc.

If you have any further doubts related to this topic and modeling network semantics when reasoning using P, feel free to get in touch with Ankush Desai. We have several examples of such cases.

[Important] New semantics in P

State machines in P can be dynamically created during the execution of the Program using the new primitive. Creation of a state machine is also an asynchronous, non-blocking operation.

P Monitors. Specifications in P are written as global runtime monitors. These global monitors observe the execution of the system and can assert any global safety or liveness invariants on the system. Note that the monitors are synchronously composed with the P state machines. Details are explained in the language manual and we provide examples in the tutorial.

When reasoning about the correctness of a distributed system, it is really important to specify both safety as well as liveness specifications.

Always specify both safety and liveness specifications

Only specifying safety property for a system is not enough, this is mainly because, a system model may be incorrect and in the worst case drop all requests on to the ether and not perform any operation. Such a system trivially satisfies all correctness specifications! Hence, it becomes essentially to combine that safety property with liveness properties to check that the system is making progress and servicing the requests. Running the checker on models that have both safety and liveness properties ensure that for all executions explored by the checker, requests are eventually serviced by the system (by sending responses potentially) and all the responses sent by the system satisfy the desired correctness safety specification. This helps ensure that your models are not doing something trivially incorrect like always doing nothing , in which case running the checker on such a model adds no value.

P Checker. The P Checker explores different possible behaviors of the P program arising out of: (1) concurrency: different interleavings of events from concurrently executing state machines as well as (2) data nondeterminism: different data input choices in the P program modeled using the choose (see) operation. The P checker explores different executions of the system that can happen because of these two forms of nondeterminism and asserts that for each of these executions the system satisfies the desired properties specified by the P Monitors.