Skip to content

Client Server

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.

Placeholder

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).

P Project

The 1_ClientServer folder contains the source code for the ClientServer project. Please feel free to read details about the recommended P program structure and P project file.

Models

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 eWithDrawReq and eWithDrawResp are used to communicate between the Client and the Server machines (manual: event declaration).
  • (L3 - L17) → Declares the payload types for the eWithDrawReq and eWithDrawResp events (manual: user defined type).
  • (L25 - L95) → Declares the Client state machine (manual: P state machine).
    • The Client machine has a set of local variables used to store the local-state of the state machine (L27 - L31). Init state is the start state of the machine where the machine starts executions on being created. The entry function of the Init state initializes the local variables based on the parameters received on creation and jumps to the WithdrawMoney state.
    • In the WithdrawMoney state, 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 eWithDrawReq event (L55) otherwise it jumps to the NoMoneyToWithDraw state. After sending a withdraw request, the machine waits for the eWithDrawResp event (L59). On receiving the eWithDrawResp event, 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 BankServer machine. 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 Database machine. 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 checking the client application.
[Expand]: Let's walk through AbstractBankServer.p
  • (L12 - L37) → Declares an abstraction of the BankServer machine. The AbstractBankServer provides an implementation of the Bank where the interaction between the BankServer and Database is abstracted away. We use the AbstractBankServer machine 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.

Key Takeaway

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.

[Expand]: Let's walk through ClientServerModules.p
  • (L1 - L5) → Declares the Client and Bank modules. 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 Client module consists of a single machine Client and the Bank module is implemented by machines BankServer and Database together (manual: P module system).
  • (L7 - L8) → The AbstractBank module uses the binding feature in P modules to bind the BankServer machine to the AbstractBankServer machine. Basically, what this implies is that whenever AbstractBank module is used the creation of the BankServer machine will result in creation of AbstractBankServer, replacing the implementation with its abstraction (manual: primitive modules).

Specifications

The P Specifications (PSpec) for the ClientServer example are implemented in the BankBalanceCorrect.p file. We define two specifications:

  • 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_Init is 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 BankBalanceIsAlwaysCorrect safety spec machine that observes the events eWithDrawReq, eWithDrawResp, and eSpec_BankBalanceIsAlwaysCorrect_Init to assert the required global invariant.
  • (L92 - L115) → Declares the GuaranteedWithDrawProgress liveness spec machine that observes the events eWithDrawReq and eWithDrawResp to 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.

Test Scenarios

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.

The test scenarios folder for ClientServer (PTst) consists of two files TestDriver.p and TestScript.p.

[Expand]: Let's walk through TestDriver.p
  • (L36 - L60) → Function SetupClientServerSystem takes as input the number of clients to be created and configures the ClientServer system by creating the Client and BankServer machines. The CreateRandomInitialAccounts function uses the choose primitive to randomly initialize the accounts map. The function also announce the event eSpec_BankBalanceIsAlwaysCorrect_Init to initialize the monitors with initial balance for all accounts (manual: annouce statement).
  • (L3 - L22) → Machines TestWithSingleClient and TestWithMultipleClients are 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 checking it with either one Client or 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 union of the modules representing each component in the system (manual: P module system). The assert module constructor is used to attach monitors or specifications to be checked on the modules (manual: assert).
  • In the tcAbstractServer test 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.

Compiling ClientServer

Navigate to the 1_ClientServer folder and run the following command to compile the ClientServer project:

p compile
Expected Output 
$ p compile

.. Searching for a P project file *.pproj locally in the current folder
.. Found P project file: P/Tutorial/1_ClientServer/ClientServer.pproj
----------------------------------------
==== Loading project file: P/Tutorial/1_ClientServer/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...
MSBuild version 17.3.1+2badb37d1 for .NET
Determining projects to restore...
Restored P/Tutorial/1_ClientServer/PGenerated/CSharp/ClientServer.csproj (in 102 ms).
ClientServer -> P/Tutorial/1_ClientServer/PGenerated/CSharp/net6.0/ClientServer.dll

Build succeeded.
0 Warning(s)
0 Error(s)

Time Elapsed 00:00:02.25


----------------------------------------
~~ [PTool]: Thanks for using P! ~~

Checking ClientServer

You can get the list of test cases defined in the ClientServer project by running the P Checker:

p check
Expected Output 
$ p check

.. Searching for a P compiled file locally in the current folder
.. Found a P compiled file: P/Tutorial/1_ClientServer/PGenerated/CSharp/net6.0/ClientServer.dll
.. Checking P/Tutorial/1_ClientServer/PGenerated/CSharp/net6.0/ClientServer.dll
Error: We found '3' test cases. Please provide a more precise name of the test case you wish to check using (--testcase | -tc).
Possible options are:
tcSingleClient
tcMultipleClients
tcAbstractServer

~~ [PTool]: Thanks for using P! ~~

There are three test cases defined in the ClientServer project, and you can specify which test case to run by using the -tc parameter along with the -s parameter for the number of schedules to explore.

Check the tcSingleClient test case for 1000 schedules:

p check -tc tcSingleClient -s 1000

Check the tcMultipleClients test case for 1000 schedules:

p check -tc tcMultipleClients -s 1000

Check the tcAbstractServer test case for 1000 schedules:

p check -tc tcAbstractServer -s 1000

Error

tcAbstractServer triggers an error in the AbstractBankServer state machine. Please use the guide to explore how to debug an error trace generated by the P Checker.

Exercise Problem

  • [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 eDepositReq and eDepositResp which 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.