Artifact for Submission 172:

Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers

Tutorial

Prerequisites

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

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