How to use this example
We assume that you have cloned the P repository locally.
git clone https://github.com/p-org/P.git
The recommended way to work through this example is to open the P/Tutorial folder in IntelliJ side-by-side a browser using which you can simultaneously read the description for each example and browse the P program.
To know more about P language primitives used in the example, please look them up in the language manual.
System: We consider a client-server application where clients interact with a bank to withdraw money from their accounts.
The bank consists of two components: (1) a bank server that services withdraw requests from the client; and (2) a backend database which is used to store the account balance information for each client. Multiple clients can concurrently send withdraw requests to the bank. On receiving a withdraw request, the bank server reads the current bank balance for the client and if the withdraw request is allowed then performs the withdrawal, updates the account balance, and responds back to the client with the new account balance.
Correctness Specification: The bank must maintain the invariant that each account must have at least 10 dollars as its balance. If a withdraw request takes the account balance below 10 then the withdraw request must be rejected by the bank. The correctness property that we would like to check is that in the presence of concurrent client withdraw requests the bank always responds with the correct bank balance for each client and a withdraw request always succeeds if there is enough balance in the account (that is, at least 10).
The P models (PSrc) for the ClientServer example consist of four files:
- Client.p: Implements the Client state machine.
[Expand]: Let's walk through Client.p
- (L19 - L22) → Events
eWithDrawRespare used to communicate between the
Servermachines (manual: event declaration).
- (L3 - L17) → Declares the payload types for the
eWithDrawRespevents (manual: user defined type).
- (L25 - L95) → Declares the
Clientstate machine (manual: P state machine).
Clientmachine has a set of local variables used to store the local-state of the state machine (L27 - L31).
Initstate is the start state of the machine where the machine starts executions on being created. The entry function of the
Initstate initializes the local variables based on the parameters received on creation and jumps to the
- In the
WithdrawMoneystate, the state machine checks if there is enough money in the account. If the balance is greater than 10 then it issues a random withdraw request to the bank by sending the
eWithDrawReqevent (L55) otherwise it jumps to the
NoMoneyToWithDrawstate. After sending a withdraw request, the machine waits for the
eWithDrawRespevent (L59). On receiving the
eWithDrawRespevent, the machine executes the corresponding event handler that confirms if the bank response is as expected and also if there is still money in the account then jumps back to the WithdrawMoney state. Note that each time we (re-)enter a state (through a transition or goto statement), its entry function is executed.
- Server.p: Implements the BankServer and the backend Database state machines.
[Expand]: Let's walk through Server.p
- (L1 - L7) → Declares the events used to communicate between the bank server and the backend database.
- (L9 - L48) → Declares the
BankServermachine. The BankServer machine uses a database machine as a service to store the bank balance for all its clients. On receiving an eWithDrawReq (withdraw requests) from a client, it reads the current balance for the account, if there is enough money in the account then it updates the new balance in the database after withdrawal and sends a response back to the client.
- (L50 - L74) → Declares the
Databasemachine. The Database machine acts as a helper service for the Bank server and stores the bank balance for each account. There are two API's or functions to interact with the Database: ReadBankBalance and UpdateBankBalance. These functions are implemented as global functions in P (L76 - L92).
- AbstractBankServer.p: Implements the AbstractBankServer state machine that provides a simplified abstraction that unifies the BankServer and Database machines. We will demonstrate how one can replace the complex bank service (consisting of two interacting components, the BankServer and the Database) by its abstraction when testing the client application.
[Expand]: Let's walk through AbstractBankServer.p
- (L12 - L37) → Declares an abstraction of the BankServer machine. The
AbstractBankServerprovides an implementation of the Bank where the interaction between the BankServer and Database is abstracted away. We use the
AbstractBankServermachine to demonstrate how one can replace a complex component in P with an abstraction that hides a lot of its internal complexity. For the client, it still exposes the same interface or behavior. Hence, when checking the correctness of the client it does not matter whether we pair it with the BankServer or the AbstractBankServer.
To mitigate the state space explosion problem, when modeling and checking complex systems consisting of several components, we would like to check the correctness of each component in isolation. When doing this kind of a compositional reasoning, we replace the environment of the component with its abstraction. The abstraction basically exposes the same interface as the environment but removes its internal complexity, simplifying the overall problem of checking the correctness of the component under test. There is a large body of literature on doing compositional reasoning of distributed systems. You can start with the Modular P paper. How to automatically replace a machine with its abstraction is described below.
- ClientServerModules.p: Declares the P modules corresponding to each component in the system.
[Expand]: Let's walk through ClientServerModules.p
- (L1 - L5) → Declares the
Bankmodules. A module in P is a collection of state machines that together implement that module or component. A system model in P is then a composition or union of modules. The
Clientmodule consists of a single machine
Bankmodule is implemented by machines
Databasetogether (manual: P module system).
- (L7 - L8) → The
AbstractBankmodule uses the
bindingfeature in P modules to bind the
BankServermachine to the
AbstractBankServermachine. Basically, what this implies is that whenever
AbstractBankmodule is used the creation of the
BankServermachine will result in creation of
AbstractBankServer, replacing the implementation with its abstraction (manual: primitive modules).
- BankBalanceIsAlwaysCorrect (safety property): The BankBalanceIsAlwaysCorrect specification checks the global invariant that the account-balance communicated to the client by the bank is always correct and the bank never removes more money from the account than that withdrawn by the client! Also, if the bank denies a withdraw request then it is only because the withdrawal would reduce the account balance to below 10.
- GuaranteedWithDrawProgress (liveness property): The GuaranteedWithDrawProgress specification checks the liveness (or progress) property that all withdraw requests submitted by the client are eventually responded.
Stating that BankBalanceIsAlwaysCorrect checks that "if the bank denies a withdraw request then the request would reduce the balance to below 10 (< 10)" is equivalent to state that "if there is enough money in the account - at least 10 (>= 10), then the request must not error". Hence, the two properties BankBalanceIsAlwaysCorrect and GuaranteedWithDrawProgress together ensure that every withdraw request if allowed will eventually succeed and the bank cannot block correct withdrawal requests.
[Expand]: Let's walk through BankBalanceCorrect.p
- (L20) → Event
eSpec_BankBalanceIsAlwaysCorrect_Initis used to inform the monitors about the initial state of the Bank. The event is announced by the TestDrivers when setting up the system (here).
- (L36 - L86) → Declares the
BankBalanceIsAlwaysCorrectsafety spec machine that observes the events
eSpec_BankBalanceIsAlwaysCorrect_Initto assert the required global invariant.
- (L92 - L115) → Declares the
GuaranteedWithDrawProgressliveness spec machine that observes the events
eWithDrawRespto assert the required liveness property that every request is eventually responded by the Bank.
- To understand the semantics of the P spec machines, please read manual: p monitors.
The test scenarios folder in P has two parts: TestDrivers and TestScripts. TestDrivers are collections of state machines that implement the test harnesses (or environment state machines) for different test scenarios. TestScripts are collections of test cases that are automatically run by the P checker.
[Expand]: Let's walk through TestDriver.p
- (L36 - L60) → Function
SetupClientServerSystemtakes as input the number of clients to be created and configures the ClientServer system by creating the
CreateRandomInitialAccountsfunction uses the
chooseprimitive to randomly initialize the accounts map. The function also
eSpec_BankBalanceIsAlwaysCorrect_Initto initialize the monitors with initial balance for all accounts (manual: annouce statement).
- (L3 - L22) → Machines
TestWithMultipleClientsare simple test driver machines that configure the system to be checked by the P checker for different scenarios. In this case, test the ClientServer system by first randomly initializing the accounts map and then testing it with either one
Clientor with multiple
Clients (between 2 and 4)).
[Expand]: Let's walk through TestScript.p
P allows programmers to write different test cases. Each test case is checked separately and can use a different test driver. Using different test drivers triggers different behaviors in the system under test, as it implies different system configurations and input generators. To better understand the P test cases, please look at manual: P test cases.
- (L4 - L16) → Declares three test cases each checking a different scenario and system. The system under test is the
unionof the modules representing each component in the system (manual: P module system). The
assertmodule constructor is used to attach monitors or specifications to be checked on the modules (manual: assert).
- In the
tcSingleClientAbstractServertest case, instead of composing with the Bank module, we use the AbstractBank module. Hence, in the composed system, whenever the creation of a BankServer machine is invoked the binding will instead create an AbstractBankServer machine.
Run the following command to compile the ClientServer project:
---------------------------------------- ==== Loading project file: ClientServer.pproj ....... includes p file: P/Tutorial/1_ClientServer/PSrc/Server.p ....... includes p file: P/Tutorial/1_ClientServer/PSrc/Client.p ....... includes p file: P/Tutorial/1_ClientServer/PSrc/AbstractBankServer.p ....... includes p file: P/Tutorial/1_ClientServer/PSrc/ClientServerModules.p ....... includes p file: P/Tutorial/1_ClientServer/PSpec/BankBalanceCorrect.p ....... includes p file: P/Tutorial/1_ClientServer/PTst/TestDriver.p ....... includes p file: P/Tutorial/1_ClientServer/PTst/Testscript.p ---------------------------------------- ---------------------------------------- Parsing .. Type checking ... Code generation .... Generated ClientServer.cs ---------------------------------------- Compiling ClientServer.csproj .. Microsoft (R) Build Engine version 16.10.2+857e5a733 for .NET Copyright (C) Microsoft Corporation. All rights reserved. Determining projects to restore... All projects are up-to-date for restore. ClientServer -> P/Tutorial/1_ClientServer/POutput/netcoreapp3.1/ClientServer.dll Build succeeded. 0 Warning(s) 0 Error(s)
You can get the list of test cases defined in the ClientServer program by passing the generated
to the P Checker:
pmc <Path>/ClientServer.dll Provide /method or -m flag to qualify the test method name you wish to use. Possible options are:: PImplementation.tcSingleClient.Execute PImplementation.tcMultipleClients.Execute PImplementation.tcSingleClientAbstractServer.Execute
There are three test cases defined in the ClientServer project and you can specify which
test case to run by using the
-m parameter along with the
-i parameter for the number of schedules to explore.
tcSingleClient test case for 1000 schedules:
pmc <Path>/ClientServer.dll \ -m PImplementation.tcSingleClient.Execute \ -i 1000
tcMultipleClients test case for 1000 schedules:
pmc <Path>/ClientServer.dll \ -m PImplementation.tcMultipleClients.Execute \ -i 1000
tcSingleClientAbstractServer test case for 1000 schedules:
pmc <Path>/ClientServer.dll \ -m PImplementation.tcSingleClientAbstractServer.Execute \ -i 1000
tcSingleClientAbstractServer triggers an error in the AbstractBankServer state machine. Please use the guide to explore how to debug an error trace generated by P Checker.
- [Problem 1] Fix the bug in AbstractBankServer state machine and run the P Checker again on the test case to ensure that there are no more bugs in the models.
- [Problem 2] Extend the ClientServer example with support for depositing money into the bank. This would require implementing events
eDepositRespwhich are used to interact between the client and server machine. The Client machine should be updated to deposit money into the account when the balance is low and the BankServer machine implementation would have to be updated to support depositing money into the bank account. After implementing the deposit feature, run the test-cases again to check if the system still satisfies the desired specifications.
What did we learn through this example?
We explored writing P state machines, safety and liveness specifications as P monitors, writing multiple model checking scenarios to check the correctness of a P program, and finally, replacing complex components in P with their abstractions using P's module system.