==================================== Installation ==================================== Getting GPUVerify ================= Prebuilt versions of GPUVerify are available in two different ways. * :ref:`docker_containers` * :ref:`nightly_builds` .. _docker_containers: Docker containers ----------------- `Docker `_ is a technology for packaging entire applications into containers to provide a light-weight (compared to VMs) and portable way to run applications in an isolated and reproducable environment. We provide two different images (the difference is each one uses a different SMT solver) for building GPUVerify containers. Installing Docker ^^^^^^^^^^^^^^^^^ See this `guide on installing Docker `_ to learn how to install it. Z3 image ^^^^^^^^ This container uses Z3 as its SMT solver. To obtain the image run:: $ docker pull delcypher/gpuverify-docker:z3 CVC4 image ^^^^^^^^^^ This container uses CVC4 as its SMT solver. To obtain the image run:: $ docker pull delcypher/gpuverify-docker:cvc4 Running GPUVerify in a container ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The easiest way to get started is to create a new container from the GPUVerify image you obtained and run an interactive shell in it (replace ``cvc4`` with ``z3`` if you pulled the ``z3`` image instead of the ``cvc4`` image):: $ docker run -ti --rm --entrypoint=/bin/bash delcypher/gpuverify-docker:cvc4 The ``--rm`` flag will remove the container once you exit (don't use this flag if you want to keep the container). Inside the container the GPUVerify tool is in your ``PATH`` so you can run for example:: $ gpuverify --help The container will have some toy kernels that are part of its testsuite in ``/home/gv/gpuverify/testsuite/`` but you probably want to verify some real kernels. To do that you will want to get some kernels into the container so you can verify them. To do this you can create a volume inside the container that mounts a directory on the underlying host machine. For example the following would make the ``/path/to/kernel`` directory visible inside the container as ``/mnt``:: $ docker run -ti --rm -v /path/to/kernels:/mnt --entrypoint=/bin/bash delcypher/gpuverify-docker:cvc4 Building the GPUVerify image from scratch ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The ``Dockerfile``\ s for building our Docker images can be found in `this GitHub repository `_. .. _nightly_builds: Nightly builds -------------- We build nightly drops for Linux and Windows. These can be found on the GPUVerify `Download `_ page. Basic Prequisites ^^^^^^^^^^^^^^^^^ GPUVerify requires python >= 2.7 and the python module `psutil `_. On Windows, we recommend installing psutil from a `prebuilt binary `_. On Linux/OSX, we recommend installing psutil with pip:: $ pip install psutil On Windows, the 32-bit version of the `Visual C++ Redistributable for Visual Studio 2012 `_ is also required. The redistributable will already be installed if a recent version of Visula Studio is present. If not, a version can be obtained for free from Microsoft through the above link. Not having the redistributable installed may lead to crashes. Linux/OSX ^^^^^^^^^ To install GPUVerify follow this guide in a bash shell. Note ``${INSTALL_ROOT}`` refers to where ever you wish to install GPUVerify. Replace as appropriate or setup an environment variable.:: $ export INSTALL_ROOT=/path/to/install #. Obtain Mono from ``_ and install. #. Download the Linux 64-bit toolchain zip file from the GPUVerify `Download `_ page. Please contact us if you require a 32-bit version. #. Now unpack the zip file:: $ cd ${INSTALL_ROOT} $ unzip GPUVerifyLinux64-nightly.zip This should unpack the GPUVerify toolchain into a path like ``2013-06-11``, which is the date that the tool was packaged. #. Finally, run the GPUVerify test suite.:: $ cd ${INSTALL_ROOT}/2013-06-11/gpuverify $ ./gvtester.py --write-pickle run.pickle testsuite/ You should check that your test run matches the current baseline. :: $ ./gvtester.py --compare-pickle testsuite/baseline.pickle run.pickle You should expect the last line of output to be.:: INFO:testsuite/baseline.pickle = new.pickle This means that your install passes the regression suite. Windows ^^^^^^^ To install GPUVerify follow this guide in a powershell window. Note ``${INSTALL_ROOT}`` refers to where ever you wish to build GPUVerify. Replace as appropriate or setup an environment variable.:: > ${INSTALL_ROOT}=C:\path\to\install We recommend that you install GPUVerify to a local hard drive like ``C:`` since this avoids problems with invoking scripts on network mounted drives. #. Download the Windows 64-bit toolchain zip file from the GPUVerify `Download `_ page. Please contact us if you require a 32-bit version. #. Right-click on the zip file and select "Properties". Now unblock the zip file by clicking on "Unblock" next to "Security". #. Now unpack the zip file:: > cd ${INSTALL_ROOT} > unzip GPUVerifyWindows64-nightly.zip This should unpack the GPUVerify toolchain into a path like ``2013-06-11``, which is the date that the tool was packaged. #. Finally, run the GPUVerify test suite.:: > cd ${INSTALL_ROOT}\2013-06-11\gpuverify > ./gvtester.py --write-pickle run.pickle testsuite/ You should check that your test run matches the current baseline. :: > ./gvtester.py --compare-pickle testsuite/baseline.pickle run.pickle You should expect the last line of output to be.:: INFO:testsuite/baseline.pickle = new.pickle This means that your install passes the regression suite.