test

[repair.git] / Repair / RepairCompiler / compile.plan

today's todo:

// INITIAL SUPPORT FINISHED - add support for three valued logic 

- create typing system which dynamically types the memory and revists
  portions to double check the validity of claims.

lets talk about the type checker. it is going to based loosely on what
the current implementation (brian's) does. the only difference is that
the initial data structure pointers ('d' in this case) need to be
checked... from then on, only pointers need to be checked. (though this
begs the question whether we will continue to attempt to 

................







short term todo -------------------------------------------------------

- add checks for each pointer dereference (before dereference!) to make
  sure the pointer points to valid memory... this does not provide type
  safety but it does provide memory safety

- add support for three valued logic in the system... i suggest maybe a
  goto mechanism or a exception mechanism... or maybe something a lot
  more clever... anyway, gotta do three valued logic

- start thinking of ways to deal with limiting space consumption (as
  well as measuring it... (add methods to brian's code to dump sizes of
  sets and what not... we want actual sizes... bytes.. perhaps

- at some point it might be a good idea to handle cyclic graphs!!!
  
--------------------
  
  

-- arg... 3 valued logic --------
alright... so it turns out that three valued logic is needed because
doubly linked lists are not 1->1 ... they are infact 1->1/0... which is
not 1->1... and we can not expect the programmer to include guards all
the time .... so maybe's it is!




about typing ***********************************************************
ok... so it turns out that typing is not that easy. first off, there is
a distinction between typing the root types and then tying
pointers. when you start off you can go ahead and type the regions that
are global variables. these regions that are typed use a different
system for testing types. basically when you are typing something and
determining sizes of structures and what not its important not to try to
type data structures as you go along because you may find that it is
impossible getting in an infinite loop... instead you must just look at
the fields and verify that they are in the correct regions. you must do
this because otherwise it is impossible to type things... the claim
might be that given a heap and a set of accesses to that heap with
specific claims as to the types of these accesses, is it possible to
determine whether that access is well typed? it may be better to only
type what you actually need... for instance always do field type checks
... of course the question might be, when do you go ahead and type an
entire structure.

now typing is of course a moot point in a memory-safe, type-safe
language like Java. 

there is another issue of explicit array bounds checks versus allowing
these to be checked by the typemaps. if you have two adjacent arrays
with the same types back to back then an out of bounds check on the
first may not fail in the typemap (unless it goes beyond the 2nd array
and you are lucky even in this case.) explicit array bounds checks may
be in order. 

the issue may boil down to this: what can we guarantee in a system where
we check things at a structure level in some places but at a field level
in other places? can we guarantee anything? if not, perhaps we should
just use the typemaps as valid memory checks at a field level so that we
don't get unexpected crashes at runtime...

in short: this problem seems to be a lot more complicated then what was
perceived initially and the returns seem to be diminishing the more we
think about it. certainly the system now proposed (check root data
structures and any pointers accessed) seems to be inately flawed in some
sense (though i can not put my finger on it :) 

i think my time is better spent working on something else... ?
************************************************************************


#STOPPED#

about typemaps : allow flag to gear level of checks. nothing, bounds,
the types. implement bounds check for now.



can we implement typemaps so that they are fast usually and slow if
something is wrong?

we're interested in space. hit theoretically low without reaching
quadratic time

create optimum benchmark sets... recognize typpical specs and generalize
heuristics to deal with these...




MARTIN's IDEA ************************************************* 7/9/03
use memory/type safe language and check only on reads (when data is
accessed) check consistency properties only when the property needs to
be consistent... only when it needs the property to be true
**********************************************************************

issue: what if you are building the model and you are adding elements to
a relation and the sets that compose those relations don't exist yet?
hmm... maybe the question boils down to a question of whether the items
being added to a relation are implied in the addition... that is if we
have:

R: S->S
condition(a) => <a, f(a)> in R

then if condition(a) => b in S then we never need to check for that
relations (R)'s type... we only need to check if condition(a) => b in S
hold ups (statically). 

if not, in this case the question is whether its better to do
a post exhaustive step or a per addition check ... in the per addition
step we will obviously need to ensure that the sets that compose the
domain and range of a relation are built prior to the rules that add
elements to relations (i'm thinking that its better to do a per addition
check because the post exhaustive step seems just as expensive and
messier!) 

question still remains though: do we need to build the sets prior?
well... of course we do unless we want the worklist to also trigger
rules based upon the additions to the sets of the respective
relations... of course we would only be interested if a particular
relation addition was blocked because of such a check... 

what do we do now? well we don't even properly include required
constraints in the required symbol list... that is being changed right
now ... we'll have to compare this with the older graph

ok... the answer is that the graph changes once we make this change
... i'm checking out if cycles appear... i'm also going to consider the
problem of not having a well defined relation domain/range
(i.e. integers rather than a strictly typed set)

------------------------------------------------------------------------

1. check at compile time how relations are used. if they are used in
   both directions (meaning inverse and otherwise) generate both
   simultaneously so that checks are fast .... otherwise only generate
   one of them that is used... code for generation should automatically
   handle the necessary switches and double-adding... 


new issues - it is not always possible to precalculate (or even
calculate) an offset for a particular field... this would be the case if
a field relied on a particular structure's fields and that fields'
offset relied upon itself or something beyond it in its own
structure... 

compilation plan xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

1. determine preconditions (required sets/relations), post conditions
   (generated sets), and measures of difficult in checking constraints

2. find best ordering of rule building to minimize the cost of space
   and time. 

3. build ordering and generate code.



set traversal xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

1. when accessing set traversal costs assume that sets do not have
   cycles and that set traversal can occur in constant time if necessary.

2. on first run, do a linear space traversal to determine a time bound
   on which the set traversal should finish. from then on use a constant
   space traversal with a dynamic time bound.



accessing ease of relation building xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

1. rank ease of relation building by whether the relation is a field
or a constant time countable function of the fields. 



changing lattices xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

1. examine how relations are built. for instance, if we can guarantee
   that duplicates shouldn't occur, and we might be able to if we use a
   hash just in case.

2. if a relation is only used for counting and we are guaranteed not
   to double count than just keep the count around (saves massive space)



plan of action xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

1. determine rules for generating pre/post conditions and cost measures
   for rule building. 

2. devise an algorithm to schedule these rule building and constraint
   checking mechanisms. 

3. be warned about tight coupling of set building and consistency
   checking. it may be better to decouple them and set up pre/post
   conditions on the consistency checks (per quantifier)

4. test scheduler against file example and compare to hand coded



plan of action revised xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

1. perform topological sort of all rules, TS[nodes]

2. mark sets that need to be built in linear space if
   a. it appears inside a guard expression or inclusion expr
   b. it is marked "build" in the spec (see redundant)
   c. if it appears as the range in a relation that is not 
      statically type safe

3. mark relations that need to be built in linear space if
   a. they appear in constraints and are difficult to build 
   b. a cycle has been found

4. detect singletons and replace with constants and wrap traversals with
   'if-else' checks. upon failure define sets that the quantifier
   appears in as empty and check as usual

5. for all sets that appear in constraints and relations that need to be
   built, sort them topologically by TS and the generate each one in order.

6. pile up set building on top of previous set traversals unless a set
   is marked 'build'. then build it and each traversal dependent on build
   should begin afresh.

7. at each interface point, assess what can be checked and check it. the
   idea is that since we are guaranteeing that everything that needs to
   traversed is traversed if we check whenever we can, what we can then
   we should end up doing a complete check.



hacks xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

1. statically find singleton sets and optimize them out of quantifiers



issues xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

1. domain type problems with relations during fast traversal

   S(node*);
   R(S->S);
   [], true => root in S
   [forall s in S], s.next != null => <s, s.next> in R
   [forall s in S], s.next != null AND s.flag = 1 => s.next in S

   the problem here is that if you have a simple linked list,
   root(1)->element(0) where the parantheses mark the value of .flag
   then the above system will add <root, element> to R but element is
   not in S because flag = 0. In brian's system the relations undergo a
   post process to determine if any elements exist don't exist in the
   domain/range of the relation. 

   the problem appears when the relation is being quickly traversed (via
   pattern matching). now it is possible for a relation to be returned
   that is not truly a match. the solution we have determined at this
   point is to assume that most specs won't have this problem (its
   arguably a problem in the spec!) and to basically do perform these
   two static tests:

   if [forall s in S], s.next != null => <s, s.next> in R
      AND  s.next != null => s.next in S

   then R is safe and no fast traversal should return non-elements,
   regardless of the state of the data structure. If it can not be
   determined whether a relation is type safe, then a linear space
   storage of S must be done so that the relations can be
   existence-checked against the stored set

2. redundancy in sets may result in slowdown

   assume we have a set of file references (set R) which reference files
   (set F). These files can contain a large amount of block
   references (set B). Now assume that we have one file but thousands of
   references to that file. If there a test on the blocks of a file than
   there can be a slow down caused by a constant space traversal of the
   sets that is disproportiate to the gain seen.

   clarification. lets assume that we test that blocks are marked as
   used. if sets R and F and B were generated in linear space than the
   number of checks done to test the constraint on B would be O(B). 

   now assume that we traverse R, F, and B in constant space. Because
   each reference points to the same file and we have no way of knowing
   in constant space whether we are rechecking each file over and over, 
   we will check the constraints on B O(R*B) times. this is much worse
   and represents a jump in the time complexity.

   static analysis of the specs will not be able to determine such a
   problem as a broken data structure is a perfectly viable input to the
   system. therefore it is necessary to have the program be given hints
   about the redundancy of structures. If a structure is highly
   redundant than that structure should be stored in linear space to
   fight the problem of quadratic blow up.

   the hint could be in the form of a keyword addition to the space file
   language. another option is to allow the checker to dynamically
   detect redundancy (how? maybe hash table? maybe sparse linear time
   checks) and change the way its builds sets realtime. for simplicity,
   the spec hint will be used. 

3. how do page accesses translate to incremental model checks?

   TBD.