Inference of Upper-Bounds on the Expected Cost of Probabilistic Programs

Resource usage analysis (a.k.a. cost analysis) aims at statically determining the number of resources required to safely execute a given program. A resource can be any quantitative aspect of the program or its environment, such as memory consumption, execution steps, energy, etc. Over the past decade several cost analysis frameworks, for different programming languages, have been developed and they can infer precise closed-form upper-bound (resp. lower-bound) functions on the worst-case (resp. bestcase) cost. However, some algorithms and problems involve probabilistic choices for which these notions of cost are not adequate. A well-known example is that of randomized algorithms, where randomized decisions are used to make the solving of computationally hard problems efficient. Besides, some problems can be precisely described only using probabilities. For example, estimating the number of attempts needed to transmit n packets of data over the network, knowing that transmission might fail with probability p. The adequate notion of cost for such scenarios is the expected cost which is, roughly, the sum of multiplying the cost of each possible trace by the probability that such a trace is produced. The goal of this work is to develop techniques for automatically inferring the expected cost of imperative probabilistic programs, using cost relations which are a formalism that generalizes classical recurrence equations and allows modeling the cost of complex programs. For this, we extend the definition of cost relations to model the expected cost, describe how to translate probabilistic programs into cost relations; and develop techniques for solving these cost relations into closed-form bounds on the expected cost. We also report on a corresponding implementation