Topics for Test-Comp Replicability Q: How do I make sure that my test generator was correctly executed? What should the teams do with the results that were sent to them? A: The first step is to make the following sanity checks: - Did the test generator start properly? - Is the log file accessible? - Is the test suite accessible? - Did the test generator find all components that are required? Q: Is the category opt-out used correctly and are the options that my test generator requires correctly set? A: It is the responsibility of the participants to make sure that the benchmark definition is correct. The benchmark definition that is used for TESTER is available in the repository: https://gitlab.com/sosy-lab/test-comp/bench-defs/-/blob/main/benchmark-defs/TESTER.xml Q: Is my test generator correctly installed on the competition machines and are the results correctly interpreted? A: It is the responsibility of the participants to make sure that the tool-info module for BenchExec works correctly. This module specifies which paths of the test generator archive should be installed on the competition machines and how to parse and translate the result from the log output. The tool-info module that is used for TESTER is available in the BenchExec repository: https://github.com/sosy-lab/benchexec/tree/main/benchexec/tools/TESTER.py Please make sure to test your tool-info module according to the instructions here: https://github.com/sosy-lab/benchexec/blob/main/doc/tool-integration.md#testing-the-tool-integration Q: Where do I find the test tasks that are used in Test-Comp? A: The test tasks for Test-Comp are available in the open repository of verification tasks at: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/tree/main/c The organizer and jury partition the test tasks into categories. Those categories are described here: http://test-comp.sosy-lab.org/2019/benchmarks.php The current plan for the category assignment is available there. Q: What directories does my test generator see on the competition machines? A: Conceptual description is available here: https://www.sosy-lab.org/research/pub/2017-STTT.Reliable_Benchmarking_Requirements_and_Solutions.pdf Technical details are available on the help page ('runexec -h'). Here is an example call to BenchExec's runexecutor and a description of it below: python -m benchexec.runexecutor --container --read-only-dir / --hidden-dir /home --hidden-dir /sys/kernel/debug --hidden-dir /var/lib/cloudy --overlay-dir /etc --overlay-dir /tmp/vcloud-vcloud-master/worker/working_dir_73f51db6-c032-4848-9c92-a94446513a4f --dir /tmp/vcloud-vcloud-master/worker/working_dir_73f51db6-c032-4848-9c92-a94446513a4f/bin-2018/utaipan --output /tmp/vcloud-vcloud-master/worker/working_dir_73f51db6-c032-4848-9c92-a94446513a4f/cloudBenchmarkOutput.txt --output-directory /tmp/vcloud-vcloud-master/worker/working_dir_73f51db6-c032-4848-9c92-a94446513a4f/bin-2018/utaipan --debug --maxOutputSize 2000000 --timelimit 60 --memlimit 7000000000 --memoryNodes 0 --cores 3,7 -- ./Ultimate.py --spec ../../sv-benchmarks/c/Termination.prp --file ../../sv-benchmarks/c/product-lines/minepump_spec1_product06_true-unreach-call_false-termination.cil.c --full-output --architecture 32bit Description: - starts BenchExec's module 'runexecutor' - in container mode [https://github.com/sosy-lab/benchexec/blob/main/doc/container.md] - making all files available in the container as 'read only', with the exceptions below - hides directory '/home' and makes a fresh copy available inside the container - same for '/sys/kernel/debug' - same for '/var/lib/cloudy' - makes the contents of '/etc' available inside the container and redirect all writes to a fresh directory - same for /tmp/vcloud-vcloud-master/worker/working_dir_73f51db6-c032-4848-9c92-a94446513a4f - working directory is set to the value given to '--dir' - all output of the verifier (stdout and stderr) is written to the file specified with '--output' - all files that are written to directory '.' (default of option '--result-files') are copied to directory specified with '--output-directory' on the host (i.e., available to the user) - debug info is produced - the maximal output size is limited to 2 MB as per SV-COMP rules - time limit is set (60 s was for the pre-runs) - mem limit is set (7 GB was for the pre-runs) - memory node 0 is used - cores with ids 3 and 7 are used (pre-runs were restricted to two cores) - the rest is specific to the test generator Results Q: Where can I find the output of my test generator? A: The status column in the HTML tables contains links to the log files. If the results do not match the expectations, this is where all necessary information to track down the problem can be found. Ensure that enough detail is printed into the log file that is useful to understand the run result. Q: Which version of my test generator was used for the last test-generation run? A: The exact version is contained in the header of each result table. The tool-info module is asked to produce a version string for the test generator. Also, a good test generator prints exact version information at the beginning, like "This is test generator BEST version 3.14 compiled 2016-11-27T1725." such that the version information is also available in the log files. Q: Were all components that my test generator needs correctly found? Which version of component X was used? A: Check the log output that the test generator produced. Any interesting exception should result in a line of output. Also, a test generator can print the exact version of a component (gcc, llvm, ...) in order to later find out what exact components were used. Q: What data is made available from the test-generation runs? A: After each test-generation run, the participating team receives an e-mail with links to the results of their test generator. The XML files are the raw data that BenchExec produced. The HTML tables contain less information for a convenient overview --- if more details are needed, please fall back to the XML files. The XML files are easy to convert to costumized HTML pages using BenchExec's tablegenerator (https://github.com/sosy-lab/benchexec/blob/main/doc/table-generator.md). The XML and HTML files with 'merged' in the name are for those categories for which test-suite validation was done. There are additional columns about the test-suite-validation process. Test-Suite Validation Q: How can I validate my test-suite myself? A: You can download and install the available validators on your own machine. Q: Was the test suite that my test generator produced, found and made available for validation? It seems the test suite that my test generator produced was not found. A: Column 'test-suite' contains a link to your test suite. Click on it to find out if your test suite is available. Check that your test suite file ends with .zip and that the required metadata fields are present. Important note: It is assumed that there is only one .zip file produced, which is searched and used. Q: Can I contribute to the test-suite validator? A: Absolutely. The validator is open source and you can improve and file merge requests.