POPL’17 artifact

A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms

aec-badge-popl

This is an artifact that accompanies the paper by Igor Konnov, Marijana LazicHelmut Veith,
and Josef Widder, which appears at POPL’17. If you have any questions about the artifact or the experiments, feel free to ask Igor Konnov.

1. Virtual machine

You can download the virtual machine (VirtualBox, 64-bit, 1.6 GB) from here.

The virtual machine contains Debian GNU/Linux 3.16 with all necessary packages installed. The packages are installed under the user account named ‘user’ with the password ‘user’. If you have to use the root account, the password is ‘root’. Alternatively, you can also use the ‘sudo’ command.

2. Package structure

The artifact files are located under the directory ‘/home/user/popl17-artifact16’, whose structure is as follows:

  • benchmarks/promela/ contains the benchmarks used in the paper, encoded in parametric Promela.
  • bymc/bymc/ contains the tool (binaries and source code).
  • klvw-popl17-camera.pdf is the camera-ready version of our paper.
  • appendix116.pdf is the appendix that contains Table 2 with details on the experimental results.
  • table2-new.pdf contains Table 2 with improved results, which were obtained after upgrading z3 to the version 4.3.2.

The original files that were submitted for the artifact evaluation are located under the directory
/home/user/popl17-artifact16-submission-oct16.

This package contains the following directories:

  • benchmarks/promela/ contains the benchmarks used in the paper, encoded in parametric Promela.
  • bymc/bymc/ contains the tool (binaries and source code).
  • logs contains log files from the runs at our server
    • table2/ contains log files for Table 2.
  • popl17-paper116.pdf is the accepted submission.
  • appendix116.pdf is the appendix that contains Table 2 with detailed experimental results.
  • table2-new.pdf contains Table 2 with improved results, which were obtained after upgrading z3 to the version 4.3.2.

3. Platform requirements

Our experiments were conducted on a server with 32 CPU cores (AMD Opteron R 6272) and 192 GB RAM. As our tool does not make use of concurrency, we used multiple cores to run several experiments in parallel.

The technique presented in this paper needs up to 17 GB RAM to evaluate each of the benchmarks (the most memory hungry benchmark is CBC). For this reason, the virtual machine is set up for 64-bit architecture. The virtual machine is shipped with the base memory of 4 GB. If you like to perform all the experiments, please increase the memory limit to, e.g., 24 GB.

4. Installation instructions

This virtual machine already contains all the necessary tools and libraries:

  • ocaml 4.x and ocamlbuild
  • ocaml libraries: batteries, ocamlgraph, sexplib, ocaml_plugin
  • python 2.x
  • Z3 4.3.2

In case you want to install the tool from scratch, please check the file ~/popl17-artifact16/bymc/bymc/README.txt.

5. Benchmarks

The following table shows the mapping between the source files in the benchmarks/promela directory and the benchmarks and their properties that are mentioned in the paper (in the same order as in Table 2). The columns S1, S2, L1, and L2 show the actual names of the temporal properties in the Promela code. The column ‘Flags’ shows the additional flags that have to be added in the end of the command line, when running the script verifypa-post (see Section 6).

No. Benchmark File S1 S2 L1 L2 Flags
1. FRB bcast-folklore-crash.pml unforg corr relay
2. STRB bcast-byz.pml unforg corr relay
3. NBACC asyn-ray97-nbac-clean.pml validity nontriv termination1 termination2
4. NBACG asyn-guer01-nbac.pml agreement abort_validity termination
5. NBAC asyn-ray97-nbac.pml validity nontriv termination1 termination2
6. BOSCO bosco.pml lemma3_0 lemma4_0 fast0 -D CASE1=1
7. BOSCO bosco.pml lemma3_0 lemma4_0 fast0 -D CASE2=1
8. BOSCO bosco.pml lemma3_0 lemma4_0 fast0 -D CASE3=1
9. BOSCO bosco.pml one_step0 fast0 -D CASE3=1 -D WEAKLY_1S=1
10. BOSCO bosco.pml one_step0 fast0 -D CASE3=1 -D STRONGLY_1S=1
11. ABA asyn-byzagreement0.pml unforg corr agreement -D CASE1=1
12. ABA asyn-byzagreement0.pml unforg corr agreement -D CASE2=1
13. C1CS c1cs.pml one_step0 fast0 -D CASE1=1
14. C1CS c1cs.pml one_step0 fast0 -D CASE2=1
15. C1CS c1cs.pml one_step0 fast0 -D CASE3=1
16. CF1S consensus-folklore-onestep.pml one_step0 fast0 -D CASE1=1
17. CF1S consensus-folklore-onestep.pml one_step0 fast0 -D CASE2=1
18. CF1S consensus-folklore-onestep.pml one_step0 fast0 -D CASE3=1
19. CBC cond-consensus2.pml validity0 agreement termination -D CASE1=1
20. CBC cond-consensus2.pml validity0 agreement termination -D CASE2=1
21. CBC cond-consensus2.pml validity0 agreement termination -D CASE3=1
22. CBC cond-consensus2.pml validity0 agreement termination -D CASE4=1

Note: In the experiments #9 and #10, we show the figures for the property one_step0 instead of lemma3_0 and lemma4_0, which are shown in the experiments #6-#8. The reason is that convergence in one communication step is the most important property of the algorithm, which holds only in the cases when either n > 5*t && f == 0 (benchmark #9), or n > 7 * t (benchmark #10).

6. Running the individual experiments

In this section, we give the commands to check the property unforg of the algorithm bcast-byz.pml. To find the properties of other benchmarks, check the table in Section 5, or search the Promela code for lines that look like ltl property_name {...}.

The following command runs the parameterized model checking technique presented in the paper:

$ ~/popl17-artifact16/bymc/bymc/verifypa-post ~/popl17-artifact16/benchmarks/promela/bcast-byz.pml unforg

you should see the following line in the output:

The property is verified in 0 refinement steps

(Since this technique uses integer counters, the number of refinement steps is always zero.)

When you pass -D BUG1=1, which adds more faults than the algorithm can tolerate, that is:

$ ~/popl17-artifact16/bymc/bymc/verifypa-post ~/popl17-artifact16/benchmarks/promela/bcast-byz.pml unforg -D BUG1=1

you should see the following line in the last six lines of the output:

> SLPS: counterexample for unforg found

The file ‘verdict.txt’ (alternatively, you can open ‘verdict.csv’ in a spreadsheet editor) contains detailed statistics, e.g., the interesting fields are as follows:

  • '06:total-sec' contains the total running time (plotted in Figure 9 of the paper),
  • '43:post-maxreskb' contains the consumed resident memory (in kilobytes, plotted in Figure 9 of the paper),
  • '52:post-nschemas' contains the number of explored lassos (plotted in Figure 9 of the paper),
  • '48:post-nlocs' and '49:post-nrules' contain the number of threshold automaton locations and rules respectively,

NOTE: some benchmarks (ABA, CBC, CF1S, C1CS, BOSCO) require several cases to consider (CASE1, CASE2, etc.). Precise flags are given in the table in Section 5. For instance,

$ ~/popl17-artifact16/bymc/bymc/verifypa-post ~/popl17-artifact16/benchmarks/promela/bosco.pml lemma3_0 -D CASE3=1 -D WEAKLY_1S=1

7. Running all experiments

To run all the experiments given in Table 2, invoke the script crunch-all.sh:

$ ~/popl17-artifact16/benchmarks/promela/crunch-all.sh uranus-post

NOTE: we ran our experiments on a computer with 32 CPU cores and 192 GB RAM. Many benchmarks were run in parallel. The command given above is will run 12 processes in parallel. This can be fixed by changing NCORES to 1 in crunch-all.sh.

Alternatively, to run at most two processes in parallel, you can run the following command:

$ ~/popl17-artifact16/benchmarks/promela/crunch-all.sh uranus-post-2cpus

8. Log files

The log files are contained in the directory ~/popl17-artifact16-submission-oct16/logs/table2. The structure is as follows:

  • out/1/$i/stdout contains the tool output for an experiment $i.
  • x/<benchmark>-<spec>-exp<i>-<timestamp> contains the files generated by the tool when verifying an experiment number <i> for a bechmark <benchmark>, and a specification <spec>. The files of interest are:
    • post.out contains the tool output.
    • fuse.sk contains the (generated) description of a threshold automaton.

9. Source files

The source files (in OCaml) are located under the directory 'popl17-artifact16/bymc/bymc/src'. The technique presented in this paper is implemented in the module 'schemaCheckerLtl.ml'. Its top-level function is called find_error, which is called by the class 'SchemaCheckerPlugin'. The implementation of the reachability analysis, which was introduced in [Konnov,Veith,Widder’15], can be found in the module 'schemaChecker.ml'.

Latest News

FORSYTE’s 2018 paper awards

FORSYTE has had a quite successful year: Adrian Rebola Pardo and his co-authors received the IJCAR best paper award for their paper Extended Resolution Simulates DRAT, Mitra Tabaei Befrouei and her co-authors received an OOPSLA 2018 Distinguished Paper award for their paper Randomized Testing of Distributed Systems with Probabilistic Guarantees, and Thomas Pani received the […]

Continue reading

OOPSLA Distinguished Paper Award

Mitra Tabaei Befrouei and her co-authors from MPI-SWS Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic, received an OOPSLA’18 Distinguished Paper Award for their contribution “Randomized Testing of Distributed Systems with Probabilistic Guarantees” (Open Access article). Congratulations!

Continue reading

Zvonimir Rakamiric visiting FORSYTE

Prof. Zvonimir Rakamiric from the School of Computing at the University of Utah is spending his sabbatical with the FORSYTE group at TU Wien. He is generously sponsored by the Wolfgang Pauli Institute and a Pauli Fellow.

Continue reading

Helmut Veith Stipend Award Ceremony

The Vice Rector for Academic Affairs of TU Wien, Kurt Matyas, will award the scholarship recipient of the Helmut Veith Stipend at the award ceremony on Friday, April 06, 2018 in the Kontaktraum, starting at 17:05.

Continue reading

Full news archive