CIS673 Sketch Presentation
Transcript: Validation time constant among iterations, sharp increase towards the end all but two under 25 iterations Richer holes built on top of ??: regular expressions: {x | y} = z {+ | -} {1 | 2 | 3}; loop constructs: repeat(??) { ... } generator functions: ... {return ??;} solver: MiniSAT CIS673@UPenn - Dec 11, 2012 Boolean formulas by unwinding loops and recursions, then converting to predicated code log2_varloop vs log2: 8 loop iterations instead of 6 References A.V. tries to find an input x' such that Time Outs bit[W] logcount (bit[W] in) implements countBits { bit[W] tmp=in; int cnt=0; repeat(??) { bit[W] m = ??; tmp=(tmp & m) + (tmp>>?? & m); assert cnt++ < 5; } return tmp; } Counter Example Guided Inductive Synthesis underlying randomness: "bad" set of counterexamples slows the synthesizer down significantly Memory Consumption CEGIS There exists a small set E of representative inputs such that : Yannis Mantzouratos I.S. tries to find a control c such that SKETCH is much more intuitive to the end user Detailed Statistics: merge_sort Decidable, but between NP and PSPACE five runs per experiment, medians presented BUT reasonable times only for low (toy) bounds QBF Translation Sketch S: a partial program Introduction log2_varloop timed out during that transition point Resolution Time ... because of that last iteration again! AMD Athlon X3 455 at 3.3 GHz with 1.5MB of L2 cache and 16GB of memory log2, log2_varloop: logarithm of 32 bit integer n in logn operations. SKETCH resolves two masks and a shift amount in a loop, as well as a loop count. logcount: number of set bits in 16 bit vector n in logn operations. merge_sort: 3 bit integers, recursion depth of 3. SKETCH decides from which sub-array we should choose an element during the merge operation. list_reverse: SKETCH synthesizes two loop counts (bounded by 3 and 5), two regular expressions within each of the loops, and a while loop conditional. Bounded Observation Hypothesis karatsuba_harder vs karatsuba: integer holes and inputs 5 bits long instead of 2 Most time consumed in synthesis Results Benchmark Suite iterations are not proportional to the number of control bits 16 sketches involving: bit manipulations (compress, log2, log2_varloop, logcount, morton, parity), integer manipulations (karatsuba, karatsuba_harder, table_based_addition, xpose), data structures (enqueue, list_reverse, set_test), high level decisions (merge_sort, partition, pollard) Larger counterexamples, bugs triggered later, more difficult SAT clauses Runs 3 and 4 died during transition All but two under 250MB, all under 500MB Int: integer size (bits), In: total input bits, Ctrl: total control bits, Iter: iterations, Synth: synthesis time (seconds), Valid: validation time (seconds), RAM in megabytes. CEGIS figure reproduced from [1] Synthesis time displays a "phase transition" void reverseSK(ref list l){ node tmp1 = null; node tmp2 = null; int t=??; assert t<3; repeat(t){ {| (tmp1 | tmp2 | l.head)(.next)? |} = {| (tmp1 | tmp2 | l.head)(.next)? |}; } while({| (tmp1 | tmp2 | l.head)(.next)? (== | !=) null |}){ int q = ??; assert q < 5; repeat(q){ {| (tmp1 | tmp2 | l.head)(.next)? |} = {| (tmp1 | tmp2 | l.head)(.next)? |}; } } } In Detail Sample Sketch Detailed Statistics: logcount Validation time dominates synthesis by orders of magnitude Unexpected: Synthesis times increase sharply Elementary integer hole: ?? In my opinion, still a long way to use it in real life Detailed Statistics: log2, log2_varloop CEGIS - Bounded Observation Hypothesis time out: 1 hour; optimization level 6 The Sketches Configuration Expected: Validation times increase, but kindly SKETCH defines correctness only in terms of harness Increasing Test Bounds Two SAT solvers in a "generate/validate" loop If S is equivalent to P on E, then S is equivalent to P on all inputs The Tool loop unrolling: 8; recursion depth: 5; integer size: 5 bits Synthesizer: complete S to be equivalent to P on all inputs For control input c and original input x: karatsuba_harder and log2_varloop consistently timed out, logcount 2 out of 5 Symbolic Holes Example: list_reverse Specification P: a reference implementation performed well in most experiments Software Synthesis with SKETCH Conclusions Intuition behind manual testing, checking common and few corner cases
Prezi Present
Prezi Video
Prezi Design
