Artifact for Submission 172:
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers
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
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.batThe 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:4Explanation:
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.
/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, programpingflood.p
has two machines. So, the formula in the example has two subformulae:
- The QuTL subformula for machine
server
(theMain
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 isDONE
, then there won't be eventDONE
any more . While the second component says: whenever anPING
appears in the queue, then the incoming event is alwaysPING
. Since the second component cannot constrain the processing event, we need the first component to complete the constraint.
- The QuTL subformula for machine
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
)