PDSolver

Latest Version | Downloads | Requirements | Quick Start | User Guide | References

This is the PDSolver webpage as submitted to Spin 2010. As of 28th October 2010, later versions of PDSolver are available.

PDSovler is a tool for evaluating both mu‐calculus formulas over pushdown systems and pushdown parity games. It is an explicit state OCaml implementation of algorithms presented at Concur [Concur09] and submitted to Information and Control [I&C10]. We also extend these algorithms to support backwards modalities [Backwards10] and allow the analysis to be restricted to reachable configurations.

This tool has been submitted to SPIN 2010 [Spin10]. Below we provide examples of control flow graphs extracted, using the Soot Framework, from the DaCapo Benchmark Suite (Version 9.12). We distribute the tool with some Soot libraries. Up‐to‐date versions can be obtained from the Soot homepage. We do not distribute a copy of the DaCapo benchmarks.

This tool is maintained by Matthew Hague. Any queries/bugs/comments/&c. can be directed to Matthew Hague * comlab ox ac uk (with * = @ and spaces are .).

Downloads

pdsolver.tgz
The OCaml sources for PDSolver.
pdsolver‐examples.tgz
An extended set of examples used as benchmarks in [Spin10].
jimpletopdsolver.tgz
A Java program for extracting pushdown control flow graphs with use/define information, used to create many of the examples above.
jimpletopdsolver‐examples.tgz
An extended set of examples used as benchmarks in [Spin10]. See below for notes on usage.

Requirements

PDSolver requires

JimpleToPDSolver requires

Quick Start

We provide a short guide to getting started in Linux.

PDSolver

Download pdsolver.tgz and run the following commands from the directory containing pdsolver.tgz. 

            tar xzf pdsolver.tgz
            cd PDSolver
            omake
If successful, we can evaluate an example. 
            ./src/main/pdsolver.opt examples/journal.pdmu

PDSolver Extended Examples

To run the examples from the SPIN submission, first download pdsolver‐examples.tgz to the same directory as pdsolver.tgz. Then run the commands below (for example). 

            tar xzf pdsolver-examples.tgz
            cd PDSolver
            ./src/main/pdsolver.opt -o avroraReg.out -r csinit examples/avroraReg.pdmu
Here, -o avroraReg.out specifies an output file, and -r csinit restricts the analysis to configurations reachable from the initial configuration <csinit, #>, where the hash marks the bottom of the stack.

JimpleToPDSolver

Download jimpletopdsolver.tgz and, from the directory that contains it, run the following commands. 

            tar xzf jimpletopdsolver.tgz
            cd JimpleToPDSolver
            ant compile
If successful, you can then create an example pushdown system with use/define information. 
            ./JimpleToPDSolver -f dataflow.out "<examples.Dataflow: void main(java.lang.String[])>"
This generates a pushdown system with use/define information, but does not add a mu‐calculus formula. Open dataflow.out and add 
            Mu Property:

            !(
                (nu X . (!csend &
                [@def__examples_Dataflow__int_i_]ff
                &
                [\use__examples_Dataflow__int_i_ usedef__examples_Dataflow__int_i_]X))
                &
                ~[\def__examples_Dataflow__int_i_ usedef__examples_Dataflow__int_i_](nu
                Y.(mu Z. csend |
                <@def__examples_Dataflow__int_i_>tt | 
                <\use__examples_Dataflow__int_i_ usedef__examples_Dataflow__int_i_>Z) & 
                ~[\def__examples_Dataflow__int_i_ _usedef__examples_Dataflow__int_i_]Y)
            )
to the end of the file, saving the file as dataflow.pdmu. This is the dataflow example from the Spin submission. We can generate the denotation of the property by running the file through pdsolver, as in the extended examples section above.

JimpleToPDSolver Extended Examples

Setting up the extended examples is a little more involved. First download a copy of dacapo‐9.12‐bach.jar from the DaCapo Benchmark Suite (Version 9.12). Save this file in the same directory as jimpletopdsolver.tgz, then extract the required library files to the JimpleToPDSolver library. 
            unzip dacapo-9.12-bach.jar 'jar/*' -d JimpleToPDSolver/lib/
Next download jimpletopdsolver‐examples.tgz, and save it in the same directory as jimpletopdsolver.tgz. Then extract the examples. 
            tar xzf jimpletopdsolver-examples.tgz
Then recompile the sources and run an example. 
            cd JimpleToPDSolver
            ant compile
            ./JimpleToPDSolver -f avroraReg.out "<examples.AvroraReg: void main(java.lang.String[])>"
Finally, add a mu property to avroraReg.out as in the previous example.

User Guide

PDSolver | JimpleToPDSolver

In the following, we assume familiarity with pushdown systems, parity games and mu‐calculus.

PDSolver

To obtain usage information on PDSolver, run 

            ./src/main/pdsolver.opt --help
There are a wealth of command line options, most of which we recommend you ignore. The most important options are --output-file, --output-format, --check-type and --reachable.

The standard invocation command is 

            ./src/main/pdsolver.opt -o <outfile> <infile>
where outfile specifies where to write the output, and infile where to find the input problem. The type of problem is determined by the file extension: pdg for a pushdown parity game, and pdmu for a pushdown system and mu‐calculus problem. Common to both is a description of a pushdown system. This takes the following form. 
            Rules:

            p a -> q _;
            p a -> q b;
            p a -> q b c;
            . . .
for pop, rewrite and push operations respectively, where p and q are control states, and a, b and c are stack characters. Note, a word of any length may be specified. E.g. p a -> q b c d e f;. The stack character # is a special character denoting the bottom of the stack. This symbol cannot be added to, or removed from the stack.

Pushdown Parity Games

An example pdg file (examples/Arnaud.pdg) is shown below. 

            Rules:

            p # -> f #;
            p a -> p _;
            f a -> p a;
            f a -> f a a;
            f # -> f #;

            Control States:

            p Abelard 1;
            f Abelard 2;
The pushdown system is described as above. The Control State section specifies, for each control state, whether the state is owned by Eloise or Abelard, and the colour of the state.

Running the command 

            ./src/main/pdsolver.opt examples/Arnaud.pdg
yields the output below, which describes Eloise's winning region. 
            Done.                                             
            4 States: { q* qe (f,1) (p,1) }

            Transitions:

            q* -#-> { { qe } }
            q* -a-> { { q* } }
            (f,1) -#-> { { qe } }
            (f,1) -a-> { { q* (p,1) } }
            (p,1) -#-> { { qe } }
            (p,1) -a-> { { (p,1) } }


            Total time: 0.003  Check time: 0.003
            Gather stats time: 0.  Final opt time: 0.
            Ma states: 4  Ma trans: 6
            Max states: 0  Max trans: 0
            Controls: 2  Characters: 2  Transitions: 5
            Colours: 2
That is, an automaton with four states. The most important states are (f,1) and (p,1) since, for example, a configuration <p, w> is in Eloise's winning region if w is accepted from (p,1). As an example, take a transition q -a-> { { q1 q2 } { q3 } }. This means the automaton has two a transitions from the state q. The first is an alternating transition to both q1 and q2. The second is a standard non‐deterministic transition to q3. The remainder of the output shows statistics on the input, runtime, and result. Note that the zero entries are zero because we did not specify --gather-stats on the command line.

Mu Calculus Problems

An example pdmu input file (examples/journal.pdmu) follows. 

            Rules:

            p a -> p _;
            p # -> f #;
            f # -> f #;
            f a -> f a a;
            f a -> p a;

            Mu Property:

            (mu Z1 . (nu Z2 . ((p & []Z1) | (f & []Z2))))


            Propositions:

            p a p;
            p # p;
            f a f;
            f # f;
The pushdown system is as described above. Atomic propositions are specified in the Propositions section, taking the following form. 
            p a x y z . . .;
This line specifies that whenever the pushdown system has control state p and top of stack character a, the atomic propositions x, y and z are true. All other propositions are false.

The syntax of the mu‐calculus is described below. Note that to ensure the correct scoping of fixed points, we recommend putting all expressions mu Z . f and nu Z . f in parenthesis. That is (mu Z . f) and (nu Z . f).

x Atomic propositions begin with a lowercase character.
Z Variables begin with an uppercase character.
f1 & f2 The conjunction of formulas f1 and f2.
f1 | f2 The disjunction of formulas f1 and f2.
!f1 The negation of f1.
<>f1 The forward diamond modality for f1.
<@x1 x2 . . .>f1 The forward diamond modality for f1, parameterised by the propositions x1, x2, &c..
<\x1 x2 . . .>f1 The forward diamond modality for f1, parameterised by all propositions other than x1, x2, &c..
[]f1 The forward box modality for f1.
[@x1 x2 . . .]f1 The forward box modality for f1, parameterised by the propositions x1, x2, &c..
[\x1 x2 . . .]f1 The forward box modality for f1, parameterised by all propositions other than x1, x2, &c..
~<>f1 The backward diamond modality for f1.
~<@x1 x2 . . .>f1 The backward diamond modality for f1, parameterised by the propositions x1, x2, &c..
~<\x1 x2 . . .>f1 The backward diamond modality for f1, parameterised by all propositions other than x1, x2, &c..
~[]f1 The backward box modality for f1.
~[@x1 x2 . . .]f1 The backward box modality for f1, parameterised by the propositions x1, x2, &c..
~[\x1 x2 . . .]f1 The backward box modality for f1, parameterised by all propositions other than x1, x2, &c..
(mu Z . f1) The least fixed point of Z in f1.
(nu Z . f1) The greatest fixed point of Z in f1.

JimpleToPDSolver

The JimpleToPDSolver tool provides very limited functionality. To extract a pushdown system from a Java program, first make sure that the program classes are available in the classpath. 

            export CLASSPATH="<path to program classes>:$CLASSPATH"
Then run the tool. For example 
            ./JimpleToPDSolver -f dataflow.out "<examples.Dataflow: void main(java.lang.String[])>"
The specified method is the initial method of the program. This must be a static method. The file dataflow.out now contains a list of pushdown rules, and a list of proposition assignments as described above. 
            Rules:

            csinit # -> csq  cpLinit0016 #;
            csq cpLinit0016 -> csq  cpL_examples_Dataflow__main_ALjava_lang_String_V__11_0;
            . . .

            Propositions:

            csq # csq #;
            csq cpL_examples_Dataflow__b_V__23_12 csq cpL_examples_Dataflow__b_V__23_12 use__examples_Dataflow__int_i_ def__i1__in___examples_Dataflow__b_V_;
            . . .
The initial configuration of the program is <csinit, #>. The main control state is csq and csend is reached when the program terminates. The alphabet contains labels of the form 
            cpL_<class>__<method name>__<argument types>__<line no>_<unique id>
The following propositions are assigned to each control state and stack character pair:
  • the name of the control state,
  • the name of the stack character,
  • use__<var name>__in___<method info> for any variables used (but not modified) by the program line. Note that the method information is only present in local variables, and specifies which method the variable is local to,
  • def__<var name>__in___<method info> for any variables defined (but not used) by the program line, and
  • usedef__<var name>__in___<method info> for any variables both used and defined by the program line.
The generated file can be turned into a pdmu file with the addition of a Mu Property section.

Translation Strategy

JimpleToPDSolver translates the Jimple representation of the program to a pushdown system. Each statement roughly corresponds to one Jimple command. All data values are ignored, so statements such as assignments simply move to the next control point, while conditional statements branch non‐deterministically to any of the possible successor points. Virtual method calls are resolved by adding a branch calling each of the implementing methods present in the program (that is, in any class mentioned in the code).

When an exception is thrown, if its type can be determined statically, execution branches to the appropriate catch block, if one occurs. Otherwise the current method returns. If the type cannot be determined, we branch to any of the available catch blocks, or return. At each return point there is a branch that assumes an exception could have been returned. Hence, as well as continuing execution, we may also branch to any available catch blocks, or return from the method.

References

[Concur09]
M. Hague and C.‐H. L. Ong. Winning regions of pushdown parity games: A saturation method. In CONCUR 2009, pages 384‐398. [pdf]
[I&C10]
M. Hague and C.‐H. L. Ong. A Saturation Method for the Modal Mu‐Calculus over Pushdown Systems. Submitted, 2010. [pdf]
[Backwards10]
M. Hague and C.‐H. L. Ong. A saturation method for the modal mu‐calculus with backwards modalities over pushdown systems, 2010. [pdf]
[Spin10]
M. Hague and C.‐H. L. Ong. Analysing Mu‐Calculus Properties of Pushdown Systems (Tool Presentation). Submitted to SPIN, 2010.