Things To Do

Release 1.0

Release 1.0 is scheduled for June 15, 2010. This is the first public release of TASS. Here is a list of features we expect in the release:

Implement library framework, including

• MPI_Send, MPI_Recv, MPI_Comm_rank, MPI_Comm_size, MPI_Init, MPI_Finalize, MPI_Sendrecv, MPI_Bcast, MPI_Reduce, MPI_Allreduce, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_INT, MPI_DOUBLE, MPI_FLOAT, MPI_Comm, MPI_COMM_WORLD, ...
• stdio: FILE, fopen, fclose, fprintf, fscanf, fread, fwrite, fseek
• stdlib: malloc, free, NULL, abs, atoi, atof, atol, exit, rand, RAND_MAX
• string: strlen, strcpy, memcpy, strcmp, strncmp
• math: pow, sin, cos, tag, exp, fabs

Tim's Goals

• fix FEVS repository
• fix integrator example
• get source/binary release process fixed

Steve's JUne 15 Goals

• add garbage collection
• fix cycle problem in dynamic type system

Ben's June 15 Goals

• ability to parse and generate TASS models from the FEVS examples using LLVM
  • ​http://vsl.cis.udel.edu/fevs

Yi's June 15 Goals

Other

• the MiniMP front-end we have been using
• A C front-end, supporting at least a subset of C, with either pragmas or type qualifiers used to provide the meta-information needed by TASS.
• XML representation of a model, including a model extractor which takes C source and produces a model in XML format, and the ability to read the XML file and construct a model from it
• convenient binary packaging that bundles everything together and makes installation as easy as possible. Versions for OS X, Windows, and linux (32- and 64-bit in each case).
• relatively complete HTML documentation on the TASS web page: background, usage, MiniMP language reference, TASS Intermediate Representation (including XML)
• bigger, more complex examples (e.g., laplace)
• complete javadocs

General To-Do Items

• add good Javadocs for all public methods, classes, and packages
• achieve much better statement and branch coverage in JUnit tests

Symbolic Module

Is the assumption argument necessary? Is it ever used for anything? How about removing it?

Check out other automated theorem provers:

• ​http://symbolaris.com/orbital/index.html
• ​http://yices.csl.sri.com/

Examples

Parameters

Library Functions

A reference to standard library files is here: ​http://www.utas.edu.au/infosys/info/documentation/C/CStdLib.html

Special functions that are currently included in the grammar can instead be treated just like any other function and "linked in" at a later stage. This will simplify the grammar and front-end. Functions that can be removed include send, recv, allocate, deallocate.

When ModelIF.complete is invoked, it will look for functions which are called but not defined. It will then look through a standard library for a function of the correct name, and add that function to the process containing the call.

Note: allocate takes a type argument, so we should also add to the grammar a new expression sizeof(type). The semantics module will associate a special symbolic constant to this expression, corresponding to the type (e.g., SIZEOF_INT). We can then replace our allocate and deallocate with the standard C functions malloc and free

Some libraries add state: shared state and process global state. How do manage this?

When a library is included into a model, it may add shared variables to the model. When it is attached to a process it may add process-global variables.

Define class Library, LibraryFunction.

attachToModel(ModelIF); attachToProcess(ProcessIF);

in ModelIF, ProcessIF, etc.: getFunctionWithName("fprintf") will return the function if it has been added.

FunctionIF: boolean field: isSystemFunction. If true, function does not have body (locations). Instead, a special class will be loaded to execute this function's transformation of the state when it is invoked.

add module library, submodule of model. also add system level function definition in semantics, next to Executor.