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