Programmers can write safety and liveness specifications in P as monitors or
spec machines are monitor state machines or observer state machines that observe a set of events during the execution of the system and
assert the desired correctness specifications based on these observations.
Machines vs Spec Machine
Syntactically, machines and spec machines in P are very similar in terms of the state machine structure. But, they have some key differences:
specmachines in P are observer machines (imagine runtime monitors), they observe a set of events in the execution of the system and based on these observed events (may keep track on local state) assert the desired global safety and liveness specifications.
specmachines are observer machines, they cannot have any side effects on the system behavior and hence,
specmachines cannot perform
specmachines are global machines, in other words, there is only a single instance of each monitor created at the start of the execution of the system. We currently do not support dynamic creation of monitors. Hence,
specmachines cannot use
specmachines are synchronously composed with the system that it is monitored. The way this is achieved is: each time there is a
announceof an event during the execution of a system, all the monitors or specifications that are observing that event are executed synchronously at that point. Another way to imagine this is: just before
annouceof an event, we deliver this event to all the monitors that are observing the event and synchronously execute the monitor at that point.
specmachines can have
coldannotations on their states to model liveness specifications.
P Spec Machine Grammar
specMachineDecl : spec iden observes eventsList statemachineBody ;
As mentioned above, syntactically, the P
spec machines are very similar to the P state machines. The main difference being the
observes annotation that specifies the list of events being observed (monitored) and also the
cold annotations on the states of a liveness specification.
spec iden observes eventsList statemachineBody ;
iden is the name of the spec machine,
eventsList is the comma separated list of events observed by the spec machine and the
statemachineBody is the implementation of the specification and its grammar is similar to the P state machine.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
The above specification checks a very simple global invariant that all
eRequest events that are being sent by clients in the system have a globally monotonically increasing
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
The above specification checks the global liveness property that every event
eRequest is eventually followed by a corresponding successful
eResponse event. The key idea is that the system satisfies a liveness specification if at the end of the execution the monitor is not in a hot state (line 13). The programmers can use
hot annotation on states to mark them as intermediate or error states. Hence, properties like
eventually something holds or
every event X is eventually followed by Y or
eventually the system enters a convergence state, all such properties can be specified by marking the intermediate state as
hot states and the checker checks that all the executions of the system eventually end in a non-hot state. If there exists an execution that fails to come out of a hot state eventually then it is flagged as a potential liveness violation.
Details about the importance of liveness specifications is described here. For several examples of liveness properties, please check the specifications in the tutorial examples.