Things To Do

Release 1.0

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

• 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

• change names of MiniMP to TASS throughout project
  • for example, in the URL for test data, in the name of the package edu.udel.cis.vsl.minimp, and so on. The name "MiniMP" should only be used for the language.
• add good Javadocs for all public methods, classes, and packages
• achieve much better statement and branch coverage in JUnit tests
• create separate test tree which mirrors the source tree but contains only JUnit tests

Symbolic Module

Consider re-designing the symbolic module based on lessons learned.

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

Then we can separate entirely the code for manipulating symbolic expressions from the code responsible for proving things and simplifying expressions based on an assumption.

How about multiple layers for the symbolic package:

1. Layer 0: Herbrand arithmetic. No simplifications of anything. This just produces new symbolic expressions based on the given arguments. Straightforward factory; operator, arguments type of thing.
2. Layer 1: Very basic simplifications only, such as x+0->x, 1*x->x, x+y->y+x. Integers commutative/associative, etc. All of which are applicable to IEEE arithmetic. Place boolean expressions in canonical form, such as CNF?
3. Layer 2: rational canonical form for real expressions. Valid for real arithmetic but does not necessarily preserve IEEE arithmetic.

Each layer could implement the same interface, SymbolicUniverseIF.

Add: a SymbolicSimplifierIF interface and a TheoremProverIF interface.

So, the following are the items exported by the symbolic module:

• SymbolicUniverseIF
  • methods for creating and manipulating symbolic expressions
  • SymbolicExpressionIF and all kinds of subtypes, operators, and so on
• SymbolicSimplifierIF
  • see the simplifier class currently in the value package
• TheoremProverIF
  • boolean valid(BooleanSymbolicExpressionIF assumption, BooleanSymbolicExpressionIF predicate);

Examples

• Diffusion
  • What does the distribution strategy do if the number of cells is less than the number of procs? Does it necessarily place two consecutive cells on two consecutive procs? If it does not, then how can the ghost cell exchange work? The exchange routine assumes that the neighboring cells will be on neighboring procs. Check this out.
  • Interestingly, the parallel version is not necessarily correct when the number of cells is less than the number of processes. It is possible for there to be a process "gap" between two consecutive cells. But you need at least 5 procs in order to see this. Added Diffusion_5_2_5_Test.java to demonstrate this. The fix: just change the way the neighbor ranks are computed (left/right, upper/lower). These should be computed using the owner function to find out the rank of the process that owns the row next to you, instead of just assuming this will be your rank +/- 1.

Parameters

We need a notion of a parametrized model. So we only have to write a single model laplace (for example), and not laplace_2_2, laplace_2_3, etc.

Should the parameters be dealt with like pre-processor directives (#define N 3)?

A parametrized model should basically be a function which takes some parameter values and returns a ModelIF. It could have a method

ModelIF instantiate(Map<P,V> parameterValues);

or something like that, where the map assigns a value to each parameter. The MiniMP representation might look something like:

parameter int N = 7; /* default value */
parameter bool BLACK;
#ifdef BLACK
...
#endif

To add:

• ParameterIF
  • TypeIF type();
  • String name();
  • int id();
• Parameter
• ParameterExpressionIF
• ParameterExpression

Add methods:

• ModelFactoryIF
  • ParameterIF newParameter(TypeIF type, String name);
    • creates a new parameter with given name
• ModelIF
  • void addParameter(ParameterIF parameter)
    • adds a parameter to this model. Parameters are numbered in the order they are added to model, starting from 0.
  • Collection<ParameterIF> parameters();
    • returns the list of parameters for this model
  • ParameterIF getParameter(int i);
    • returns the i-th parameter for this model.
  • ModelIF instantiate(Map<ParameterIF,Object> parameterValueMap)
    • returns the model obtained by substituting the values for the corresponding parameters. Not every parameter need occur as a key in the map. The resulting model will have parameter set that is the difference between the original parameter set and the parameters occurring as keys the map
  • boolean isParametrized()
    • equivalent to !parameters.isEmpty()
• Expression
  • Expression substitute(Map<ParameterIF,Object> parameterValueMap);
    • each ParameterExpression gets replaced by a LiteralExpression for the value given in the map. If the parameter does not occur in the map, it remains a ParameterExpression

Modify methods:

• complete: needs to determine if model is parameterized