fse_talk_v6_2

Views:
 
Category: Entertainment
     
 

Presentation Description

No description available.

Comments

Presentation Transcript

Synthesizing Data-Structure Manipulations from Storyboards:

Synthesizing Data-Structure Manipulations from Storyboards Rishabh Singh and Armando Solar- Lezama

Programming with Code:

Programming with Code dllDelete (Node v) { n = v.next ; p = v.prev ; p.next = n; n.prev = p; }

Heap Structure:

Heap Structure b x next prev a next prev next prev next prev b next prev a next prev next prev v x n

Bridging the semantic gap:

Bridging the semantic gap b x next prev a next prev b next prev a n dllDelete (Node v) { n = v.next ; p = v.prev ; p.next = n; n.prev = p; } WHAT? HOW? Program Synthesis

Programming with Scenarios:

Programming with Scenarios A scenario is more powerful than an example each scenario represents an infinite set of examples It is also less powerful Partial specification, ambiguous for … b next prev a b x next prev a next prev n b x next prev a next prev n next prev next prev next prev next prev

Synthesis with Scenarios:

Synthesis with Scenarios Trick: combine many simple specs to constrain behavior Abstract Scenarios Structural Info Concrete Scenarios Synthesizer Storyboard Framework Correct Code Storyboard

Linked List Reversal:

Linked List Reversal next f e mid a b e’ f’ mid’ a b head next next next head

Scenarios for LL-reversal:

Scenarios for LL-reversal a b next head a b head next a head a head head head f e mid a b head next next e’ f’ mid’ a b next next head

Inductive insights with fold/unfold:

Inductive insights with fold/unfold f e mid f’ e’ mid x’ next x’ x’ = f x’= e x’ = f e = e’ Unfold:

Inductive insights with fold/unfold:

Inductive insights with fold/unfold f e mid f’ e’ mid x’ next x’ x’ = f x’= e x’ = f e = e’ Unfold: f e mid f’ e’ mid x’ next x’ x’ = f x’= e x’ = f e = e’ F old:

Fold/Unfold:

Fold/Unfold Can’t reason summary nodes without unfold Additional algorithmic insights f b stree stuff y stuff’ y stuff’ f’ b’ stree ’ stuff y f’ b’ stree ’ val == y.val f=b=y val < y.val f=y b=b’ val > y.val f=y b=b’

Text representation of Scenario:

Text representation of Scenario f e mid a b head next next e’ f’ mid’ a b next next head

Text Representation of Unfold:

Text Representation of Unfold f e mid f’ e’ mid x’ next x’ x’ = f x’= e x’ = f e = e’ Unfold:

Loop Sketch:

void llReverse( Node head) { ?? /*1*/ while ( ?? /*p*/ ) { ?? /*2*/ } ?? /*3*/ } Loop Sketch

Loop Sketch:

void llReverse( Node head) { cstmt * /*1*/ while ( cond /*p*/ ) { cstmt * /*2*/ } cstmt * /*3*/ } Loop Sketch

Conditional Statements :

Conditional Statements cstmt : if (COND) then STMT var (. ptr ? ) op var (. ptr ? ) | null var (. ptr ? ) = var (. ptr ? ) unfold/fold var

Demo:

Demo

How it Works:

How it Works

Data flow equations:

Data flow equations s in s 1 s 3 s 2 s out f 1 f 2 f 3 f p true false

Synthesis vs. Verification:

Synthesis vs. Verification Verification known : f, s in unknown : s out Synthesis known : s in, s out unknown : f

Synthesis Challenges:

Synthesis Challenges Find values for Can’t give to solver w e are interested in LFP s i are sets of shapes Key: a void set reasoning

1 : Loop unrolling:

1 : Loop unrolling f 1 f 2 f 3 f p true false f 1 f 3 f p false p 0 f 1 f 3 f p false f p f 3 true p 1 f 1 f p f 3 true f 3 f p false . . . k iters p k

Slide 23:

f 1 f 3 f p false p 0 f 1 f 3 f p false f p f 3 true p 1 f 1 f p f 3 true f 3 f p false . . . p k

2: Non-deterministic Functions:

2: Non-deterministic Functions f Parameterize the choice j j

Solving the constraint:

Solving the constraint Rewrite as subset constraints:

Quantifier alternation constraint:

Quantifier alternation constraint

Quantifier alternation constraint:

Quantifier alternation constraint Sketch solver

Experiments:

Experiments

Data Structure Manipulations:

Linked lists : insert, delete, reverse, swap-first-last Doubly Linked lists : reverse, traverse Binary Search Trees : search, min, rotate, insert, delete User-defined : AIG (And-Inverter-Graph) insertion Complex data structures : Red Black Tree Insertion Data Structure Manipulations

Red Black Tree Insertion:

Red Black Tree Insertion 4 cases to fix red black tree invariant after insertion

Red Black Tree Insertion:

Red Black Tree Insertion fixRBTree (Node root, Node x){ w hile(x.p != null && x.p.p != null){ y = x.p; z = x.p.p ; if(cond1) //case1 elsif (cond2) //case2 elsif (cond3) //case3 elsif (cond4) //case4 else break; x = z; } color[root] = black; }

And-Inverter Graph (AIG):

And-Inverter Graph (AIG) DAG Encodes logical functionality of circuits Two-input AND gates and inverters Minimize memory usage f : pointer to its father node m: pointer to its mother node nf : pointer to father’s next child nm: pointer to mother’s next child c h : pointer to its first child f m nf nm ch x

And-Inverter Graph (AIG):

And-Inverter Graph (AIG) x

And-Inverter Graph (AIG):

And-Inverter Graph (AIG) x ch

And-Inverter Graph (AIG):

And-Inverter Graph (AIG) x ch f nf m nm

AIG Insertion:

AIG Insertion z F x 1 x 2 x n ch f/m f/m f/m nf /nm nf /nm M y n y 2 y 1 ch nf /nm nf /nm f/m f/m f/m z F x 1 x 2 x n ch f/m f/m f/m nf /nm nf /nm M y n y 2 y 1 ch nf /nm nf /nm f/m f/m f/m nf /nm nf /nm f m

Case studies - I:

Case studies - I Manipulation #Clauses Memory # Scen Time ll -insertion 1.99M 0.75G 4 2m9s ll -deletion 1.88M 0.54G 4 1m48s ll -reverse 1.30M 0.35G 4 1m49s ll -find-last 1.02M 0.29G 4 0m56s ll -swap-first-last 1.08M 0.31G 4 4m18s dll -traversal 1.72M 0.88G 4 1m58s dll -reversal 2.04M 0.49G 4 3m47s

Case studies - II:

Case studies - II Manipulation #Clauses Memory # Scen Time bst -search(contains) 0.62M 0.37G 1 1m02s bst -search 0.77M 0.45G 1 6m07s bst -find-min 0.63M 0.45G 1 0m58s bst -find-max 0.57M 0.18G 1 0m23s bst -left-rotate 1.41M 0.50G 3 3m18s bst -right-rotate 1.47M 0.43G 3 3m15s bst -insertion 1.04M 0.46G 3 1m52s bst -deletion 0.63M 0.62G 6 3m13s Manipulation #Clauses Memory # Scen Time aig -insertion 0.17M 0.31G 4 1m04s

BST Deletion:

BST Deletion Simple storyboard was under-constrained Two additional concrete instances were required Synergy b/w abstract and concrete scenarios s ix concrete scenarios do not scale

Research Questions:

Research Questions Interactivity Debugging storyboards Corner cases Automated fuzzing of scenarios Encoding Symmetry reduction Concurrent data structures

Conclusion:

Conclusion Heap descriptions for manipulations Abstraction is necessary Constraints are a powerful basis for synthesis

Thanks!:

Thanks! Questions/Comments [email protected] http://www.storyboardprogramming.com

Backup Slides:

Backup Slides

Storyboard Programming:

Storyboard Programming

Challenges:

Challenges

1. Defining semantics of pictures:

1. Defining semantics of pictures

Slide 47:

a head b Locations : a, b, null Variables : head Ptr Fields : next VarMap : Var → Loc (head → a) Heap : Loc × Ptr → Loc ( a.next → b, b.next → null) next next

Summary Locations:

Summary Locations a b head f e mid Attachment points: f, e f e mid x x f’ e’ mid { f=x, e=x } { f=x, e=e’ } unfold Unfold: (f, (f → x, e → x), {true}) ( f, (f → x, e → e’), { x.next → f’ })

State constraints:

State constraints Environment { variables : head, temp1, temp2, temp3 locations : a, f, e, b, null summary: {mid( f,e )} selectors : next unfold : (f, (f → x, e → x), (true)) ( f, (f → x, e → e’), (x.next → f’ )) } state s2 { stack : head → b heap : a.next → null, f.next → a, b.next → e } a b head f e mid

2. Modeling the synthesis problem into constraints:

2. Modeling the synthesis problem into constraints

Verification:

Verification void llReverse( Node head) { Node temp1 = null , temp2 = null , temp3 = null ; temp1 = head; while (temp1 != null ) { // unfold temp1; head = temp1; temp1 = temp1.next; head.next = head; head.next = temp3; temp3 = head; // fold temp3; } }

Slide 52:

void llReverse(Node head){ Node temp1 = null, temp2 =null, temp3 = null; temp1 = head; while (temp1 != null){ // unfold temp1; head = temp1; temp1 = temp1.next; head.next = temp3; temp3 = head; // fold temp3; } } s in s 1 s 3 s 2 s out f 1 f 2 f 3 f p true false

Slide 53:

void llReverse(Node head){ Node temp1 = null, temp2 =null, temp3 = null; temp1 = head; while ( temp1 != null ){ // unfold temp1; head = temp1; temp1 = temp1.next; head.next = temp3; temp3 = head; // fold temp3; } } s in s 1 s 3 s 2 s out f 1 f 2 f 3 f p true false f 1 f 2 f p

Slide 54:

void llReverse(Node head){ Node temp1 = null, temp2 =null, temp3 = null; temp1 = head; while ( temp1 != null ){ // unfold temp1; head = temp1; temp1 = temp1.next; head.next = temp3; temp3 = head; // fold temp3; } } s in s 1 s 3 s 2 s out f 1 f 2 f 3 f p true false f 1 f 2 f p s in s 1 s 2 s 3 s out

Transfer function:

unfold temp1; head = temp1; temp1 = temp1.next; head.next = temp3; temp3 = head; fold temp3; b h f e mid t1 t3 a Transfer function f 2

Slide 56:

s in s 1 s 3 s 2 s out f 1 f 2 f 3 f p true false a b h f e mid b h a t1 t3 f e mid’

Finitize function choices:

Finitize function choices f 1 f 11 f 12 f 13 f 14 cstmt 1 cstmt 2 cstmt 3 cstmt 4 cstmt n . . . Parameterize the function choice f 11 (c 11 ) c 11 =

Conditional Statements :

Conditional Statements cstmt : if (COND) then STMT var (. ptr ? ) op var (. ptr ? ) | null temp1 == temp2 var (. ptr ? ) = var (. ptr ? ) temp1 = temp1.next unfold/fold var unfold temp1

Solving:

Solving s i : sets of states Hard to solve Two reasons Loops Unfold

Termination Constraint:

Termination Constraint All reachable states can reach return location Does not guarantee termination in general Guarantee termination for special class single pass algorithms

Fold/Unfold:

Fold/Unfold These rules are part of the specification without them the scenarios are too imprecise They can also serve to communicate insights b x next prev a next prev next prev b next prev a next prev v lleft lright lleft lright

Programming with Scenarios:

Programming with Scenarios Each scenario is a partial specification that’s why they can be simple Completeness vs. complexity tradeoff irrespective of format complete specs are more complex Trick: combine many simple specs in different formalisms to fully constrain the behavior

authorStream Live Help