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:305m Talk | Mirror: Making Lock-Free Data Structures Persistent PLDIDOI | ||
| 13:355m Talk | 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 UniversityDOI | ||
| 13:405m Talk | 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 ChicagoDOI | ||
| 13:455m Talk | 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 UtahDOI Pre-print | ||
| 13:505m Talk | 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 LabsDOI | ||
| 13:555m Talk | Logical Bytecode Reduction PLDI Christian Gram Kalhauge University of California at Los Angeles; Technical University of Denmark, Jens Palsberg University of California at Los AngelesDOI | ||
| 14:005m Talk | 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-SWSDOI | ||
Fri 25 JunDisplayed time zone: Eastern Time (US & Canada) change
| 01:30 - 02:05 | |||
| 01:305m Talk | Mirror: Making Lock-Free Data Structures Persistent PLDIDOI | ||
| 01:355m Talk | 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 UniversityDOI | ||
| 01:405m Talk | 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 ChicagoDOI | ||
| 01:455m Talk | 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 UtahDOI Pre-print | ||
| 01:505m Talk | 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 LabsDOI | ||
| 01:555m Talk | Logical Bytecode Reduction PLDI Christian Gram Kalhauge University of California at Los Angeles; Technical University of Denmark, Jens Palsberg University of California at Los AngelesDOI | ||
| 02:005m Talk | 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-SWSDOI | ||

