PICASSO: Termination of Depth-Bounded Processes
Downloading and using Picasso
The sources of Picasso can be obtained from the tool webpage.
For termination proofs Picasso uses the additional tools: ARMC, Princess, Z3
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).
Summary
| Example | # loc | # variables | # transitions | Cover | Abstraction | ARMC | Total |
|---|---|---|---|---|---|---|---|
| split/merge | 4 | 3 | 9 | 1.5 | 6.8 | 0.1 | 8.4 |
| 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 | 6 | 10 | 15 | 2.0 | 8.8 | 0.2 | 11.0 |
| 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 |
| Herlihy/Wing queue | 3 | 13 | 25 | 3.8 | 24.9 | 6.5 | 34.2 |
| 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.
Examples
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.
split/merge
input: split_merge.dbp
command: java -jar picasso-core-0.2.jar --termination split_merge.dbp
report: split_merge-report.html
Work stealing, 3 workers
input: stealing-3proc.dbp
command: java -jar picasso-core-0.2.jar --termination stealing-3proc.dbp --namedTPreds job
report: stealing-3proc-report.html
Work stealing, parametrized
input: stealing3.dbp
command: java -jar picasso-core-0.2.jar --termination stealing3.dbp
report: stealing3-report.html
Compute server job queue
input: clientserver.dbp
command: java -jar picasso-core-0.2.jar --termination clientserver.dbp
report: clientserver-report.html
Chatroom
input: chatroom.dbp
command: java -jar picasso-core-0.2.jar --termination chatroom.dbp --namedTPreds posts --namedTPreds userpost
report: chatroom-report.html (warning: large file, ~18MB)
Map reduce
input: mapReduce.dbp
command: java -jar picasso-core-0.2.jar --termination mapReduce.dbp
report: mapReduce-report.html
Map reduce with failures
input: mapReduceFailure.dbp
command: java -jar picasso-core-0.2.jar --termination mapReduceFailure.dbp --namedTPreds mapper,crash --namedTPreds reducer,crash
report: mapReduceFailure-report.html
Treiber’s stack (coarse-grained)
input: simple_non_blocking.dbp
command: java -jar picasso-core-0.2.jar --termination simple_non_blocking.dbp --namedTPreds Op
report: simple_non_blocking-report.html
Treiber’s stack (fined-grained)
input: treiber-full2.dbp
command: java -jar picasso-core-0.2.jar --termination treiber-full2.dbp --namedTPreds push
report: treiber-full2-report.html
Herlihy/Wing queue
input: HWqueue.dbp
command: java -jar picasso-core-0.2.jar --termination HWqueue.dbp
report: HWqueue-report.html
Michael/Scott queue (dequeue only)
input: msq6-deq-only.dbp
command: java -jar picasso-core-0.2.jar --termination msq6-deq-only.dbp
report: msq6-deq-only-report.html
Michael/Scott queue (enqueue only)
input: msq6-enq-only.dbp
command: java -jar picasso-core-0.2.jar --termination msq6-enq-only.dbp --namedTPreds "enq1,enq3,enq0"
report: msq6-enq-only-report.html
Michael/Scott queue
input: msq6.dbp
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