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

People

IST Austria