Changes between Version 20 and Version 21 of Things To Do


Ignore:
Timestamp:
05/18/10 09:08:47 (16 years ago)
Author:
Stephen Siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Things To Do

    v20 v21  
    1616== General To-Do Items ==
    1717
    18  * change names of MiniMP to TASS throughout project
    19    * 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.
    2018 * add good Javadocs for all public methods, classes, and packages
    2119 * achieve much better statement and branch coverage in JUnit tests
    22  * create separate test tree which mirrors the source tree but contains only JUnit tests
    2320
    2421== Symbolic Module ==
    2522
    26 Consider re-designing the symbolic module based on lessons learned.
    27 
    28 First, is the assumption argument necessary?   Is it ever used for anything?  How about removing it?
    29 
    30 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.
    31 
    32 How about multiple layers for the symbolic package:
    33 
    34  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.
    35  1.  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?
    36  1.  Layer 2: rational canonical form for real expressions.  Valid for real arithmetic but does not necessarily preserve IEEE arithmetic.
    37 
    38 Each layer could implement the same interface, SymbolicUniverseIF. 
    39 
    40 Add: a SymbolicSimplifierIF interface and a TheoremProverIF interface.
    41 
    42 So, the following are the items exported by the symbolic module:
    43 
    44  * {{{SymbolicUniverseIF}}}
    45    * methods for creating and manipulating symbolic expressions
    46    * {{{SymbolicExpressionIF}}} and all kinds of subtypes, operators, and so on
    47  * {{{SymbolicSimplifierIF}}}
    48    * see the simplifier class currently in the value package
    49  * {{{TheoremProverIF}}}
    50    * {{{boolean valid(BooleanSymbolicExpressionIF assumption, BooleanSymbolicExpressionIF predicate);}}}
    51 
    52 Other simplifications to symbolic module:
    53 
    54   * get rid of >, >=.  Just use <,<=.
    55   * get rid of NEQ?  Just use NOT(EQUAL).  Actually, NEQ might be useful if we want a normal form that pushes all "not"s inward.
    56 
    57 Additional features:
    58 
    59  * valid methods should return one of three values: YES, NO, or MAYBE
    60  * write a {{{BigRational}}} class using Java's {{{BigInteger}}} class.  Use it for all numbers.  It will support infinite precision rational numbers.  A rational number is stored as a numerator and denominator which are relatively prime.   Note {{{BigInteger}}} has a gcd method so reducing to relatively prime form should be a no-brainer.   The denominator must be positive.   Now two rationals are equal iff the numerators and denominators are.  Use a Flyweight pattern.   Support +,-,*,/,floor,ceil,<,<=,compare,... and any other operation needed.
     23Is the assumption argument necessary?   Is it ever used for anything?  How about removing it?
    6124
    6225Check out other automated theorem provers:
    … …  
    6932== Examples ==
    7033
    71  * Diffusion
    72     * 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.
    73     * 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.
    74 
    7534== Parameters ==
    7635
    77 I added support for parameters by simply giving the user the ability to specify a concrete value for any input variable in the initial state. At the command line, this is done by
    78 {{{
    79 -inputX=V
    80 }}}
    81 where X is the name of the variable and V its value. In a {{{RunConfiguration}}}, this is done using the method {{{setInput(String,Object)}}}. Now we don't need multiple versions of a single model which just differ by some bounds. Instead, just make the bound an input. I have applied this to several of the examples
    82 .
     36
    8337== Library Functions ==
    8438
    … …  
    8842
    8943Note:  {{{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}}}
     44
     45
     46Some libraries add state: shared state and process global state.  How do manage this?