                               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

Building TASS from Source:  TASS requires the following external
software systems:

   Ant
   CVC3
   ANTLR
   JUnit

1. Download and build CVC3 with Java.  See
http://cs.nyu.edu/acsys/cvc3/download.html and follow the instructions
for building with Java.  Put the CVC3 directory anywhere you like.
Let's call this directory CVC3DIR.  If everything worked correctly,
CVC3DIR should now contain a file java/lib/libcvc3.jar.

2. Get the ANTLR v3 runtime library.  See
http://www.antlr.org/download.html.  This can be the jar file for the
complete ANTLRWorks + ANTLR distribution (which will be called
something like antlrworks-*.jar), or the jar file for just the
complete ANTLR distribution (antlr-3.x.jar), or the jar file for just
the ANTLR runtime (antlr-runtime-3.x.jar).  Any of these will do, and
all three are available from the ANTLR web site.  Put this anywhere
you like.

3. Get the Cobertura runtime library.  See
http://cobertura.sourceforge.net/download.html.  Put this anywhere you
like.

4. Get the JUnit 4 jar file.  See
http://sourceforge.net/projects/junit/files/junit/.  This will be
called something like junit-4.x.jar.  Put this anywhere you like.

5. Ant is pretty standard, but if you don't already have it, download
and install: http://ant.apache.org/.

6. Download, gunzip, and untar the tass distribution.  Put anywhere
you like.  Let us call the main directory created TASSDIR.

7. Create a file in TASSDIR called build.properties.  Model it off of
one of the examples in TASSDIR/config.  This gives paths for the four
required systems ANTLR, JUnit, Cobertura, and CVC3.  The file will be 4 lines
long and look something like this:

antlr3-lib.name=/Applications/ANTLRWorks.app/Contents/Resources/Java/antlrworks.jar
junit.name=/tools/junit4.4/junit-4.4.jar
cvc3.dir=/tools/cvc3-20090309
cobertura.lib.dir=/usr/local/apps/cobertura

8. From within the TASSDIR directory, type "ant".  This should build
the entire TASS system and create MiniMP.jar and an executable script
file called tass in TASSDIR.  Put tass somewhere in your path.

9. To run the JUnit test suite, just type "ant test" from within
TASSDIR.  This will run all of the tests and generate HTML reports
summarizing the results.


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