Tutorial

Prerequisites

  • Our tool requires 64-bit Windows 10. Using Windows Command Prompt is most effective.

  • To better understand our tool PAT, please read the design description under Documentation tab first.

  • For this tutorial, please enter the examples/tutorial/ directory.

  • To have the executable of our tool readily available, please add the location your-unpacked-path /artifact/bin/x64/Binaries/ to the PATH environment variable.

1. Help Info

The following command prints usage help info: 
pt /h
Some options related to our tool (PAT = pt /os-list) are explained as follows 
---------------------------------------------
Options ::
---------------------------------------------
/h                       Print the help message

Flags related to exhaustive state space exploration:
/dfs                     Perform DFS exploration of the state space
/os-list                 Perform OS exploration (based on DFS) of the state space, with queue list abstraction
/queue-bound:k           Bound queue size to k (i.e. a machine's send is disabled when its current buffer is 
                         size k) (default: 0=unbounded for DFS, 1 for OS).
                         In case of /os-list search, this bound applies to the first-round queue and is 
                         incremented subsequently.
/queue-prefix:p          Keep prefix of queue of length p(>=0) /exact/ (abstraction applies to suffix starting 
                         at position p) (default: 0)
/interactive             Interactive mode: need users to press button to increase queue bound and continue 
                         exploration
/file-dump               Pretty-print accumulated states into files. For debugging only; this may create LARGE 
                         files!

Flags related to QuTL model checker:
/qutl:formula            Use QuTL formula to specify the properties which states should satisfy
/concrete                Invoke concrete model checker to test the correctness of QuTL formula!

If none of /psharp, /dfs, /os-... are specified: perform random testing
</p>

We illustrate tool usage through a motivating example, pingflood.p, included in the examples/tutorial/pingflood/ directory. It is the same example we show in Section 2 of the paper except that some functions/variables use different names.

2. Compile a P program

A P compiler pc.exe is included in the directory bin/x64/Binaries, and a batch script to compile pingflood.p is also included in examples/tutorial/pingflood/. So, simply run the following command to compile pingflood.p. 

build.bat
The compilation produces a file named pingflood.dll, which is used by PAT, as shown below.

Warning: The compilation might take several minutes.

3. Run PAT

Remark: verify P programs via iteratively increasing the unabstracted prefix of queues. For example, 
pt /os-list pingflood.dll /queue-prefix:0
pt /os-list pingflood.dll /queue-prefix:1
pt /os-list pingflood.dll /queue-prefix:2
pt /os-list pingflood.dll /queue-prefix:3
pt /os-list pingflood.dll /queue-prefix:4
Explanation:
  • pingflood.dll: a compiled P program which is the target of verification.
  • /os-list : use the list abstraction.
  • /queue-prefix: the size of the un-abstracted prefix of queues (default value is 0). During verification, this value will be iteratively increased, until you either experience convergence, or reach an (artificially specified) upper bound.
Example: The example does NOT converge when the value of /queue-prefix is 0~3. But it converges when the value of queue-prefix is 4. The output of queue-prefix:4 is shown at the bottom of this page. Whenever there is a plateau but meanwhile our tool cannot determine the convergence, our tool provides two options to users: 
(c)ontinue, by increasing the queue bound, ignoring the unreached successor, OR
(i)nvestigate; we will then locate the state with that hash code.
The second one (i)nvestigate typically tell users why convergence does not appear at this point. Subsequently, users might be able to get some hints to design queue invariants to exclude spurious abstract states, if any.

4. Run PAT+I

Other than iteratively increasing the un-abstracted prefix of an abstract queue, an alternative solution is to specify some invariant, via a QuTL formula, to exclude the spurious abstract states.

Remark: PAT+Invariant will enable QuTL model checker to exclude some spurious abstract states, which will prevent convergence. In the current implementation, the QuTL formula is written in Reverse Polish Notation (RPN) (i.e. postfix notation). This is a limitation of the usability. We will improve this and use the infix notation in the next version.

One thing we hope users keep in mind is that: Typically, there are many different helpful invariants. For instance, for the given example, one invariant is the same as we present in the paper. The other one is as follows: 

pt /os-list pingflood.dll /qutl:"true:$ DONE = DONE # 0 = => () PING PING G => () G &"
We have included both invariants in the batch script run.bat under directory tutorial/pingflood/.

Explanation:
  • /qutl:formula: The entire formula is a collection of machine-wise QuTL subformulae. The subformulae are separated by semicolon (;). For example, program pingflood.p has two machines. So, the formula in the example has two subformulae:
    • The QuTL subformula for machine server (the Main machine in the code) is: true

    • The QuTL subformula for machine client is: $ DONE = DONE # 0 = => () PING PING G => () G &, whose infix form is ($ = DONE => #DONE = 0) & G(PING => G PING).

      Remark: This subformula consists of two components, connected by logic and &. They actually present a same constraint from different perspectives. In other words, The first one is a supplementary of the second one. Symbol $ represents the current processing event. So, the first component says: if the current processing event is DONE, then there won't be event DONE any more . While the second component says: whenever an PING appears in the queue, then the incoming event is always PING . Since the second component cannot constrain the processing event, we need the first component to complete the constraint.

Example: The example converges with the invariant, even when queue-prefix:0. The output is shown at the bottom of this page.

5. Example Output

PAT (with /queue-prefix:p)

PAT+I (with /qutl:formula)