| 1 | CIVL: The Concurrency Intermediate Verification Language
|
|---|
| 2 | v 0.8
|
|---|
| 3 |
|
|---|
| 4 | ------------------------------ Overview -------------------------------
|
|---|
| 5 |
|
|---|
| 6 | CIVL is a framework encompassing...
|
|---|
| 7 |
|
|---|
| 8 | * a programming language, CIVL-C, which adds to C a number of
|
|---|
| 9 | concurrency primitives, as well as the ability to define
|
|---|
| 10 | functions in any scope. Together, these features make for
|
|---|
| 11 | a very expressive concurrent language that can faithfully
|
|---|
| 12 | represent programs using various APIs and parallel languages,
|
|---|
| 13 | such as MPI, OpenMP, CUDA, and Chapel. CIVL-C also provides
|
|---|
| 14 | a number of primitives supporting verification.
|
|---|
| 15 | * a model checker which uses symbolic execution to verify a
|
|---|
| 16 | number of safety properties of CIVL-C programs. The model
|
|---|
| 17 | checker can also be used to verify that two CIVL-C programs
|
|---|
| 18 | are functionally equivalent.
|
|---|
| 19 | * a number of translators from various commonly-used languages
|
|---|
| 20 | and APIs to CIVL-C. (This part is still a work in progress.)
|
|---|
| 21 |
|
|---|
| 22 | CIVL is developed by the Verified Software Laboratory at the
|
|---|
| 23 | University of Delaware Department of Computer Science.
|
|---|
| 24 | For more information, visit http://vsl.cis.udel.edu/civl
|
|---|
| 25 |
|
|---|
| 26 | Developers:
|
|---|
| 27 |
|
|---|
| 28 | Stephen F. Siegel
|
|---|
| 29 | Timothy K. Zirkel
|
|---|
| 30 | Manchun Zheng
|
|---|
| 31 | Ziqing Luo
|
|---|
| 32 |
|
|---|
| 33 | ------------------------------- License -------------------------------
|
|---|
| 34 |
|
|---|
| 35 | CIVL is open source software distributed under the GNU
|
|---|
| 36 | General Public License. However, the libraries used by CIVL
|
|---|
| 37 | (and incorporated into the complete distribution) use various
|
|---|
| 38 | licenses. See directory licenses for the license of each component.
|
|---|
| 39 |
|
|---|
| 40 | -------------------------- Updates from v 0.7 -------------------------
|
|---|
| 41 |
|
|---|
| 42 | 1. Dyscopes are now first-class objects, like processes and other types.
|
|---|
| 43 | Refer to CIVL Manual Section 6.2.2 for more details about $scope expressions.
|
|---|
| 44 |
|
|---|
| 45 | 2. Interfaces for message passing are significantly simplified. Refer to
|
|---|
| 46 | CIVL Manual Section 7.3.2 and examples/messagePassing for more details.
|
|---|
| 47 |
|
|---|
| 48 | 3. $wait is not implemented as a system function declared in civlc.h,
|
|---|
| 49 | instead of a language primitive. So the syntax becomes "$wait(p)"
|
|---|
| 50 | instead of "$wait p".
|
|---|
| 51 |
|
|---|
| 52 | 4. There is no longer a $heap type. Instead, every dynamic scope has its
|
|---|
| 53 | own heap automatically. The $malloc function has been modified to take
|
|---|
| 54 | a scope as its first argument, e.g., $malloc($here, sizeof(int)).
|
|---|
| 55 |
|
|---|
| 56 | ------------------------- Binary Installation -------------------------
|
|---|
| 57 |
|
|---|
| 58 | For most users, this will be the easiest way to install and use CIVL.
|
|---|
| 59 |
|
|---|
| 60 | 1. Install a Java 7 SDK if you have not already. Go to
|
|---|
| 61 | http://www.oracle.com/technetwork/java/javase/downloads/ for the
|
|---|
| 62 | latest from Oracle. On linux, you can optionally sudo apt-get install
|
|---|
| 63 | openjdk-7-jdk.
|
|---|
| 64 |
|
|---|
| 65 | 2. If you already have the VSL dependencies library, you may
|
|---|
| 66 | skip this step. Otherwise, download the archive of VSL
|
|---|
| 67 | dependencies from http://vsl.cis.udel.edu/tools/vsl_depend,
|
|---|
| 68 | choosing the version for your OS type (32-bit linux,
|
|---|
| 69 | 64-bit linux, or 64-bit OS X). Unzip and untar the
|
|---|
| 70 | downloaded .tgz file and you will have a folder named "vsl".
|
|---|
| 71 | If you do not already have a directory /opt, create one with
|
|---|
| 72 | "mkdir /opt". Move vsl into /opt. Use sudo as needed.
|
|---|
| 73 |
|
|---|
| 74 | 3. Download the appropriate CIVL distribution from
|
|---|
| 75 | http://vsl.cis.udel.edu/civl.
|
|---|
| 76 |
|
|---|
| 77 | 4. Unzip and untar the downloaded file if this does not happen
|
|---|
| 78 | automatically. This should result in a folder named
|
|---|
| 79 | CIVL-TAG, where TAG is some version id string. This folder
|
|---|
| 80 | contains the following:
|
|---|
| 81 |
|
|---|
| 82 | - README : this file
|
|---|
| 83 | - bin : containing one executable sh script called "civl"
|
|---|
| 84 | - lib : containing civl-TAG.jar
|
|---|
| 85 | - doc : containing the manual and the tutorial of CIVL
|
|---|
| 86 | - licenses : licenses for CIVL and included libraries
|
|---|
| 87 | - examples : some example CIVL programs
|
|---|
| 88 |
|
|---|
| 89 | 5. Move CIVL-TAG into /opt.
|
|---|
| 90 |
|
|---|
| 91 | 6. Put the civl script in your path however you like to put things
|
|---|
| 92 | in your path. Either move it to a directory in your path,
|
|---|
| 93 | or create a symlink to it, or edit your .profile or equivalent
|
|---|
| 94 | to put it in your path.
|
|---|
| 95 |
|
|---|
| 96 | ------------------------- Source Installation -------------------------
|
|---|
| 97 |
|
|---|
| 98 | We recommend using the Eclipse IDE for Java/EE developers.
|
|---|
| 99 |
|
|---|
| 100 | 1. Install prerequisite projects ABC, SARL and GMC.
|
|---|
| 101 | Make sure that the three projects are put in the workspace
|
|---|
| 102 | directory where CIVL will be put.
|
|---|
| 103 |
|
|---|
| 104 | a. Install the C front-end ABC. In Eclipse,
|
|---|
| 105 | select New Project...from SVN, use the archive
|
|---|
| 106 | svn://vsl.cis.udel.edu/abc. After entering that, open it
|
|---|
| 107 | up and select the "trunk". After checking out trunk, name
|
|---|
| 108 | the project "ABC". Then follow the instructions in the INSTALL
|
|---|
| 109 | file for Eclipse installation. Build the abc.jar from within
|
|---|
| 110 | Eclipse by right-clicking (or ctrl-clicking on OS X) on the
|
|---|
| 111 | build.xml file and selecting Run As->Ant Build.
|
|---|
| 112 |
|
|---|
| 113 | b. Install the symbolic algebra and reasoning library SARL.
|
|---|
| 114 | In Eclipse, select New Project...from SVN, use the archive
|
|---|
| 115 | svn://vsl.cis.udel.edu/sarl. After entering that, open it
|
|---|
| 116 | up and select the "trunk". After checking out trunk, name
|
|---|
| 117 | the project "SARL". Then follow the instructions in the INSTALL
|
|---|
| 118 | file for Eclipse installation. Build the sarl.jar from within
|
|---|
| 119 | Eclipse by right-clicking (or ctrl-clicking) on the build.xml
|
|---|
| 120 | file and selecting Run As->Ant Build.
|
|---|
| 121 |
|
|---|
| 122 | c. Install the generic model checking utilities package GMC.
|
|---|
| 123 | In Eclipse, select New Project...from SVN, use the archive
|
|---|
| 124 | svn://vsl.cis.udel.edu/gmc. After entering that, open it
|
|---|
| 125 | up and select the "trunk". After checking out trunk, name
|
|---|
| 126 | the project "GMC". Build the gmc.jar from within Eclipse
|
|---|
| 127 | by right-clicking (or ctrl-clicking) on the build.xml file and
|
|---|
| 128 | selecting Run As->Ant Build.
|
|---|
| 129 |
|
|---|
| 130 | 2. From within Eclipse, select New Project...from SVN. The archive is
|
|---|
| 131 | svn://vsl.cis.udel.edu/civl. After entering that, open it up and
|
|---|
| 132 | select the "trunk". (It is simplest to just check out the trunk for
|
|---|
| 133 | the Eclipse project.)
|
|---|
| 134 |
|
|---|
| 135 | 3. Check out the trunk, and create the project using the New Java
|
|---|
| 136 | Project Wizard as usual, naming it "CIVL". The .project, .classpath,
|
|---|
| 137 | and other Eclipse meta-data are already in the SVN archive, saving you
|
|---|
| 138 | a bunch of work.
|
|---|
| 139 |
|
|---|
| 140 | 4. If you already have the VSL dependencies library, you may
|
|---|
| 141 | skip this step.
|
|---|
| 142 |
|
|---|
| 143 | Download the tgz archive of VSL dependencies from
|
|---|
| 144 | http://vsl.cis.udel.edu/tools/vsl_depend,
|
|---|
| 145 | choosing the right .tgz according to your platform:
|
|---|
| 146 |
|
|---|
| 147 | vsl_linux32-1.0.tgz - 32-bit linux
|
|---|
| 148 | vsl_linux64-1.0.tgz - 64-bit linux
|
|---|
| 149 | vsl_osx64-1.0.tgz - 64-bit osx
|
|---|
| 150 |
|
|---|
| 151 | Unzip the .tgz file and you will have the folder vsl.
|
|---|
| 152 | Move vsl to /opt (you might need to use sudo for this.
|
|---|
| 153 | Also, if you don't already have a directory called /opt,
|
|---|
| 154 | you will have to create it with mkdir /opt).
|
|---|
| 155 |
|
|---|
| 156 | Suppose that you put the .tgz file (or .tar file if your browser
|
|---|
| 157 | unzipped it automatically to a .tar file) in the directory $Download.
|
|---|
| 158 | You can use the following commands:
|
|---|
| 159 |
|
|---|
| 160 | $ cd $Download
|
|---|
| 161 | $ tar xzf YourTgzOrTarFile vsl
|
|---|
| 162 | $ sudo mv vsl /opt
|
|---|
| 163 |
|
|---|
| 164 | Now you can type "ls /opt/vsl", and the output should be
|
|---|
| 165 |
|
|---|
| 166 | README.txt lib licenses src
|
|---|
| 167 |
|
|---|
| 168 | 5. Create a file build.properties in the directory where build.xml is in.
|
|---|
| 169 | Copy and paste the content from properties/build.properties.osx or
|
|---|
| 170 | properties/build.properties.linux depending on your platform.
|
|---|
| 171 | If your workspace directory is the default setting of Eclipse,
|
|---|
| 172 | i.e., HOME/Documents/workspace for osx or HOME/workspace for linux,
|
|---|
| 173 | then you dont have to anything.
|
|---|
| 174 | Otherwise, you need to edit the entry "workspace" to point to the
|
|---|
| 175 | corresponding directory where you put the projects ABC, SARL and GMC.
|
|---|
| 176 |
|
|---|
| 177 | 6. Navigate to Preferences -> Java -> Build Path -> ClassPath
|
|---|
| 178 | Variables, and then select New to create a classpath variable VSL,
|
|---|
| 179 | and specify its value to be /opt/vsl. Navigate to Preferences -> Run/Debug
|
|---|
| 180 | -> String Substitution -> New, and then define an entry vsl_lib and
|
|---|
| 181 | set its value to be /opt/vsl/lib.
|
|---|
| 182 |
|
|---|
| 183 | 7. Do a clean build. Everything should compile. Generate the civl.jar
|
|---|
| 184 | by right-clicking (or ctrl-click on OS X) the build.xml file and
|
|---|
| 185 | Run As->Ant Build.
|
|---|
| 186 |
|
|---|
| 187 | 8. Go to Run->Run Configurations... Create a new JUnit configuration.
|
|---|
| 188 | Name it CIVL Tests. Select "Run all tests in the selected project..."
|
|---|
| 189 | and navigate to the folder "test" in the CIVL project.
|
|---|
| 190 | The Test runner should be JUnit 4. Under the Arguments tab, type
|
|---|
| 191 | "-ea" (without the quotes) in the VM arguments area (to enable assertion
|
|---|
| 192 | checking). Under the Environment tab, create an entry
|
|---|
| 193 | DYLD_LIBRARY_PATH (OS X) or LD_LIBRARY_PATH (linux),
|
|---|
| 194 | specify its value by clicking Variables and choose vsl_lib from the list,
|
|---|
| 195 | or you may type ${vsl_lib} in the value entry.
|
|---|
| 196 |
|
|---|
| 197 | 9. An example of how to set up a single test from within Eclipse:
|
|---|
| 198 | create a new Run Configuration via the Run->Run
|
|---|
| 199 | Configurations... menu. Create a new "Java Application"
|
|---|
| 200 | configuration. Call it "CIVL barrier2". The Project is CIVL. The
|
|---|
| 201 | main class is edu.udel.cis.vsl.civl.CIVL. Under the Arguments tab,
|
|---|
| 202 | set the Program arguments to "examples/barrier2.cvl" (without the
|
|---|
| 203 | quotes). Modify the VM arguments and the Environment as in the step
|
|---|
| 204 | above. You should now be able to run the test by clicking "Run".
|
|---|
