Incremental Whole-Program Analysis in Datalog with Lattices
Fri 25 Jun 2021 01:50 - 01:55 at PLDI-B - Talks 4B: Concurrency, Compilation, and Debugging
Incremental static analyses provide up-to-date analysis results in time proportional to the size of a code change, not the entire code base. This promises fast feedback to programmers in IDEs and when checking in commits. However, existing incremental analysis frameworks fail to deliver on this promise for whole-program lattice-based data-flow analyses. In particular, prior Datalog-based frameworks yield good incremental performance only for intra-procedural analyses.
In this paper, we first present a methodology to empirically test if a computation is amenable to incrementalization. Using this methodology, we find that
incremental whole-program analysis may be possible. Second, we present a new incremental Datalog solver called LADDDER to eliminate the shortcomings of prior Datalog-based analysis frameworks. Our Datalog solver uses a non-standard aggregation semantics which allows us to loosen monotonicity requirements on analyses and to improve the performance of lattice aggregators considerably. Our evaluation on real-world Java code confirms that LADDDER provides up-to-date points-to, constant propagation, and interval information in milliseconds.
Thu 24 JunDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 14:05 | |||
13:30 5mTalk | Mirror: Making Lock-Free Data Structures Persistent PLDI DOI | ||
13:35 5mTalk | Fluid: A Framework for Approximate Concurrency via Controlled Dependency Relaxation PLDI Huaipan Jiang Pennsylvania State University, Haibo Zhang Pennsylvania State University, Xulong Tang University of Pittsburgh, Vineetha Govindaraj Pennsylvania State University, Jack Sampson Pennsylvania State University, Mahmut Taylan Kandemir Pennsylvania State University, Danfeng Zhang Pennsylvania State University DOI | ||
13:40 5mTalk | Frequent Background Polling on a Shared Thread, using Light-Weight Compiler Interrupts PLDI Nilanjana Basu University of Illinois at Chicago, Claudio Montanari University of Illinois at Chicago, Jakob Eriksson University of Illinois at Chicago DOI | ||
13:45 5mTalk | Alive2: Bounded Translation Validation for LLVM PLDI Nuno P. Lopes Microsoft Research, Juneyoung Lee Seoul National University, Chung-Kil Hur Seoul National University, Zhengyang Liu University of Utah, John Regehr University of Utah DOI Pre-print | ||
13:50 5mTalk | Incremental Whole-Program Analysis in Datalog with Lattices PLDI Tamás Szabó JGU Mainz; Workday, Sebastian Erdweg JGU Mainz, Gábor Bergmann Budapest University of Technology and Economics; IncQuery Labs DOI | ||
13:55 5mTalk | Logical Bytecode Reduction PLDI Christian Gram Kalhauge University of California at Los Angeles; Technical University of Denmark, Jens Palsberg University of California at Los Angeles DOI | ||
14:00 5mTalk | RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types PLDI Michael Sammler MPI-SWS, Rodolphe Lepigre MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Kayvan Memarian University of Cambridge, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS DOI |
Fri 25 JunDisplayed time zone: Eastern Time (US & Canada) change
01:30 - 02:05 | |||
01:30 5mTalk | Mirror: Making Lock-Free Data Structures Persistent PLDI DOI | ||
01:35 5mTalk | Fluid: A Framework for Approximate Concurrency via Controlled Dependency Relaxation PLDI Huaipan Jiang Pennsylvania State University, Haibo Zhang Pennsylvania State University, Xulong Tang University of Pittsburgh, Vineetha Govindaraj Pennsylvania State University, Jack Sampson Pennsylvania State University, Mahmut Taylan Kandemir Pennsylvania State University, Danfeng Zhang Pennsylvania State University DOI | ||
01:40 5mTalk | Frequent Background Polling on a Shared Thread, using Light-Weight Compiler Interrupts PLDI Nilanjana Basu University of Illinois at Chicago, Claudio Montanari University of Illinois at Chicago, Jakob Eriksson University of Illinois at Chicago DOI | ||
01:45 5mTalk | Alive2: Bounded Translation Validation for LLVM PLDI Nuno P. Lopes Microsoft Research, Juneyoung Lee Seoul National University, Chung-Kil Hur Seoul National University, Zhengyang Liu University of Utah, John Regehr University of Utah DOI Pre-print | ||
01:50 5mTalk | Incremental Whole-Program Analysis in Datalog with Lattices PLDI Tamás Szabó JGU Mainz; Workday, Sebastian Erdweg JGU Mainz, Gábor Bergmann Budapest University of Technology and Economics; IncQuery Labs DOI | ||
01:55 5mTalk | Logical Bytecode Reduction PLDI Christian Gram Kalhauge University of California at Los Angeles; Technical University of Denmark, Jens Palsberg University of California at Los Angeles DOI | ||
02:00 5mTalk | RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types PLDI Michael Sammler MPI-SWS, Rodolphe Lepigre MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Kayvan Memarian University of Cambridge, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS DOI |