/==============================================================================================================================/ / Title: GPU Acceleration of Bounded Model Checking with ParaFROST / Objective : Test and evaluate ParaFROST integration with CBMC / Soft Prerequisites: cuda screen python3.8 pip matplotlib numpy / Hard Prerequisites: CUDA-enabled GPU machine with minimum: / 5.0 compute capability / 16 GB system memory / 12 GB device memory / Graphics driver v455 or later / Ubuntu, at least version 18.04 /==============================================================================================================================/ 0) How to evaluate this artifact? --------------------------------- Unpack the ZIP-file on a machine running Ubuntu, at least version 18.04, equipped with at least (1) NVIDIA GPU. Proceed with the next step below. ================================================================================================================================= 1) How to install all tools in the artifact? -------------------------------------------- - First install all the artefact scripts dependencies by running the command sudo apt install flex bison (required by CBMC) sudo apt install python3.8 python3.8-dev python3.8-distutils python3.8-venv python3-pip python3.8 -m pip install -U pip python3.8 -m pip install -U numpy python3.8 -m pip install -U matplotlib - Second install CUDA 11.0 or later, if not already available on your machine. Installing CUDA --------------- - Install the CUDA driver (450 or later) through the software manager in Ubuntu. Reboot your machine. You can now verify whether this worked by running: nvidia-smi You should get output similar to this, indicating the presence of your GPU: +-----------------------------------------------------------------------------+ | NVIDIA-SMI 450.66 Driver Version: 450.66 CUDA Version: 11.0 | |-------------------------------+----------------------+----------------------+ | GPU Name Persistence-M| Bus-Id Disp.A | Volatile Uncorr. ECC | | Fan Temp Perf Pwr:Usage/Cap| Memory-Usage | GPU-Util Compute M. | | | | MIG M. | |===============================+======================+======================| | 0 TITAN RTX Off | 00000000:01:00.0 Off | N/A | | 41% 42C P8 36W / 280W | 226MiB / 24220MiB | 0% Default | | | | N/A | +-------------------------------+----------------------+----------------------+ - Next, download and install CUDA using the commands: wget https://developer.download.nvidia.com/compute/cuda/repos/ubuntu1804/x86_64/cuda-ubuntu1804.pin sudo mv cuda-ubuntu1804.pin /etc/apt/preferences.d/cuda-repository-pin-600 sudo apt-key adv --fetch-keys https://developer.download.nvidia.com/compute/cuda/repos/ubuntu1804/x86_64/7fa2af80.pub sudo add-apt-repository "deb https://developer.download.nvidia.com/compute/cuda/repos/ubuntu1804/x86_64/ /" sudo apt-get update sudo apt-get -y install cuda How to compile CBMC with ParaFROST and MiniSat? ----------------------------------------------- The good news is we have an all-in-one script for that, all you need to do is running the script 'install.sh' in "artifact/cbmc". It will download our interface gpu4bmc (https://github.com/muhos/gpu4bmc) which has its own installer for building CBMC v5.31 with ParaFROST v2.2.3 (both GPU and CPU versions). In addition, the script will try to install CBMC + MiniSat 2.2.1. After the installation runs its course, the binaries (cbmc_parafrost_cpu, cbmc_parafrost_gpu, cbmc_minisat) should be in "artifact/cbmc/bin". ================================================================================================================================= 2) Running artifact script to produce the experimental results reported in the paper ------------------------------------------------------------------------------------- Since running all experiments in the paper will take much longer than 5 hours, we categorized all AWS proofs w.r.t. their verified time by ParaFROST-GPU-NoMDM into 3 difficulty modes in "artifact/proofs/[easy][medium][hard][all].list". Each difficulty mode of the proof list (i.e. .list) has the following characteristics: - easy: has 125 proofs and takes around 4 hours or less to verify within a time limit of 230 seconds per proof. - medium: has 11 proofs and takes around 8 hours or less to verify within a time limit of 630 seconds per proof. - hard: has 19 proofs and takes around 2 days or more to verify within a time limit of 3600 seconds per proof. - all: has all proofs (168 including 13 unverified within 3600 seconds) and takes around 4 days or more to verify within a time limit of 3600 seconds per proof. Run the "easy.sh" script for example in the "artifact" folder to produce the same figures and the table reported in the paper using the proofs listed in the "artifact/proofs/easy.list". All figures will be printed in high resolution in PDF format and can be found in the "artifact/results" folder after the artifact runs successfully. The table will be printed both on 'screen' and in a comma-separated file in "artifact/results". The same applies on "medium.sh", "hard.sh", and "all.sh" scripts. The runtim figures (figure 4) will be found in: - "artifact/results/verify_time.pdf" (plot (a)) - "artifact/results/simplify_percentage.pdf" (plot (b)) The table will be found on screen and in "artifact/results/performance.csv". Complete log files of all CBMC experiment can be checked in "artifact/results/logs". ================================================================================================================================= 3) More info. on CBMC + ParaFROST --------------------------------- Follow the guidlines by CBMC authors in (http://www.cprover.org/cprover-manual/cbmc/tutorial/) to test and run CBMC. ParaFROST solver can be fully configured within CBMC via editing the configuration file in: 'artifact/cbmc/gpu4bmc/interface/satcheck-parafrost/parafrost_config.ini' Upon running CBMC, the solver will check first the configuration file automatically from the above location. The location can be changed by setting the enviromental variable 'PFROSTCONFIG' ParaFROST source code is accessable online via https://github.com/muhos/ParaFROST. The solver interface with CBMC and all necessary patches to compile the GPU version with CBMC is available in: https://github.com/muhos/gpu4bmc. =================================================================================================================================