                               TASS 1.0
             The Toolkit for Accurate Scientific Software

                               1. About

TASS is a suite of integrated tools for the formal verification of
programs used in computational science, including
message-passing-based parallel programs.  TASS uses symbolic execution
and model checking techniques to verify a number of standard safety
properties (such as absence of deadlocks and out-of-bound references),
but its most innovative feature is the ability to establish that two
programs are functionally equivalent.  This is particularly useful in
scientific computing, where developers often start with a simple
sequential encoding of an algorithm, then gradually transform this
into a production code by introducing parallelism and a host of other
optimizations by hand.  The final implementation is intended to be
functionally equivalent to the original specification, but this is
generally extremely difficult to check.

TASS is developed in the Verified Software Laboratory in the
Department of Computer and Information Sciences at the University of
Delaware.  See http://vsl.cis.udel.edu/tass for more information.


                               2. Usage

Currently TASS accepts programs written in the MiniMP dialect of C.
Support for all of C, C++, and Fortran, all wtih MPI, is in progress.

Command-line usage:

            tass verify [options] model.mmp 
            tass compare [options] spec.mmp impl.mmp
            tass extract model.mmp 
            tass gui
Options: 
   -np=N                : number of processes [default=1], used in Verify or Extract mode.
   -np1=N               : number of processes for specification program [default=1], used in Compare mode.
   -np2=N               : number of processes for implementation program [default=1], used in Compare mode.
   -reduce=std          : no partial order reduction [default]
   -reduce=urgent       : urgent partial order redunction
   -deadlock=absolute   : check for absolute deadlocks only [default]
   -deadlock=potential  : check for potential deadlocks (includes absolute)
   -deadlock=ignore     : ignore all deadlocks
   -verbose             : print detailed model and state information
   -debug               : print debugging information
   -nosimplify          : do not simplify symbolic expressions [default: simplify]
   -buffer=N            : max number buffered messages [default=10]
   -loop                : use method of loop co-invariants [default: off]


                           3. Installation
                           
Binary Installation: 
For most users, this will be the easiest way to install and
use TASS.  Developers should instead follow the instructions for
"Source Installation" below.

1. 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/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

2. 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

3. Download the TASS distribution from http://vsl.cis.udel.edu/tass.

4. Unzip and untar the TASS distribution file if this
does not happen automatically.  This should result in a
folder named TASS-TAG, where TAG is some version ID string.
This folder contains the following:

 - README   : this file
 - bin      : containing one executable sh script called "tass"
 - lib      : containing TASS-TAG.jar
 - LICENSE  : license for TASS
 - examples : some example TASS programs

5.  You can move the TASS folder wherever you want.
The shell script "tass" in the bin directory is all 
you need to run TASS. Place the script somewhere in 
your PATH.   Alternatively, you can just define an alias 
in your .profile, .bash_profile, or equivalent, such as

alias tass='/path/to/tass'



Source Installation:  
TASS requires the following external software systems:

   Ant
   CVC3
   ANTLR
   JUnit
   

1. 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 optionally sudo apt-get install
openjdk-7-jdk.

2. Install Apache ant, if you don't already have it
(http://ant.apache.org).

3. 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

   Now you can type "ls /opt/vsl", and the output should be

   		README.txt    lib        licenses    src

4. svn checkout svn://vsl.cis.udel.edu/tass/trunk tass

5. cd tass

6.  Look at build_default.properties and see if the paths
are correct for your system.  If they are not, you will have
to create a file called build.properties (in the same directory),
copying the content of build_default.properties, but correcting
values as necessary.  For example, if your VSL dependencies path
is not in /opt/vsl, then you need to do this,
modifying the value of entry "root" to be the path to your
VSL dependencies folder.  

7. Type "ant" and everything should build without warnings or errors
and produce abc.jar.  Type "ant test" to run a JUnit test suite.  All
tests should pass.


                              4. License

TASS is copyright 2010, Stephen F. Siegel

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or (at
your option) any later version.

This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program.  If not, see http://www.gnu.org/licenses/.
