From: droy Date: Mon, 7 Jul 2003 16:03:55 +0000 (+0000) Subject: blah X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=98152370df2804e762d8ec12dcc5afb4d45c0349;p=repair.git blah --- diff --git a/Repair/RepairCompiler/cdl.tex b/Repair/RepairCompiler/cdl.tex new file mode 100755 index 0000000..a62732b --- /dev/null +++ b/Repair/RepairCompiler/cdl.tex @@ -0,0 +1,50 @@ +Constraint Definition Language +xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx + +constraints ::= constraints constraint | constraint + +constraint ::= optcrash OPENBRACKET quantifiers CLOSEBRACKET COMMA body SEMICOLON + +optcrash ::= CRASH | /* nothing */ + +quantifiers ::= quantifiers COMMA quantifier | quantifier | /* nothing */ + +quantifier ::= FORALL ID:var IN set:set + +set ::= ID:setname + | OPENBRACE listofliterals CLOSEBRACE + +listofliterals ::= listofliterals COMMA literal | literal + +body ::= body AND body + | body OR body + | NOT body + | OPENPAREN body CLOSEPAREN + | predicate + +predicate ::= SIZEOF OPENPAREN setexpr CLOSEPAREN limitedcompare DECIMAL:dec + | ID:var IN setexpr + | ID:var DOT ID:relation compare:compare expr + +setexpr ::= ID:var + | ID:var DOT ID:relation + | ID:var DOTINV ID:relation + +expr ::= ID:var + | OPENPAREN expr CLOSEPAREN + | LITERAL OPENPAREN literal CLOSEPAREN + | expr operator expr + | expr DOT ID:field + | SIZEOF OPENPAREN setexpr CLOSEPAREN + | CAST OPENPAREN ID:type COMMA expr CLOSEPAREN + +operator ::= ADD | SUB | MULT | DIV + +literal ::= TRUE | DECIMAL | STRING | CHAR | ID + +limitedcompare ::= EQUALS | wGT + +compare ::= LT | GT | LE | GE | EQUALS + + + diff --git a/Repair/RepairCompiler/compile.plan b/Repair/RepairCompiler/compile.plan new file mode 100755 index 0000000..075afbb --- /dev/null +++ b/Repair/RepairCompiler/compile.plan @@ -0,0 +1,172 @@ + +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 => 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 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 => 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. + + diff --git a/Repair/RepairCompiler/mdl.tex b/Repair/RepairCompiler/mdl.tex new file mode 100755 index 0000000..165b23a --- /dev/null +++ b/Repair/RepairCompiler/mdl.tex @@ -0,0 +1,44 @@ +Model Definition Language +xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx + +rules ::= rules rule | rule + +rule ::= ruletype OPENBRACKET quantifiers CLOSEBRACKET COMMA guard IMPLIES inclusions SEMICOLON + +ruletype ::= STATIC | DELAY | /*nothing*/ + +quantifiers ::= quantifiers COMMA quantifier | quantifier | /* nothing */ + +quantifier ::= FORALL ID:var IN ID:set + | FORALL LT ID:r1 COMMA ID:r2 GT IN ID:relation + | FOR ID:var EQUALS expr:lower TO expr:upper + +guard ::= guard AND guard + | guard OR guard + | NOT guard + | expr EQUALS expr + | expr LT expr + | TRUE + | OPENPAREN guard CLOSEPAREN + | expr IN ID:set + | LT expr:r1 COMMA expr:r2 GT IN ID:relation + | ISVALID OPENPAREN expr CLOSEPAREN + | ISVALID OPENPAREN expr COMMA ID:var CLOSEPAREN + +inclusion ::= expr IN ID:set + | LT expr:r1 COMMA expr:r2 GT IN ID:relation + + + +expr ::= ID:var + | OPENPAREN expr CLOSEPAREN + | LITERAL OPENPAREN literal CLOSEPAREN + | expr operator expr + | expr DOT ID:field + | expr DOT ID:field OPENBRACKET expr:index CLOSEBRACKET + | CAST OPENPAREN ID:type COMMA expr CLOSEPAREN + +operator ::= ADD | SUB | MULT | DIV + +literal ::= TRUE | DECIMAL | STRING | CHAR | ID +