Fri 25 Jun 2021 01:55 - 02:00 at PLDI-B - Talks 4B: Concurrency, Compilation, and Debugging
Reducing a failure-inducing input to a smaller one is challenging
for input with internal dependencies because most sub-inputs are invalid.
Kalhauge and Palsberg made progress on this problem by mapping the task to
a reduction problem for dependency graphs that avoids invalid inputs entirely.
Their tool J-Reduce efficiently reduces Java bytecode to 24 percent of
its original size, which made it the most effective tool until now.
However, the output from their tool is often too large to be helpful in
a bug report.
In this paper, we show that more fine-grained modeling of dependencies leads to much more reduction.
Specifically, we use propositional logic for specifying dependencies and
we show how this works for Java bytecode.
Once we have a propositional formula that specifies all valid sub-inputs,
we run an algorithm that finds a small, valid, failure-inducing input.
Our algorithm interleaves runs of the buggy program and
calls to a procedure that finds a minimal satisfying assignment.
Our experiments show that we can reduce Java bytecode to 4.6 percent of its
original size, which is 5.3 times better than the 24.3 percent achieved by J-Reduce.
The much smaller output is more suitable for bug reports.
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 |