SWS   Info

Public Audience

English

-- Not specified --

Saarbrücken

Research in the programming languages community has made great progress on statically estimating the execution cost of a program. The execution cost could be the number of execution steps or any other abstract metric of resource usage. Static execution cost analysis techniques based on program analysis, type systems and abstract interpretation are well-studied. However, if we are interested in establishing bounds on the execution cost of a program relative to another program's cost, naively combining worst- and best-case execution costs of the two programs does not work well in many cases. The reason is that such unary analysis techniques analyze the two programs in isolation, ignoring the similarities between the programs and their inputs.

In this thesis proposal, I propose the first relational cost analysis framework that establishes the relative cost of one program with respect to another, possibly similar program by taking advantage of the similarities in their inputs and their code. Among other things, such a relational cost analysis can be used to prove statements like: 1) Of two similar algorithms to solve a problem, one is faster than the other, without having to establish the exact complexity of either algorithm; 2) The execution cost of a program is independent of a secret input, so nothing can be inferred about the secret input by observing the cost of executing the program; and 3) The cost of a program varies very little with input changes; this can aid resource allocation and scheduling.

I show that in cases where the two programs and their inputs are closely related, relational cost analysis is superior to non-relational analysis both in terms of precision and simplicity. Specifically, I show that a refinement type and effect system provides a precise and compact mechanism for proving the relative cost of two programs.
The idea behind relational cost analysis can be extended to other nontrivial domains. In particular, I show that relational cost analysis can be adapted to prove upper bounds on the update costs of incremental programs. 
Finally, I briefly present a bidirectional technique to typecheck relational cost bounds.

--email hidden

Yes

Kaiserslautern

G26

111

passcode not visible

logged in users only