- Author: Wenhao Wu, (wuwenhao@udel.edu) Jan Hueckelheim, (jhueckelheim@anl.gov) Paul Hovland, (hovland@anl.gov) Stephen Siegel, (siegel@udel.edu) - Abstract This is the README file for replicating experiments mentioned in the paper 'Verifying Fortran Programs with CIVL', which is submitted to TACAS2022. - Experiment Replication 1. Download Execution Environment 1). Install VirtualBox from: https://www.virtualbox.org/wiki/Downloads (This tool archive is created and tested on VirtualBox ver. 6.1.28 r147628) 2). VirtualBox OS Image can be downloaded from: https://zenodo.org/record/5562597#.YXgSZi-B1pR (This tool archive is created and tested on OS imported from 'TACAS AE.ova', which is based on Ubuntu 20.04. ) 3). This tool archive can be downloaded from: https://vsl.cis.udel.edu/tacas2022 2. Tool Archive Deployment 1). unzip the tool archive file to '/home/tacas22/Documents/': > unzip civl_tacas22.zip -d /home/tacas22/Documents/ * It is required to extract the zip archive to '/home/tacas22/Documents/', so that CIVL executable jar file can be found in '/home/tacas22/Documents/civl_tacas22/bin' 2). directories and files included in the archive are: a). directory './civl_tacas22/bin/' includes i). civl.jar: the binary executable jar file of CIVL ii). civl: a bash script invokes civl.jar from '/home/tacas22/Documents/civl_tacas22/bin' b). directory './civl_tacas22/deps/' includes i). *.deps: dependencies required by CIVL, which are: openjdk11, cvc4, and z3 ii). *.deb: offline packages used for installing all required dependencies c). directory './civl_tacas22/examples' includes i). './examples/civl/': 17 verification examples (19 files) in CIVL verification suite ii). './examples/smack/': 22 verification examples (22 files) in SMACK verification suite iii). './examples/nek5000/': 3 verification examples (12 files) from Nek5000 application. d). directory './out/': holds generated files containing verification results. A single *.out file is generated for each example. e). directory './out_paper/': holds verification results mentioned in paper, which are executed in the environment mention in paper (Sec. 5.1) f). file './License.txt': includes License information of CIVL, SAMCK, and Nek5000 g). file './makefile': is used for replicating all verification experiments in the paper (The instruction of using 'make' can be found in Sec. 5.) h). file './README': is the instruction of using the tool package. 3. Dependency Installation: 1). change directory to './civl_tacas22/deps/' after the archive is unzipped. > cd /home/tacas22/Documents/civl_tacas22/deps/ 2). install all required dependencies including: openjdk11, cvc4, and z3 > sudo dpkg -i *.deb 3). back to the root directory './civl_tacas22/' > cd .. 4). check versions of dependencies installed: > java --version | openjdk 11.0.11 2021-04-20 > cvc4 --version | This is CVC4 version 1.6 > z3 --version | Z3 version 4.8.7 - 64 bit 4. Configure CIVL (including Fortran extension) 1). set the bash script ./bin/civl to be executable > chmod ugo+x ./bin/civl 2). add the script 'civl' to directory '/usr/local/bin/' > sudo cp ./bin/civl /usr/local/bin/civl 3). configure CIVL > civl config | .. | Adding Z3 version 4.8.7 - 64 bit at /usr/bin/z3 | Adding CVC4 version 1.6 at /usr/bin/cvc4 | .. | SARL configuration file created successfully in /home/tacas22/.sarl | .. * If 'civl' can not be 'sudo cp' to '/usr/local/bin/' then 'civl' command used in makefile variable 'CMD_CIVL' (line 8) can be replaced by 'java -jar /home/tacas22/Documents/civl_tacas22/bin/civl.jar' e.g., CMD_CIVL=java -jar /home/tacas22/Documents/civl_tacas22/bin/civl.jar 4). set the awk script 'collect_outputs.awk' to be executable > chmod +x collect_outputs.awk 5. Replicate Experiments with Make command: 1). get verification results for all examples mentioned in the paper terminal outputs for each example are saved to directory: ./out * two .table files will be created: out.table collects execution result data from VM execution output in ./out/*.out out_paper.table collects ones from the execution samples, which come from the machine mentioned in the paper. > make all | civl verify ./examples/civl/abs.f90 >> ./out/abs.out | .. 2). get verification results for specific example set (i.e., civl, smack or nek) > make civl | civl verify ./examples/civl/abs.f90 >> ./out/abs.out | .. > make smack | civl verify ./examples/smack/array.f90 >> ./out/array.out | .. > make nek | civl compare -inputBOUND=2 -spec ./examples/nek5000/mxm/mxm_driver.f ./examples/nek5000/mxm/mxm_naive.f -impl ./examples/nek5000/mxm/mxm_driver.f ./examples/nek5000/mxm/mxm_pencil.f >> ./out/pencil2x2.out | .. 3). rules of verifying any single example can be found in './makefile' > cat ./makefile | ## This is makefile used for replicating experiments mentioned in paper | .. | omp_do.out: $(DIR_CIVL)/omp_do.f90 | $(VRF) $(OMP) $(DIR_CIVL)/omp_do.f90 >> $(DIR_OUT)/omp_do.out | .. 4). instructions of customizing verification examples can be found in corresponding source files 5). rules of generating result table > make run > make out.table | touch ./out/summary.out | cat ./out/array.out >> ./out/summary.out | .. | ./collect_outputs.awk < ./out/summary.out > out.table | rm ./out/summary.out 6). temporary files generated by executing CIVL verification can be removed by > make clean 6. Explanation of Verification Result in *.out File 1). An example of verification output (abs.out): > $ civl verify ./examples/civl/abs.f90 | CIVL v1.20+ of 2019-09-27 -- http://vsl.cis.udel.edu/civl | === Source files === | abs.f90 (./examples/civl/abs.f90) | | === Command === | civl verify ./examples/civl/abs.f90 | | === Stats === | time (s) : 0.68 | memory (bytes) : 2155872256 | max process count : 1 | states : 6 | states saved : 3 | state matches : 0 | transitions : 5 | trace steps : 1 | valid calls : 1 | provers : cvc4, z3, why3 | prover calls : 1 | |=== Result === |The standard properties hold for all executions. 2). The last line shows the final result of the verification execution. a). "The standard properties hold for all executions." means that there is no violation detected based on given/default correctness properties * In the paper, this output is equivalent to result (Res.) 'True' or 'Eqv' in Table 1 and 2 (Section 5.3 and 5.4). b). "The program MAY NOT be correct. See CIVLREP/abs_bad_log.txt" means that these is a violation found and the program may have bugs or violated assertions. * In the paper, this output is equivalent to result (Res.) 'False' or 'NEq' in Table 1 and 2 (Section 5.3 and 5.4). 3). statistic data can be found in section 'Stats' a). time(s): shows the number of seconds this verification procedure costs b). memory (bytes): shows the memory size (bytes) used by this verification execution. c). states: shows the number of states generated for the given source program. * In the paper, Time column of Table 1. and 2. are filled with the average run time of 7 verification executions. * LoC of Table 1. and 2. will NOT count blank and comment lines. 7. Customize Verification Examples 1). CIVL verification suite: a). abs: - The range of 'arg' can be changed to any valid integers by modifying CIVL assumption on Line 6. Then, the assertion on Line 8 shall be changed to corresponding range. - Invalid assumption (e.g., 0 < arg && arg < 0) will result in false path condition, then NO violation shall be reported. Because anything implied by a false condition is evaluated as true. b). array_section: - Both the rank and index ranges of each rank can be changed. Initial array element values and updated values in subroutine 'subr' can be changed also. - Additional assertions can be added to ensure the value of each array element. c). intent_intout: - change 'inout' to 'out' on Line 15 shall result in violation. d). intent_out: - any variable with attribute intent(out) cannot be read without being assigned. e). omp_do: - Variables accessed in omp parallel do regin can be changed, and read-write or write-write conflicts on shared variables are reported as data race. - The current version has limited support on OpenMP Fortran bindings f). short_circuit: - The 'idx' can be changed to any valid integers. An index-out-of-bound violation will be reported if the value of 'idx' is out of the defined range without short-circuit evaluation (when the first sub-expression (Line 18) is evaluated to be true) - Users can create similar examples with multi-dimensional arrays with different index ranges. - Users can change the logic expression on Line 18 with any sub-expression that access an array element with any index value. If the value is out of the range, a violation shall be reported. g). truncate: - the character '1' on Line 7 column 73 is truncated implicitly based on Fortran 77 standard (because the file suffix is f and using a fixed form) Thus, sum is evaluated as: sum = 10 + extremelylongvariablename + extremelylongvariablename By shortening the variable name from 'extremelylongvariablename' to 'shortname' and 'extremelylongvariablename1' to 'shortname1', the expression on Line 7 shall not exceed a length of 73. Then, sum shall be evaluated as: sum = 10 + shortname + shortname1 If the assertion is unchanged and evaluates 'sum .EQ. 10', an assertion violation is reported because the actual sum value with no implicit truncation should be 11. h). mod: - By making mod_impl.f90 calculate incorrect mod-by-2 result, an assertion violation showing outputs between specification program 'mod_spec.f90' and implementation program 'mod_impl.f90' are NOT equivalent. - By fixing mod_impl_bad.f90 to correctly compute mod-by-2, no violation shall be reported by comparing two programs. * CIVL compare command is used as: > civl compare -spec mod_spec.f90 -impl mod_impl.f90 i). mult: - This example is similar with example 'mod'. 2). SMACK verification suite: a). array: - 'array' can be declared with different ranks and index ranges, values assigned to array elements can be changed too. CIVL assertions can be added or changed for checking values of different array elements. * Array expression is not supported yet, so expressions like 'array = 3' (which assigns 3 to each array element) shall be reported as type conversion violation (i.e., integer type can not be converted to array type) b). compound: - Variable p can be assigned with different values and assertions can be modified for different fields in the compound type. c). compute: - Variable and operators can be changed. d). fib: - The recursive function fib(n) can be implemented to calculate different recursive math formula. CIVL assertions can be used for checking the result of fib(n). e). forloop: - The loop variable can be changed with different initial, bound and stride values. The expression in the loop body can also be changed. * CIVL will not check the termination of a loop, so users shall ensure that the loop will terminate eventually. f). function: - The function can be replaced by any other simple math functions, which only have features supported by CIVL Fortran extension. g). hello: - Change '.TRUE.' to '.FALSE.' will result in an assertion violation h). inout: - In Fortran, arguments with a scalar type are passed-by-reference. i). pointer: - The value of 'x' can be changed, and the corresponding assertions shall be updated so that no assertion violation is reported. 3). Nek5000 application examples: a). mxm_pencil: - This example compares the matrix-multiply implementation used by nek5000 with the naive implementation, so that the pencil approach is proved to be correct. - Users can change '-inputBOUND=2' in the verification command to scale the size of input matrices. - Users can make the implementation program 'mxm_pencil.f' incorrect, and then execute a set of verification with BOUND from 2 to 5. Then, at least one execution shall report an assertion violation, because the pencil implementation have distinct branches for matrices with different sizes. * Command used for comparing two programs: > civl compare -inputBOUND=2 -spec mxm_driver.f mxm_naive.f -spec mxm_driver.f mxm_pencil.f b). mxm_unroll: - Users can created their own matrix-multiply unroll implementation and then use civl compare command to check the functional output equivalence between the naive version and user-created version. * Command used for comparing two programs: > civl compare -inputBOUND=3 -spec mxm_driver.f mxm_naive.f -spec mxm_driver.f mxm_unroll3.f c). speclib: - Users can modify the correct subroutine in 'speclib.f' for causing assertion violation or fix the bad version. - This example only support NP from 2 to 3. It requires additional assumptions on trigonometry functions to scale NP. 4). User provided examples: CIVL Fortran extension supports a subset of Fortran. If users would like to test customized examples, it is recommended to start with a smaller or simpler Fortran program derived from provided examples. 8. Misc. 1). CIVL development documents are organized as Java-doc in the source code (Instruction of getting CIVL source code can be found from: http://vsl.cis.udel.edu/lib/sw/civl/trunk/latest/release/index.html ) 2). CIVL JUnit test and coverage test reports can be found from: http://vsl.cis.udel.edu/lib/sw/civl/trunk/latest/ 3). Other information of CIVL can be found from: https://vsl.cis.udel.edu/trac/civl/ 4). SMACK bench can be found from: https://github.com/soarlab/gandalv/ 5). Nek5000 source code can be found from: https://github.com/Nek5000/Nek5000/ 9 Change Log Nov-29-2021 - Add file collect_outputs.awk for extracting artifact execution result data from each .out file * collect_outputs.awk is require to be set as executable by using chmod command. - Update Makefile * Add rules generating .table file by using collect_outputs.awk * Update 'all' rule to run all experiments, then collect output data from outputs from both the machined mentioned in paper and the VM used for artifact submission. - Update README.txt file for changes mentioned above.