## Artifact for Submission 172:

### Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers

- Checklist
- Tool
- Documentation
- Tutorial
- Experiments

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