CIVL: The Concurrency Intermediate Verification Language v1.21 ------------------------------ Overview ------------------------------- CIVL is a framework encompassing... * a programming language, CIVL-C, which adds to C a number of concurrency primitives, as well as the ability to define functions in any scope. Together, these features make for a very expressive concurrent language that can faithfully represent programs using various APIs and parallel languages, such as MPI, OpenMP, Pthread, CUDA, and Chapel. CIVL-C also provides a number of primitives supporting verification. * a model checker which uses symbolic execution to verify a number of safety properties of CIVL-C programs. The model checker can also be used to verify that two CIVL-C programs are functionally equivalent. * a number of translators from various commonly-used languages and APIs to CIVL-C. (This part is still a work in progress.) CIVL is developed by the Verified Software Laboratory at the University of Delaware Department of Computer Science. For more information, visit http://vsl.cis.udel.edu/civl Active Developers: Matthew B. Dwyer Mitchell Gerrard Ziqing Luo Stephen F. Siegel Wenhao Wu Alexander Wilton Inactive Developers: John Edenhofner Andre Marianiello Michael Rogers Timothy K. Zirkel Si Li Manchun Zheng Yihao Yan ------------------------------- License ------------------------------- CIVL is open source software distributed under the GNU General Public License. However, the libraries used by CIVL (and incorporated into the complete distribution) use various licenses. See directory licenses for the license of each component. -------------------------- Updates from v1.20 ------------------------- -- 1. refine the Fortran extension for paper submitted to TACAS 2022 1.1 Complete Fortran Array Descriptor for tracking changes made on index ranges by array section and reshape operations. Any declared array type is transformed into a Fortran array descriptor by Fortran to CIVL-C AST transformer. 1.2 Introduce four basic CIVL verification primitives Fortran bindings 1.2.1 Type qualifiers: - !$CVL $input: indicates that all variables declared immediately in the next line are symbolic and read-only. - !$CVL $output: indicates that all variables declared immediately in the next line are write-only and used for verifying functional output equivalence. A type declaration statement is required to be used immediately after any CIVL type qualifier and variables qualified shall follow read/write constraints mentioned above. CIVL assumption primitives can be used for limiting the value range of variables qualified by '!$CVL $input'. e.g., !$CVL $input integer :: n, a(n) !! both 'n' and elements of 'a' are symbolic and read-only !$CVL $output integer :: sum !! sum is write-only and can be used for comparing with another !! program, which also has 'sum' with a same type and qualified !! by '!$CVL $output' 1.2.2 Verification - !$CVL $assume(logic_expr); Make CIVL only explores paths, whose path conditions shall make 'logic_expr' to be true. Set the value range for varialbes qualified by '!$CVL $input' - !$CVL $assert(logic_expr); Checks predicates representing specific correctness properties that users expect to verify. If any CIVL assertion primitive is evaluated as false, then CIVL shall report an assertion violation. 1.3 Add supports for additional Fortran features include: 1.3.1 'inout' and 'out' attributes declared by 'intent' statement 1.3.2 compound types with fields having scalar types. 1.3.3 pointer types to scalar types. 1.3.4 logic expression evaluation without short-circuits 1.3.5 line truncation for fixed and free forms 1.3.6 other features are shown here: https://vsl.cis.udel.edu/trac/civl/wiki/FortranTransformations 1.4 Add test cases imported from SMACK verification suite https://github.com/soarlab/gandalv/ 2. CUDA Support Improvement 2.1 Fixed CUDA bug in which CUDA kernel declarations were not being transformed properly 2.2 Fixed source info bug (completeSources wasn’t being called everywhere that it should) 2.3 Fixed short circuit bug described in ticket #943 2.4 Added small optimization to short circuit transformer to allow for finer granularity of its transformation 3. Other Improvement and Fixed Bugs 3.1 MPI_Comm types can be compared by equality operator ('=='). 3.2 Java-Doc improvements -------------------------- Updates from v1.19 ------------------------- -- 1. added new language primitives: 1.1 $local_start() and $local_end() An execution of the statements in between of this pair, including this pair themselves, is NOT ONLY uninterruptable BUT ALSO purely local to the view of the verifier. 1.2 $read_set_push() and $read_set_pop() (the correspondence for write set has already been supported) This pair of primitives can be used to turn on/off the capturing of read set during execution. -- 2. added Fortran support for translating basic Fortran features into CIVL-AST (see: https://vsl.cis.udel.edu/trac/civl/wiki/FortranTransformations) -- 3. added simple Fortran verification examples (edited) ------------------------- Binary Installation ------------------------- For most users, this will be the easiest way to install and use CIVL. Developers should instead follow the instructions for "Source Installation" below. 1. Install at least one of the theorem provers below. The more provers you install, the more precise CIVL analysis will be. Note that CIVL only requires the binary executable version of each prover; you can ignore the libraries, various API bindings, etc. You just need to ensure that each binary executable is in your PATH when you run "civl config". The currently supported provers are: - CVC3, http://www.cs.nyu.edu/acsys/cvc3/download.html download the latest, optimized build with static library and executable for your OS. Place the executable file "cvc3" in your PATH. You can discard everything else. Alternatively, on some linux systems, CVC3 can be installed using the package manager via "sudo apt-get install cvc3". This will place cvc3 in /usr/bin. - CVC4, http://cvc4.cs.nyu.edu/downloads/ - Z3, http://z3.codeplex.com/SourceControl/latest 2. Install a Java 8 SDK if you have not already. Go to http://www.oracle.com/technetwork/java/javase/downloads/ for the latest from Oracle. On linux, you can instead use the package manager: sudo apt-get install openjdk-8-jdk 3. Download the CIVL distribution from http://vsl.cis.udel.edu/civl. 4. Unzip and untar the CIVL distribution file if this does not happen automatically. This should result in a folder named CIVL-TAG, where TAG is some version ID string. This folder contains the following: - README : this file - bin : containing one executable sh script called "civl" - lib : containing civl-TAG.jar - doc : containing the manual and the tutorial of CIVL - emacs : CIVL-C emacs mode and its installation instructions - licenses : licenses for CIVL and included libraries - examples : some example CIVL programs 5. You can move the CIVL folder wherever you want. The JAR file in the lib directory is all you need to run CIVL. You may also move this jar file wherever you want. You run CIVL by typing a command that begins "java -jar /path/to/civl-TAG.jar ...". For convenience you may instead use the shell script "civl" in bin, which allows you to replace "java -jar /path/to/civl-TAG.jar" with just "civl" on the command line. Simply edit the civl script to reflect the path to civl-TAG.jar and place the script somewhere in your PATH. Alternatively, you can just define an alias in your .profile, .bash_profile, or equivalent, such as alias civl='java -jar /path/to/civl-TAG.jar' In the following, we will assume that you have defined a command "civl" in one these ways. 6. Type "civl config". This should report that it found the theorem provers you installed (and are in your PATH). It should create a file called ".sarl" in your home directory which you can also edit by hand. ------------------------- Source Installation ------------------------- We recommend using the Eclipse IDE for Java/EE developers. 0. Install theorem provers following the directions above. Install Eclipse IDE for Java/EE developers if you have not already done so. 1. Install an SVN plugin in Eclipse (such as Subversive) if you have not already. 2. Install prerequisite projects ABC, SARL and GMC. Make sure that the three projects are put in the workspace directory where CIVL will be created. Specifically: a. Install the symbolic algebra and reasoning library SARL. In Eclipse, select New Project...from SVN, use the archive svn://vsl.cis.udel.edu/sarl. After entering that, open it up and select the "trunk". After checking out trunk, name the project "SARL". Then follow the instructions in the INSTALL file for Eclipse installation. Build the sarl.jar from within Eclipse by right-clicking (or ctrl-clicking) on the build.xml file and selecting Run As->Ant Build. b. Install the C front-end ABC. In Eclipse, select New Project...from SVN, use the archive svn://vsl.cis.udel.edu/abc. After entering that, open it up and select the "trunk". After checking out trunk, name the project "ABC". Then follow the instructions in the INSTALL file for Eclipse installation. Build the abc.jar from within Eclipse by right-clicking (or ctrl-clicking on OS X) on the build.xml file and selecting Run As->Ant Build. c. Install the generic model checking utilities package GMC. In Eclipse, select New Project...from SVN, use the archive svn://vsl.cis.udel.edu/gmc. After entering that, open it up and select the "trunk". After checking out trunk, name the project "GMC". Build the gmc.jar from within Eclipse by right-clicking (or ctrl-clicking) on the build.xml file and selecting Run As->Ant Build. 3. From within Eclipse, select New Project...from SVN. The archive is svn://vsl.cis.udel.edu/civl. After entering that, open it up and select the "trunk". (It is simplest to just check out the trunk for the Eclipse project.) 4. Check out the trunk, and create the project using the New Java Project Wizard as usual, naming it "CIVL". The .project, .classpath, and other Eclipse meta-data are already in the SVN archive, saving you a bunch of work. 5. If you already have the VSL dependencies library, you may skip this step. Otherwise, download the tgz archive of VSL dependencies from http://vsl.cis.udel.edu/lib/tools/vsl_depend Unzip the .tgz file and you will have the folder vsl. Move vsl to /opt. Note: you probably will need to use sudo for this. Also, if you don't already have a directory called /opt, you will have to create it with "mkdir /opt". Also, if you don't want to use /opt for some reason, you can use any directory you want; just modify the instructions below accordingly. Suppose that you put the .tgz file (or .tar file if your browser unzipped it automatically to a .tar file) in the directory DOWNLOAD. You can use the following commands: $ cd DOWNLOAD $ tar xzf YourTgzOrTarFile vsl $ sudo mv vsl /opt (Leave out the "x" in the tar command if the file was already unzipped.) Now you can type "ls /opt/vsl", and the output should be README.txt lib licenses src 6. If default_build.properties matches the configuration of your system, then you can skip this step. Otherwise, you may need to create a file build.properties in the directory containing build.xml. Copy and paste the content from any file under properties, edit each entry with the path configured in your system. The newly created file build.properties will automatically be used by ant to to build the .jar file. 7. Navigate to Preferences -> Java -> Build Path -> ClassPath Variables, and then select New to create a classpath variable VSL, and specify its value to be /opt/vsl. 8. Do a clean build. Everything should compile. Generate the civl.jar by right-clicking (or ctrl-click on OS X) the build.xml file and Run As->Ant Build. 9. Shortcuts for running CIVL Somewhere on your system, create a plain text file containing exactly the following two lines: #!/bin/sh java -jar /Path/To/Your/workspace/CIVL/civl.jar $@ where "/Path/To/Your/workspace" is replaced with the path to your Eclipse workspace directory. Name this file "civl", put it in your PATH, and make it executable (chmod ugo+x civl). 10. From a terminal window, execute "civl config". This should find the theorem provers in your PATH and create a file .sarl in your home directory. 11. In Eclipse, navigate to "Run->Run Configurations... Create a new JUnit configuration." Name it "CIVL Regression Tests". Select "Run all tests in the selected project..." and navigate to the folder "test/regress" in the CIVL project. The Test runner should be JUnit 4. Under the Arguments tab, type "-ea" (without the quotes) in the VM arguments area (to enable assertion checking). 12. An example of how to set up a single test from within Eclipse: create a new Run Configuration via the Run->Run Configurations... menu. Create a new "Java Application" configuration. Call it "CIVL barrier2". The Project is CIVL. The main class is edu.udel.cis.vsl.civl.CIVL. Under the Arguments tab, set the Program arguments to verify examples/concurrency/barrier2.cvl Modify the VM arguments as in the step above. You should now be able to run the test by clicking "Run".