PICASSO: Termination of Depth-Bounded Processes
Downloading and using Picasso
The sources of Picasso can be obtained from the tool webpage.
To run Picasso and prove termination the option to use is --termination.
Assuming that this file is named input.dbp, it is possible to run the example with the command:
# java -jar picasso-core-0.2.jar --termination input.dbp
Additionally it is possible to use the -r option to get an html report that contains the important information about the execution. With -r Picasso produces a file called input-report.html.
Other useful options are:
- -h: for help.
- -v: to increase the verbosity.
- --stats: to record and print some statistics.
- --noAssert: to skip some runtime checks, resulting in faster execution.
- --armc: give the command for armc (when it is not in the path).
- --smtSolver: give the command to use for smtlib2 queries (when z3 is not in the path).
- --princess: give the command for pricess (when it is not in the path).
|Example||# loc||# variables||# transitions||Cover||Abstraction||ARMC||Total|
|Work stealing, 3 workers||4||4||20||1.7||13.1||0.2||15|
|Work stealing, parametrized||2||3||4||1.5||5.6||0.1||6.2|
|Compute server job queue||2||5||4||1.6||6.1||0.1||7.8|
|Chatroom||5||34||80||9.8||61.3||5 min.||6 min.|
|Map reduce with failures||6||15||21||2.3||11.1||0.9||14.3|
|Treiber’s stack (coarse-grained)||2||6||4||1.9||7.2||0.2||9.3|
|Treiber’s stack (fine-grained)||3||14||13||2.7||14.2||1.2||17.1|
|Michael/Scott queue (dequeue only)||4||7||23||2.8||13||0.6||16.4|
|Michael/Scott queue (enqueue only)||7||15||53||3.8||43.7||7.6||55.1|
|Michael/Scott queue||9||31||223||25||265||3 wks||3 wks|
Summary of the experimental results. First, we give some statistics about the size of the numerical abstraction: number of locations, variables, and transitions. Then, the time required to compute the covering set, extract the numerical abstraction, and the time requires to prove termination. The time are given in second unless another unit is specified.
Here are the inputs give to Picasso and the resulting output. We also give the command that was used. You may notice that some commands also contains hints for the transitions predicates given to ARMC. Picasso generates transition predicates by summing the variables which names start by the given prefixes.
Work stealing, 3 workers
Work stealing, parametrized
Compute server job queue
Map reduce with failures
Treiber’s stack (coarse-grained)
Treiber’s stack (fined-grained)
Michael/Scott queue (dequeue only)
Michael/Scott queue (enqueue only)
command: java -jar picasso-core-0.2.jar --termination msq6.dbp --namedTPreds "enq1,enq3,enq0" --namedTPreds "enq0,enq1,enq3,deq" --namedTPreds deq
partial report: msq6-partial-report.html