advertisement

popl05

75 %
25 %
advertisement
Information about popl05
Education

Published on June 20, 2007

Author: Aric85

Source: authorstream.com

advertisement

Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules:  Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules Sorin Lerner* Todd Millstein** Erika Rice* Craig Chambers* * University of Washington ** UCLA [graduating this year!] A traditional compiler:  A traditional compiler Parser Code Gen Compiler Opt Opt Opt Using a domain specific language:  Using a domain specific language Parser Code Gen Compiler DSL Opt DSL Opt DSL Opt Using a domain specific language:  Using a domain specific language Parser Code Gen Compiler DSL Execution engine DSL Opt DSL Opt DSL Opt Checking correctness automatically:  Checking correctness automatically Parser Code Gen Compiler DSL Execution engine DSL Opt DSL Opt DSL Opt Checking correctness automatically:  Checking correctness automatically Parser Code Gen Compiler DSL Execution engine Checking correctness automatically:  Checking correctness automatically Checker Checking correctness automatically:  DSL Opt Checking correctness automatically Checker Checking correctness automatically:  DSL Opt Checking correctness automatically Checking correctness automatically:  Checking correctness automatically VCGen Verification Condition (VC) Checker DSL Opt Checking correctness automatically:  Checking correctness automatically VCGen DSL Opt Checker Verification Condition (VC) Checking correctness automatically:  Checking correctness automatically Checker Lemma: VC implies correctness VC Cobalt:  Cobalt The Cobalt DSL is an instantiation of this architecture An opt written in Cobalt is a rewrite rule triggered by a declarative global condition over the CFG Expressed and automatically proved the correctness of a variety of intraprocedural optimizations, including: const prop and folding, branch folding, CSE, PRE, DAE, partial DAE [PLDI 03] In this talk: the Rhodium DSL:  In this talk: the Rhodium DSL Increased expressiveness New model for expressing opts: local propagation rules with explicit dataflow facts Heap summaries Infinite analysis domains Flow-sensitive and -insensitive Intraprocedural and interprocedural Some Rhodium opts not expressible in Cobalt: Arithmetic invariant detection, integer range analysis, loop-induction-variable strength reduction, Andersen's may-point-to analysis with allocation-site summaries Outline:  Outline Overview Rhodium by example Checking correctness automatically Future work, related work and conclusion MustPointTo analysis:  MustPointTo analysis c := a a := andamp;b *c := d MustPointTo info in Rhodium:  MustPointTo info in Rhodium c := a a := andamp;b *c := d MustPointTo info in Rhodium:  MustPointTo info in Rhodium c := a a := andamp;b *c := d c := a a := andamp;b *c := d MustPointTo info in Rhodium:  MustPointTo info in Rhodium define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d Propagating facts:  Propagating facts c := a a := andamp;b *c := d define fact mustPointTo(X:Var,Y:Var) Propagating facts:  if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Propagating facts define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d mustPointTo (a, b) mustPointTo (c, d) if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out a := andamp;b mustPointTo (a, b) Propagating facts:  if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Propagating facts define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d Propagating facts:  if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Propagating facts if mustPointTo(X,Y)@in Æ currStmt = [Z := andamp;W] Æ X  Z then mustPointTo(X,Y)@out define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d mustPointTo (a, b) mustPointTo (c, d) mustPointTo (c, d) if mustPointTo(X,Y)@in Æ currStmt = [Z := andamp;W] Æ X  Z then mustPointTo(X,Y)@out a := andamp;b mustPointTo (c, d) mustPointTo (c, d) Propagating facts:  if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Propagating facts if mustPointTo(X,Y)@in Æ currStmt = [Z := andamp;W] Æ X  Z then mustPointTo(X,Y)@out define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d mustPointTo (a, b) mustPointTo (c, d) mustPointTo (a, b) mustPointTo (c, b) if mustPointTo(X,Y)@in Æ currStmt = [Z := X] then mustPointTo(Z,Y)@out c := a mustPointTo (a, b) mustPointTo (c, b) Propagating facts:  if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Propagating facts if mustPointTo(X,Y)@in Æ currStmt = [Z := andamp;W] Æ X  Z then mustPointTo(X,Y)@out define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d if mustPointTo(X,Y)@in Æ currStmt = [Z := X] then mustPointTo(Z,Y)@out Transformations:  if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Transformations if mustPointTo(X,Y)@in Æ currStmt = [Z := andamp;W] Æ X  Z then mustPointTo(X,Y)@out define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d Transformations:  *c := d Transformations define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d mustPointTo (a, b) mustPointTo (c, b) if mustPointTo(X,Y)@in Æ currStmt = [*X := Z] then transform to [Y := Z] mustPointTo (c, b) b := d Semantics of a Rhodium opt:  Semantics of a Rhodium opt Run all the propagations rules using optimistic iterative analysis starting with complete set of facts until the best fixed point is reached Then run all transformation rules For better precision, combine analyses and transformations using our previous composition framework [POPL 02] More in Rhodium (see paper for details):  More in Rhodium (see paper for details) Mixing facts Heap summaries MayPointTo analysis via MustNotPointTo Infinite domains Flow-sensitive and -insensitive Intraprocedural and interprocedural Outline:  Outline Overview Rhodium by example Checking correctness automatically Future work, related work and conclusion Rhodium correctness checker:  Rhodium correctness checker Automatic theorem prover Checker opt- independent VCGen VC Lemma: VC ) correctness Rhodium optimization Rhodium correctness checker:  Rhodium correctness checker Automatic theorem prover Checker opt- independent VCGen Rhodium optimization define fact … if … then transform … if … then … VC Lemma: VC ) correctness Rhodium correctness checker:  Rhodium correctness checker Automatic theorem prover Rhodium optimization Checker opt- independent Lemma: VC ) correctness define fact … if … then transform … if … then … VCGen Local VC Local VC Lemma: Local VCs ) correctness Local correctness of prop. rules:  Local correctness of prop. rules define fact mustPointTo(X:Var,Y:Var) Z := X currStmt = [Z := X] then mustPointTo(Z,Y)@out if mustPointTo(X,Y)@in Æ Local correctness of prop. rules:  define fact mustPointTo(X:Var,Y:Var) Local correctness of prop. rules currStmt = [Z := X] then mustPointTo(Z,Y)@out Z := X Z := X in out Local VC sent to ATP: if mustPointTo(X,Y)@in Æ Local correctness of trans. rules:  Local correctness of trans. rules define fact mustPointTo(X:Var,Y:Var) if mustPointTo(X,Y)@in Æ currStmt = [*X := Z] then transform to [Y := Z] with meaning « X == andamp;Y ¬ then if « X == andamp;Y ¬ (in) Æ *X := Z in out Y := Z in out *X := Z *X := Z out ? Y := Z out Y := Z Local VC sent to ATP: More on correctness (see paper for details):  More on correctness (see paper for details) Heap summaries Separating profitability from correctness Theorem stating soundness of the framework for creating interprocedural and flow-insensitive analyses Outline:  Outline Overview Rhodium by example Checking correctness automatically Future work, related work and conclusion Current and future work:  Current and future work Backward optimizations Infer rules from just the dataflow fact declarations and their meanings Debugging Efficient execution engine Some related work:  Some related work Proving correctness by hand Abstract interpretation [Cousot and Cousot 77, 79] Partial equivalence relations [Benton 04] Temporal logic [Lacey et al. 02] Proving correctness with interactive theorem prover Using Coq proof assistant [Cachera et al. 04] Testing correctness one compilation at a time Translation validation [Pnueli et al. 98, Necula 00] Credible compilation [Rinard 99] Execution engines Incremental execution of transformations [Sittampalam et al. 04] Running opts specified with temporal logic [Steffen 91] Conclusion:  Conclusion Local rules in Rhodium are more expressive than Cobalt’s global condition The correctness checker found subtle bugs in our Rhodium opts Good step towards pushing more of the burden of writing compilers on to the computer

Add a comment

Related presentations

Related pages

POPL 2005 - Computer Science Department at Princeton ...

Welcome to POPL 2005. POPL is the ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages. POPL 2005 Invited Speakers. Pat Hanrahan (Stanford ...
Read more

www2.informatik.uni-freiburg.de

www2.informatik.uni-freiburg.de
Read more

Transition Predicate Abstraction and Fair Termination

Transition Predicate Abstraction and Fair Termination∗ Andreas Podelski Andrey Rybalchenko Max-Planck-Institut fu¨r Informatik Saarbru¨cken, Germany
Read more

CiteULike: bec's popl05 [8 articles]

Recent papers added to bec's library classified by the tag popl05. You can also see everyone's popl05.
Read more

Precise Interprocedural Analysis using Random Interpretation

Published in the Proceedings of the Principles of Programming Languages (POPL), 2005 Precise Interprocedural Analysis using Random Interpretation
Read more

A Semantics for Procedure Local Heaps and its Abstractions

A Semantics for Procedure Local Heaps and its Abstractions Noam Rinetzky∗ Jorg Bauer¨ † Thomas Reps‡ Mooly Sagiv‡ Reinhard Wilhelm Tel Aviv Univ ...
Read more

The Java Memory Model - Sarita Adve's Group

The Java Memory Model ∗ Jeremy Manson and William Pugh Department of Computer Science University of Maryland, College Park College Park, MD {jmanson ...
Read more

www.verisoft.de

@InProceedings{Podelski:POPL05-132, author = "Andreas Podelski and Andrey Rybalchenko", title = "Transition Predicate Abstraction and Fair ...
Read more

Dynamic Partial-Order Reduction for Model Checking Software

Dynamic Partial-Order Reduction for Model Checking Software Cormac Flanagan University of California at Santa Cruz cormac@cs.ucsc.edu Patrice Godefroid
Read more

A Probabilistic Language based upon Sampling Functions

A Probabilistic Language based upon Sampling Functions Sungwoo Park Frank Pfenning Computer Science Department Carnegie Mellon University {gla,fp}@cs.cmu.com
Read more