Thu 16 Jun 2022 11:40 - 12:00 at Toucan - Analysis Chair(s): Xiaokang Qiu
Thu 16 Jun 2022 23:40 - 00:00 at Toucan - Analysis

We present a novel approach to differential cost analysis that, given a program revision, attempts to statically bound the difference in resource usage, or cost, between the two program versions. Differential cost analysis is particularly interesting because of the many compelling applications for it, such as detecting resource-use regressions at code-review time or proving the absence of certain side-channel vulnerabilities. One prior approach to differential cost analysis is to apply relational reasoning that conceptually constructs a product program on which one can over-approximate the difference in costs between the two program versions. However, a significant challenge in any relational approach is effectively aligning the program versions to get precise results. In this paper, our key insight is that we can avoid the need for and the limitations of program alignment if, instead, we bound the difference of two cost-bound summaries rather than directly bounding the concrete cost difference. In particular, our method computes a threshold value for the maximal difference in cost between two program versions \emph{simultaneously} using two kinds of cost-bound summaries—a potential function that evaluates to an upper bound for the cost incurred in the first program and an \emph{anti-potential} function that evaluates to a lower bound for the cost incurred in the second. Our method has a number of desirable properties: it can be fully automated, it allows optimizing the threshold value on relative cost, it is suitable for programs that are not syntactically similar, and it supports non-determinism. We have evaluated an implementation of our approach on a number of program pairs collected from the literature, and we find that our method computes tight threshold values on relative cost in most examples.

Thu 16 Jun

Displayed time zone: Pacific Time (US & Canada) change

10:40 - 12:00
AnalysisPLDI at Toucan +12h
Chair(s): Xiaokang Qiu Purdue University, USA
10:40
20m
Talk
CycleQ: an efficient basis for cyclic equational reasoning
PLDI
Eddie Jones University of Bristol, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol
DOI
11:00
20m
Talk
Finding the Dwarf: Recovering Precise Types from WebAssembly Binaries
PLDI
Daniel Lehmann University of Stuttgart, Michael Pradel University of Stuttgart
DOI Pre-print
11:20
20m
Talk
Abstract Interpretation Repair
PLDI
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona, Roberta Gori University of Pisa, Francesco Ranzato University of Padova
DOI Pre-print
11:40
20m
Talk
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
PLDI
Đorđe Žikelić IST Austria, Pauline Bolignano Amazon, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Franco Raimondi Amazon & Middlesex University
DOI Pre-print
22:40 - 00:00
AnalysisPLDI at Toucan
22:40
20m
Talk
CycleQ: an efficient basis for cyclic equational reasoning
PLDI
Eddie Jones University of Bristol, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol
DOI
23:00
20m
Talk
Finding the Dwarf: Recovering Precise Types from WebAssembly Binaries
PLDI
Daniel Lehmann University of Stuttgart, Michael Pradel University of Stuttgart
DOI Pre-print
23:20
20m
Talk
Abstract Interpretation Repair
PLDI
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona, Roberta Gori University of Pisa, Francesco Ranzato University of Padova
DOI Pre-print
23:40
20m
Talk
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
PLDI
Đorđe Žikelić IST Austria, Pauline Bolignano Amazon, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Franco Raimondi Amazon & Middlesex University
DOI Pre-print