source: CIVL/README@ 5d390d68

      CIVL: The Concurrency Intermediate Verification Language
                               v0.15

------------------------------ 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, 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

Developers:

Matthew B. Dwyer
Ziqing Luo
Michael Rogers
Stephen F. Siegel
Manchun Zheng
Timothy K. Zirkel

------------------------------- 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 v 0.14 -------------------------

1. Fixed the bug that erroneously checking mpi processes statuses inside communicators

2. Fixed the bug that invalid command line inputs crash CIVL.

3. Fixed the bug that CIVL mis-handling float-to-int conversion.

4. Fixed the bug that Translation will ignore unused variable erroneously.

5. Fixed the bug that CIVL implementation misses extents information for literal array assignments.

6. Fixed the bug that CIVL didn't report array out of bound error.

7. Fixed performance bug dealing with MPI/link.

8. Fixed the bug that POR didn't recognize input array.

9. Fixed the bug that ABC can't print $forall.

10. Fixed the bug of linkage with bound variables.

11. Improving CIVL by get rid of unnecessary statements enabled from a nondeterministic statement.

12. Support compound literals for input variables.

13. Improves the performance of SARL which also makes CIVL run faster.

14. Makes sources of inserted texts by transformer more clear.

15. Support time.h

16. Implemented fflush()

17. Extended ABC to handle Cuda-c extensions.

18. Simplify array representation in SARL.

   
   
------------------------- 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 the automated theorem prover CVC3 (if you have not already).
The easiest way to do this is to visit

  http://www.cs.nyu.edu/acsys/cvc3/download.html
  
and download the latest, optimized build with static library
and executable for your OS.  Place the executable file "cvc3"
somewhere in your PATH.  You can discard everything else.

Alternatively, on linux systems, CVC3 can be installed
using the package manager via "sudo apt-get install cvc3".
This will place cvc3 in /usr/bin.

2. Install the automated theorem prover CVC4 (if you have not already).
The easiest way to do this is to visit

  http://cvc4.cs.nyu.edu/downloads/

and choose one of the installation approaches.  You only need the
binary (cvc4), and you must put it in your PATH.

3. Install a Java 7 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-7-jdk

4. Download the CIVL distribution from http://vsl.cis.udel.edu/civl.

5. Unzip and untar the downloaded 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

6. Move CIVL-TAG into /opt.   Alternatively, if you don't want to
put it in /opt for some reason, put CIVL-TAG wherever you want
and edit the script (bin/civl) to reflect the chosen path.

7. Put the script bin/civl in your path however you like to put things
in your path.   Either move it to a directory in your path,
or create a symlink to it, or edit your .profile or equivalent
to put it in your path.

8. Type "civl config".  This should report that it found cvc3 and cvc4,
and it should create a file called ".sarl" in your home directory.


------------------------- Source Installation -------------------------

We recommend using the Eclipse IDE for Java/EE developers.

0. Install CVC3 and CVC4 executables 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. 

    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. Download the tgz archive of VSL dependencies from 
   http://vsl.cis.udel.edu/tools/vsl_depend, choosing the right .tgz 
   according to your platform:
        
        vsl_linux32-1.0.tgz     - 32-bit linux
        vsl_linux64-1.0.tgz     - 64-bit linux
        vsl_osx64-1.0.tgz       - 64-bit osx
        
   Unzip the .tgz file and you will have the folder vsl.
   Move vsl to /opt (you might 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).

   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 where build.xml is in.
   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. Navigate to Preferences -> Run/Debug 
   -> String Substitution -> New, and then define an entry vsl_lib and 
   set its value to be /opt/vsl/lib.

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. Go to Run->Run Configurations... Create a new JUnit configuration.
   Name it CIVL 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). Under the Environment tab, create an entry 
   DYLD_LIBRARY_PATH (OS X) or LD_LIBRARY_PATH (linux), 
   specify its value by clicking Variables and choose vsl_lib from the list, 
   or you may type ${vsl_lib} in the value entry.

10. 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"
   (without the quotes).  Modify the VM arguments and the Environment
   as in the step above.  You should now be able to run the test by
   clicking "Run".