Martin Avanzini
email: martin.avanzini@inria.fr

Georg Moser
email: georgmoser@uibk.ac.at

Michael Schaper
email: michael.schaper@student.uibk.ac.at

A Modular Cost Analysis for Probabilistic Programs *

Keywords: CCS Concepts:, Theory of computation → Program analysis; Automated reasoning probabilistic programs, average complexity, automation, modularity ACM Reference

We present a novel methodology for the automated resource analysis of non-deterministic, probabilistic imperative programs, which gives rise to a modular approach. Program fragments are analysed in full independence. Moreover, the established results allow us to incorporate sampling from dynamic distributions, making our analysis applicable to a wider class of examples, for example the Coupon Collector's problem. We have implemented our contributions in the tool eco-imp, exploiting a constraint-solver over iterative refineable cost functions facilitated by off-the-shelf SMT solvers. We provide ample experimental evidence of the prototype's algorithmic power. Our experiments show that our tool runs typically at least one order of magnitude faster than comparable tools. On more involved examples, it may even be the case that execution times of seconds become milliseconds. At the same time we retain the precision of existing tools. The extensions in applicability and the greater efficiency of our prototype, yield scalability of sorts. This effects into a wider class of examples, whose expected cost analysis can be thus be performed fully automatically.

INTRODUCTION

Resource analysis is a subfield of static analysis, studying a non-functional property of programs, namely the use of resources (see [START_REF] Cohen | Two Languages for Estimating Program Efficiency[END_REF][START_REF] Wegbreit | Mechanical Program Analysis[END_REF][START_REF] Wegbreit | Verifying Program Performance[END_REF] for early references). Resource analysis impacts on the correctness or safety of programs. Programs that over-exceed available computing resources are most likely to fail, and hence cannot run correctly. See eg. [START_REF] Albert | Running on Fumes -Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis[END_REF] for an application of resource analysis on the safety of smart contracts.

In the last decades there has been significant progress in the area of fully automated resource analysis, where no user interaction is required. This resulted in significant success stories showing that resource analysis can be practicable and scalable, cf. [START_REF] Frohn | Complexity Analysis for Java with AProVE[END_REF][START_REF] Gulwani | SPEED: Precise and Efficient Static Estimation of Program Computational Complexity[END_REF][START_REF] Hoffmann | Towards Automatic Resource Bound Analysis for OCaml[END_REF][START_REF] Wilhelm | The Worst Case Execution Time Problem -Overview of Methods and Survey of Tools[END_REF][START_REF] Wilhelm | Computation Takes Time, But How Much?[END_REF]. Modularity of the analysis turned out as a key ingredient to the scalability of automated resource analysis, as modularity allows for code fragments to be analysed in full independence, so that, whole-program analyses can be overcome. This may significantly speeds up the analysis without affecting the precision of the analysis. See for example [START_REF] Avanzini | TcT: Tyrolean Complexity Tool[END_REF][START_REF] Brockschmidt | Analyzing Runtime and Size Complexity of Integer Programs[END_REF][START_REF] Frohn | Complexity Analysis for Java with AProVE[END_REF][START_REF] Gulwani | The Reachability-Bound Problem[END_REF][START_REF] Moser | From Jinja Bytecode to Term Rewriting: A Complexity Reflecting Transformation[END_REF][START_REF] Sinn | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis[END_REF][START_REF] Sinn | Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints[END_REF] for references to the literature on fully automated resource analysis methods of imperative programs.

Apart from modularity, the study of non-deterministic programs has proven immensely useful. Non-determinism appears naturally through program abstraction. Program abstraction allows to focus on those program behaviours essential for resource analysis, while ignoring other aspects. For example, in a conditional statement typically the resource usage of both branches needs to be analysed, while the condition's guard is not essential. Thus, the conditional can be abstracted by allowing for non-deterministic choice. In particular, in the analysis of imperative programs, program abstractions form an integral part. They provide the stepping stone for the modularity of static program analysis itself, for example through modular combinations of abstract interpretations, cf. [START_REF] Cousot | Modular Static Program Analysis[END_REF][START_REF] Dillig | A Modular and Symbolic Approach to Static Program Analysis[END_REF][START_REF] Gulwani | Combining Abstract Interpreters[END_REF]. For instance, it is due to program abstractions that sophisticated, fully automated analyses of complex, pointer-based programs have become possible. (See Fiedor et al. [2018] also for further pointers to the literature.)

Interrelations between computer science and probability theory are well-studied. Indeed, probabilistic variations on well-known models like automata, Turing machines or the 𝜆-calculus have been studied since the early days of theoretical computer science (see [START_REF] Kozen | Semantics of Probabilistic Programs[END_REF] for an early reference). Generalising the model of computation further and allowing for probabilistic, non-deterministic programs, induces new challenges to an automated resource analysis.

First, non-deterministic probabilistic programs have not received much attention in the literature. Predominately, the semantics of languages with non-deterministic choice are modelled in terms of Markov Decision Processes so that schedulers resolve non-deterministic choices based on the current history of states. These constructions are technical and heavy handed; in our opinion a new foundation is essential. Second, automation, in particular automation of the push-button variety is not yet firmly established. Only few prototypes exist and the literature is lacking clear experimental comparisons. Further, intuitive textbook examples, like the Coupon Collector's problem (see Figure 1c) cannot be represented properly in existing tools. This is due to the lack of support for dynamic distributions, ie. for sampling from distributions whose support or value depends on the current environment. Third, and most crucially, modularity of the analysis is not provided for. Instead, the automated analysis in all existing prototypes degenerates to a whole-program analysis. Indeed, in a probabilistic setting this is not too straight forward, as running a command results in a distribution of possible end states. The established results in this paper overcome all these issues.

We are concerned with an automated average runtime analysis of a prototypical imperative language pWhile in the spirit of Dijkstra's Guarded Command Language. This language is endowed with primitives for sampling and non-deterministic choice so that randomised algorithms can be expressed. Further, a dedicated command consume(𝑒) allows for the representation of unbounded non-negative costs given by the expression 𝑒. Non-negativity is required so as to ensure that the expected cost of a program is well-defined. Thus our automated analysis provides an expected cost analysis. By instrumenting the program so that every program statement is attributed cost one, this analysis can be used to assess the mean-time to termination and, as such, assesses that a program is (positive) almost-surely terminating [START_REF] Bournez | Proving Positive Almost-Sure Termination[END_REF].

Contributions. We present a novel modular methodology for the automated resource analysis of non-deterministic, probabilistic programs. Precisely,

• we present a novel structural operational semantics in terms of probabilistic abstract reduction systems originally due to Bournez and Garnier-significantly simplifying the formal development; following Avanzini and Yamada [2020], we refine this model by attributing costs to rules, so as neatly express the expected cost of computations. • we generalise the expected runtime transformer of Kaminski et al. [2016] to a cost transformer and formally prove it sound wrt. our novel operational semantics; • we establish a novel alternating expected cost and expected value analysis, which gives rise to the first fully modular resource analysis of non-deterministic, probabilistic programs; • we demonstrate how sampling from dynamic distributions can be incorporated, making the analysis applicable to a wider class of programs; specifically, we allow for uniform sampling from an interval dependent on program states; • we have implemented our method in the tool eco-imp and show efficiency and scalability of this automation by comparison with existing prototypes in the literature; while eco-imp parallels other tools in precision, its analysis times are significantly faster; • finally, we detail our resource analysis algorithm underlying our prototype eco-imp, together with an in-depth discussion on the employed constraint solving mechanism. Our prototype facilitates off-the-shelf SMT solvers for the iteratively refineable synthesis of cost expressions. In benchmarking, we focus on complex and novel scenarios, thus emphasising the algorithmic power and scalability of our approach. We validate its effectiveness on a set of 66 challenging probabilistic programs taken from the literature. In particular, for programs with non-linear bounds and nested loop structure our analysis is upto three orders of magnitude faster than existing prototypes. At the same time we retain the precision.

Outline. We start with motivating our quest for a modular framework in Section 2, where we also provide a high-level introduction to automated expected cost analysis. Our novel, modular approach is outlined in Section 3. Probabilistic abstract reduction systems, which form the theoretical underpinning, and our imperative language are presented in Section 4 and 5, respectively. Section 6 details a weakest precondition calculus due to [START_REF] Kaminski | Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms[END_REF], which is generalised in Section 7 to serve our needs of a modular analysis. In Section 8, the actual implementation is described and ample experimental evidence is given. In this section, we also explain our dedicated constraint solver and highlight our methodology on a handful of interesting examples. Section 9 discusses related work and we conclude in Section 10.

AUTOMATED EXPECTED COST ANALYSIS

We motivate the central contribution of our work: an automated and modular expected cost analysis of non-deterministic, probabilistic programs. First, we present a classic analysis of an algorithm incorporating a one-dimensional random walk, cf. Figure 1a. Second, we highlight the need for a more refined analysis technique, when it comes to compositionality of the analysis. Third, we detail the challenges of automated verification techniques. Finally, we motivate the need for modularity of the analysis in this context. Our contributions to this respect are highlighted in Section 3 below.

Recurrence equations. A classical way to analyse the runtime of a program is to set up a set of recurrence equations, whose closed-form provides the sought runtime. [START_REF] Wegbreit | Mechanical Program Analysis[END_REF][START_REF] Wegbreit | Verifying Program Performance[END_REF] was the first to automate this approach for deterministic programs. This idea generalises straight forward to probabilistic programs.

Consider the program C trader due to [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF] in Figure 1a, which illustrates the behaviour of a stock trader. While the stock price (𝑝) is above the minimum (𝑚𝑖𝑛), the trader decides to buy shares. The stock price is governed by a one-dimensional random walk. With probability 1 /4 the price increases (by one), and with probability 3 /4 the price decreases. To this end, an integer 𝑏 is sampled from the Bernoulli distribution with parameter 1 /4, that is, the distribution assigns 1 to 𝑏 with probability 1 /4, and 0 with probability 3 /4. After the change of the stock price takes effect, the trader decides to buy upto 10 shares, all with equal probability. In the program, this is modelled by sampling the number of shares 𝑛 from a uniform distribution of values from the interval [0, 10]. The cost for the trader is given as the total amount invested. This is indicated by the command consume(𝑝), which signals that 𝑝 units of resources are required.

Clearly, the total cost of bought shares is unbounded in some scenarios, namely, when the price 𝑝 stays above the minimum price. However, the combined probability of all such cases is 0. Worst case bounds are thus not informative in this context. A more informative measure, and the one we are interested in, is given by the expected cost. Ie. the average cost emitted on all the computational branches, weighted by their probability. Simplifying the analysis by assuming 𝑚𝑖𝑛 = 0 for now, the expected cost of C trader is expressed by the recurrence

𝑇 (𝑝) = 1 /4 • 10 𝑛=0 1 /11 • 𝑛 • (𝑝 + 1) + 𝑇 (𝑝 + 1) + 3 /4 • 10 𝑛=0 1 /11 • 𝑛 • (𝑝 -1) + 𝑇 (𝑝 -1) = 5 • 𝑝 -5 /2 + 1 /4𝑇 (𝑝 + 1) + 3 /4𝑇 (𝑝 -1) .
Here, the two sums, weighted by probabilities 1 /4 and 3 /4, respectively, give the expected cost of an increasing and decreasing stock price. The terms 𝑛 • (𝑝 + 1) and 𝑛 • (𝑝 -1), with 𝑛 taking a value between 0 and 10 with probability 1 /11, account for the cost incurred by the inner loop. This recurrence 𝑇 is a non-homogeneous linear second-order recurrence, whose closed-form can be computed as 5 • 𝑝 • (𝑝 + 1). While the general solution of the corresponding homogeneous recurrence can be derived directly (see [START_REF] Levitin | The Design and Analysis of Algorithms[END_REF]), the manual computation of the closed-form of 𝑇 requires some work. It is well-known that in general such a manual analysis-even for small and simple programs as in the case of C trader -is tedious, error prone and fragile to small changes of the recurrence equations.

Compositionality of the Analysis. A central observation in the seminal work by [START_REF] Kaminski | Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms[END_REF] is that an expected runtime analysis is inherently non-compositional, that is, from finite expected runtimes of program parts, we cannot conclude finite expected runtime of the whole program. A related issue has been encountered-and overcome-in the context of unbounded updates of non-deterministic (but non-probabilistic) programs, cf. [Ben-Amram 2011; Ben-Amram 2015; Ben-Amram and Hamilton 2019; Ben-Amram and Kristiansen 2012; [START_REF] Hirokawa | Automated Complexity Analysis Based on the Dependency Pair Method[END_REF][START_REF] Jones | A Flow Calculus of mwp-Bounds for Complexity Analysis[END_REF].

To illustrate, let us first consider the program C geo depicted in Figure 1b. In this example, the final value of 𝑥 follows a geometric distribution, more precisely, the loop will exit after 𝑖 = 1, 2, . . . iterations with probability 1 /2 𝑖-1 , in which case the variable 𝑥 will hold the value 2 𝑖 . While also this example potentially diverges, its expected cost-the number of loop iterations-is given as:

1 + 1 /2 + 1 /4 + • • • = ∞ 𝑖=1 1 /2 𝑖-1 = 2 .
Second, consider the composition of C geo with a program D, whose expected cost is given by 𝑓 (𝑥). Then the expected cost of C geo ; D, that is, running the two programs in sequence, becomes

∞ 𝑖=1 1 /2 𝑖-1 + ∞ 𝑖=1 1 /2 𝑖-1 • 𝑓 (2 𝑖 ) = ∞ 𝑖=1 1 /2 𝑖-1 • (1 + 𝑓 (2 𝑖 )) .
(1) When 𝑓 grows at least linearly, this sum is infinite. Conclusively, while the expected costs of C geo and D are finite, the expected cost of their composition is not. This is in contrast to non-probabilistic programs, where the sequential composition of two programs with bounded runtime yields again a program with bounded runtime. Generalising a weakest precondition calculus à la Dijkstra's to an expected runtime transformer ert, Kaminski et al. overcome this issue through the expression of the expected runtime in continuation passing style, cf. [START_REF] Kaminski | A Weakest Pre-expectation Semantics for Mixed-sign Expectations[END_REF]Kaminski et al. 2016[START_REF] Kaminski | Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms[END_REF]Olmedo et al. 2016]. As already observed by Kaminski et al.-and as we will see later in Section 6-this transformer in turn generalises seamlessly to an expected cost transformer

ect[C] : (Σ → R ∞ ≥0 ) → (Σ → R ∞ ≥0 )
, for reasoning about expected costs. Informally, when 𝑓 : Σ → R ∞ ≥0 measures the expected cost of a continuation in terms of a valuation 𝜎 ∈ Σ, ect[C] (𝑓 ) yields the overall cost of first executing C, followed by the continuation. The expected cost of a program C is then given by ecost[C] ≜ ect[C] (𝜆𝜎.0), ie. by attributing the continuation a cost of 0.

Formalising the expected cost in terms of a cost transformer facilitates a recursive definition of program costs. If 𝑒 evaluates to a natural 𝑖 under a given store, we set ect[consume(𝑒)] (𝑓 ) ≜ 𝜆𝜎.𝑖 + 𝑓 (𝜎), which accounts for the fact that consume(𝑒) incurs an additional cost of 𝑖. If 𝑑 evaluates to a distribution assigning probabilities 𝑝 𝑖 to integers 𝑖 under a given store 𝜎, we let ect where 𝜙 ⊨ 𝑓 = 𝑔 indicates that 𝑓 coincides with 𝑔 on inputs satisfying 𝜙. Following standard semantics, the expected cost thus equals the cost of unrolling the loop once in case the guard 𝜙 holds, or the cost 𝑓 of the continuation when the guard does not hold. To illustrate this, re-consider the program C geo from Figure 1b. Let us denote by 𝐶 (𝑏, 𝑥) the expected cost of the while-loop wrt. a cost of the continuation 𝑓 , measured in the program variable 𝑥. Then (2) translates to

𝑏 = 1 ⊨ 𝐶 (𝑏, 𝑥) = 1 + 1 /2 • 𝐶 (1, 2 • 𝑥) + 1 /2 • 𝐶 (0, 2 • 𝑥) 𝑏 ≠ 1 ⊨ 𝐶 (𝑏, 𝑥) = 𝑓 (𝑥) .
Since 𝑏 and 𝑥 are initialized to one, 𝐶 (1, 1) then gives the cost (1) of C geo . To derive closed forms for the expected cost, we can again resort to methods for solving such (conditional) recurrences, unlike above however, recurrences can be extracted in a systematic, compositional way.

To sum up, the ert-calculus and its expected cost derivative, are more refined technical tools for the analysis of probabilistic programs than the classical analysis through recurrence relations. The analysis becomes clean and is less fragile. Kaminski et al. have shown that the ert-calculus allows an optimal analysis of a variety of interesting case studies, like eg. the Coupon Collector's Problem formulated with the program C coupons from Figure 1c. However, [START_REF] Kaminski | Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms[END_REF] do not provide an automation and also only superficially concepts automation. So the method remains tedious.

Automation. The crux of turning such a calculus into a fully automated analysis lies in deriving closed forms for expected costs of loops. Related problems have been extensively studied in the literature, eg. [START_REF] Contejean | Mechanically Proving Termination Using Polynomial Interpretations[END_REF][START_REF] Fuhs | SAT Solving for Termination Analysis with Polynomial Interpretations[END_REF][START_REF] Podelski | A Complete Method for the Synthesis of Linear Ranking Functions[END_REF]. One prominent approach lies in assigning templates to cost functions, by which the recurrences can be reduced to a set of constraints treatable with off-the-shelf SMT solvers.

The Absynth prototype provided by [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF] has been the first automated expected resource analysis of probabilistic programs, implementing such an approach, thereby demonstrating the feasibility of an automated analysis. For instance, Absynth infers the manual bound on the expected cost of C trader shown above, fully automatically. Conceptually, this tool can be seen as a specialised automation of Kaminski's ert-calculus. The transformer is coached into a Hoarestyle calculus and expected cost functions are formalised as potential functions [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF]. Automation is achieved by specialising these potential functions to linear combinations of base functions, the latter abstracting stores as non-negative numbers.

Recently, [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF] provides a resource analysis, based on martingale theory. Notably, their methodology is the first to also account for negative costs. The main challenge in accommodating negative costs lies in ensuring that the overall expected cost remains well-defined. Wang et al. ensures this by requiring that in the presence of negative costs, program updates are generally bounded and almost-sure termination is required.

Modularity of the Analysis. It is perhaps important to emphasise that composability of the analysis of the expected cost of sequential commands does not induce composability of the synthesis of the corresponding bounding functions. We illustrate the difference wrt. C trader . Concretely, as C trader features a nested loop, its expected cost is driven by the following inter-dependent constraints. Below, 𝐼 (𝑛, 𝑝, 𝑚𝑖𝑛) and 𝑂 (𝑛, 𝑝, 𝑚𝑖𝑛) stands for the cost before entering the inner and outer loop, respectively.

𝑝 > 𝑚𝑖𝑛 ≥ 0 ⊨ 𝑂 (𝑛, 𝑝, 𝑚𝑖𝑛) = 1 /4 • 10 𝑛=1 1 /11 • 𝐼 (𝑛, 𝑝 + 1, 𝑚𝑖𝑛) + 3 /4 • 10 𝑛=1 1 /11 • 𝐼 (𝑛, 𝑝 -1, 𝑚𝑖𝑛) ¬(𝑝 > 𝑚𝑖𝑛 ≥ 0) ⊨ 𝑂 (𝑛, 𝑝, 𝑚𝑖𝑛) = 0 𝑛 ≥ 0 ⊨ 𝐼 (𝑛, 𝑝, 𝑚𝑖𝑛) = 𝑝 + 𝐼 (𝑛 -1, 𝑝, 𝑚𝑖𝑛) ¬(𝑛 ≥ 0) ⊨ 𝐼 (𝑛, 𝑝, 𝑚𝑖𝑛) = 𝑂 (𝑛, 𝑝, 𝑚𝑖𝑛) .
Here, through the first equation, the cost of the outer loop 𝑂 (𝑛, 𝑝, 𝑚𝑖𝑛) depends on the cost of the inner loop. Vice verse, since the execution of the inner loop eventually gives back control, the cost of the inner loop 𝐼 (𝑛, 𝑝, 𝑚𝑖𝑛) is also dependent on the outer loop. Therefore, the costs 𝐼 (𝑛, 𝑝, 𝑚𝑖𝑛) and 𝑂 (𝑛, 𝑝, 𝑚) cannot be considered in isolation. In general, synthesis degenerates to a whole-program analysis, ie. program parts cannot be treated in isolation.

Indeed, the aforementioned tool Absynth [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF]] and the prototype described by Wang et al. perform such a whole-program analysis, which is not modular and results in issues with scalability even on small, handcrafted examples. To whit, consider a more realistic variant of C trader , where the stock trader is choosing uniformly upto 100.000 shares. In this setting, Absynth is no longer able to compute a bound, while the prototype established by [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF] requires upto 20 seconds of runtime-additionally a significant amount of user guidance is required. Similar issues hold wrt. multiple nested loops (see Figure 8). In contrast, we provide a novel modular and efficient automation, inspired by the continuation-passing style analysis method formalised in the ert-calculus, which is free of the aforementioned scalability issues. In the following, we refer to the composability of the synthesis of upper invariants as modularity of the (expected) cost analysis. In the next section we provide a high-level overview of the crucially needed concepts to provide such a modular analysis.

A MODULAR EXPECTED COST ANALYSIS

Modularity requests that the cost analysis for a program can be broken into an independent cost analysis of program parts. This establishes a crucial stepping stone for the scalability of the analysis. For that, we suite the approach outlined in the preceding section to one that interleaves a value analysis.

It is well known that a modular cost analysis can be obtained by combining cost with an analysis on how values evolve within a program [START_REF] Avanzini | TcT: Tyrolean Complexity Tool[END_REF][START_REF] Brockschmidt | Analyzing Runtime and Size Complexity of Integer Programs[END_REF][START_REF] Frohn | Complexity Analysis for Java with AProVE[END_REF][START_REF] Gulwani | The Reachability-Bound Problem[END_REF][START_REF] Moser | From Jinja Bytecode to Term Rewriting: A Complexity Reflecting Transformation[END_REF][START_REF] Sinn | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis[END_REF][START_REF] Sinn | Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints[END_REF]. Consider for instance a sequential command C; D. To determine the cost of this command from the costs of C and D, given as functions in their input states, it is necessary to determine how the program's state evolves to the point where the second command is executed. A value analysis provides such additional information. The case is similar for loops, that sequentially execute a given command several times.

Combining Cost with Value Analysis. Since it is clearly infeasible to reason how program values evolve in all-possibly uncountable many-execution paths, we focus on incorporating an expected, or mean value analysis. To this end, we start with an expected cost transformer as outlined above. As in previous approaches, we express program costs as linear combination of base functions 𝑏 𝑖 , mapping program valuations to (positive) real numbers. These base functions serve as a numerical abstraction of program stores. Base functions encompass a variety of common abstractions, for example the absolute value of a variable, the difference between two variables and more generally arbitrary polynomial combinations thereof.

In the majority of cases, expected costs can be computed symbolically on such cost expressions. Particularly, we express the cost of a loop while (𝜙) {C} as a linear combination 𝜅 (𝑏 1 , . . . , 𝑏 𝑛 ) of base functions. Rather than directly subjecting this symbolic bound to recurrences (2) however, we seek for an upper-bound satisfying

𝜙 ⊨ 𝜅 (𝑏 1 , . . . , 𝑏 𝑛 ) ≥ ecost[C] + 𝜅 (evalue[C] (𝑏 1 ), . . . , evalue[C] (𝑏 𝑛 )) ¬𝜙 ⊨ 𝜅 (𝑏 1 , . . . , 𝑏 𝑛 ) ≥ 0 (3)
[x x + 1; b Bernoulli( 1 /2)] (𝜆𝜎.𝜎 (𝑏) • 𝜎 (𝑥)) = 𝜆𝜎. 1 /2 • (𝜎 (𝑥) + 1) .
The constraints (3) thus witnesses that the inferred cost 𝜅 (𝑏 1 , . . . , 𝑏 𝑛 ) of the loop while (𝜙) {C} dominates the cost of an iteration (ecost[C]), plus the cost of re-iterating the loop, in terms of measures 𝑏 𝑖 after the execution (𝜅 (evalue[C] (𝑏 1 ), . . . , evalue[C] (𝑏 𝑛 ))).

In contrast to the constraints given by (2), in (3), the cost 𝜅 (𝑏 1 , . . . , 𝑏 𝑛 ) is not passed down along the transformer given by the body C. Indeed, ecost[C], as well as the expected values evalue[C] (𝑏 𝑖 ) of base functions 𝑏 𝑖 can be pre-computed and substituted into the above upper bounds, and then offloaded to a constraint solver to determine a concrete bound, in isolation. To whit, reconsider the trader example C trader from Figure 1a. Rather than proceeding top-down to extract the recurrences in the preceding section, we proceed inside out and start with the analysis of the inner loop

while (n > 0) { consume(p); n n -1 }
While the body is iterated 𝑛 > 0 times, the cost of the loop's body is 𝑝 ≥ 0. This suggests 𝑛 and 𝑝 play a role in the cost of this loop. Let us thus choose the template 𝜅 (⟨𝑛⟩, ⟨𝑝⟩, ⟨𝑛⟩ • ⟨𝑝⟩), a simple-mixed template [START_REF] Contejean | Mechanically Proving Termination Using Polynomial Interpretations[END_REF]] over (non-negative) base-functions ⟨𝑛⟩ = max(𝑛, 0) and ⟨𝑝⟩ = max(𝑝, 0). Since 𝑛 is decremented in the loop body while 𝑝 remains unchanged, the (expected) value of the three given base functions is given by ⟨𝑛-1⟩, ⟨𝑝⟩ and ⟨𝑛-1⟩•⟨𝑝⟩, respectively. Based on these, the upper bounds (3) translates to

𝑛 > 0 ⊨ 𝜅 (⟨𝑛⟩, ⟨𝑝⟩, ⟨𝑛⟩ • ⟨𝑝⟩) ≥ 𝑝 + 𝜅 (⟨𝑛 -1⟩, ⟨𝑝⟩, ⟨𝑛 -1⟩ • ⟨𝑝⟩) 𝑛 ≤ 0 ⊨ 𝜅 (⟨𝑛⟩, ⟨𝑝⟩, ⟨𝑛⟩ • ⟨𝑝⟩) ≥ 0 .
The inequalities hold by taking 𝜅 (𝑥, 𝑦, 𝑧) ≜ 𝑧 as indeed, 𝑛 > 0 entails ⟨𝑛⟩ • ⟨𝑝⟩ ≥ 𝑝 + ⟨𝑛 -1⟩ • ⟨𝑝⟩, and ⟨𝑛⟩ • ⟨𝑝⟩ is always non-negative. The cost of the program is thus (tightly) upper-bounded by ⟨𝑛⟩ • ⟨𝑝⟩. One can now proceed with the outer loop, by substituting this bound in the recurrence (3) and derive the bound

10 • ⟨𝑚𝑖𝑛 + 1⟩ • ⟨𝑝 -𝑚𝑖𝑛⟩ + 5 • ⟨𝑝 -𝑚𝑖𝑛⟩ 2 .
(4) See Section 7.1 for further details.

Proving that (3) yields indeed an upper-bound 𝜅 (𝑏 1 , . . . , 𝑏 𝑛 ) on the cost of loops is non-trivial in the presence of probabilistic sampling. Indeed, our main theorem witnessing the soundness of this approach, Theorem 7.5, relies essentially on the fact that 𝜅 is assumed a linear, more generally concave, function.

Computing Expected Values. A crucial insight is that the ect-calculus keeps track of expected values on cost functions 𝑓 . As it turns out, this machinery can be turned into one for reasoning about expected values. Indeed, we have ect

[C] (𝑓 ) = ecost[C] + evalue[C] (𝑓 ) for probabilistic programs 1 C
. By removing all cost emitting statements consume(𝑒) from C, or alternatively, by setting evalue[consume(𝑛)] (𝑓 ) ≜ 𝑓 , but otherwise defining the expected value along the way of the expected cost transformer, we obtain a recursive definition that can be inferred by exactly the same procedure we employ to reason about expected costs.

Automating our Approach. We have successfully automated this approach in our tool eco-imp, see Section 8. This tool proceeds with an analysis as just outlined, and integrates a dedicated constraint solver for solving constraints of the form (3). Our tool derives the bound (4) in 25ms. This constitutes a significant speedup to the Absynth prototype-which can be considered among the most efficient implementations of such an analysis to date-which requires more than 3 seconds, and the prototype of [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF] which requires 10 seconds to analyse this example. Our implementation significantly benefits from the fact that program fragments can be considered in isolation. For one, the recurrences handled are considerably simpler, as they describe a single loop, rather than the whole program's cost behaviour. But also heuristics, such as for constructing suitable templates from a given program can be made more precise, and simpler. Indeed, as it turned out, we do not even require the (brittle) use of invariant generation tools [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF] or manual annotations for this task [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]. Unsurprisingly, the approach is particularly effective in the analysis of nested loops, which has direct consequences for the scalability and speed of the analysis. Benefits are, of course, most pronounced when the program under consideration contains nested loops, see Section 8.2 where we present our experimental evaluation.

An Intuitive Textbook Example. We conclude this section with a non-trivial example that is beyond the scope of pre-existing tools. Following the formulation of [START_REF] Mitzenmacher | Probability and Computing: Randomized Algorithms and Probabilistic Analysis[END_REF], the above mentioned Coupon Collector's problem states as follows. Given a box with 𝑛 different coupons, one is interested in the expected number of draws (with replacement) that are needed before having drawn each coupon at least once. The corresponding code C coupons is depicted in Figure 1c. Here, coupons represents the number of unique coupons collected; draw is sampled uniformly from the interval [1,n], with n an input parameter. The chosen cost model reflects the number of trials. Note, that the probability of collecting a new coupon drops in proportion of the collected coupons, that is, in proportion1 /𝑐𝑜𝑢𝑝𝑜𝑛𝑠 + 1. In particular, the expected cost is finite.

The full pen-and-paper analysis of C coupons given by [START_REF] Kaminski | Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms[END_REF]-which provides the optimal expected time bound O(𝑛 log 𝑛)-spans several pages and requires non-trivial estimations. Thus, non surprisingly, automation poses significant challenges. So far, to the best of our knowledge, the Coupon Collector's problem has been elusive to an automated analysis. As already mentioned, no existing tool can even represent the corresponding code C coupons . To date support for dynamic probabilistic branching-when sampling draws a number of samples not statically bounded-is lacking. When sampling is in contrast static, expectations are finite, weighted sums, and consequently can be encoded by their unfolding. When sampling is dynamic though, such as within the program C coupons through the assignment draw Uniform(1,n), such an unfolding is no longer possible. To illustrate this, observe

ect[draw Uniform(1,n)] (𝑓 ) = 𝜆𝜎. 𝜎 (𝑛) 𝑖=1 1 /𝜎 (𝑛) • 𝑓 (𝜎 [𝑑𝑟𝑎𝑤/𝑖]) .
To reason about such costs, we define the sum in terms of a constraint of the form (3), and make use of our dedicated constraint solver to find an upper bound. See Section 8 for the details.

Through this encoding, our prototype eco-imp is able to derive the (non-optimal) bound 𝑛+ 1 /2•𝑛 2 fully automatically in a fraction of a second for the expected cost of C coupons . If the distribution is set statically, eg. to a uniform distribution of 10 coupons, the example becomes expressible by existing tools through unrolling. Alas, only the Absynth tool can provide a (non-optimal) bound (see Section 8.2). Still the employed potential functions are not amenable to express the subtle dependency of the expected cost of C coupons on the (now) static distribution governing the draw. Ie. the generated constraint grows linearly to the number of coupons. Wrt. tool execution time this implies that our prototype eco-imp handles a uniform distribution of upto 100 coupons in seconds. On the other hand the Absynth tool and the prototype by [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]] cannot provide bounds for larger numbers, even after several minutes of runtime, cf. Table 2

(d).

PROBABILISTIC REDUCTION SYSTEMS

Probabilistic abstract reduction systems are due to [START_REF] Bournez | Proving Positive Almost-Sure Termination[END_REF] and form a generalisation of abstract reduction systems, accounting for probabilistic choice. Avanzini and Yamada [2020] extend probabilistic abstract reduction systems with weights, allowing for the formulation of a suitable cost model. We refer to the weighted variant again as probabilistic abstract reduction systems (PARSs).

Let R ∞ ≥0 denote the set of non-negative real numbers extended with ∞, ie. R ∞ ≥0 ≜ R ≥0 ∪ {∞}. A (discrete) subdistribution over 𝐴 is a function 𝛿 : 𝐴 → R ≥0 so that 𝑎 ∈𝐴 𝛿 (𝑎) ≤ 1, and a distribution if 𝑎 ∈𝐴 𝛿 (𝑎) = 1. We may write subdistributions 𝛿 as {{𝛿 (𝑎) : 𝑎}} 𝑎 ∈𝐴 . The set of all subdistributions over 𝐴 is denoted by D (𝐴). We restrict to distributions over countable sets 𝐴. The expectation of a function 𝑓 : 𝐴 → R ∞ ≥0 wrt. a distribution 𝛿 is given by E 𝛿 (𝑓 ) ≜ 𝑎 ∈𝐴 𝛿 (𝑎) • 𝑓 (𝑎).

Probabilistic abstract reduction systems. A PARS over 𝐴 is a set of rules 𝑎 -→ 𝛿 indicating that 𝑎 ∈ 𝐴 reduces to 𝑏 ∈ 𝐴 with probability 𝛿 (𝑏) if 𝛿 (𝑏) ≠ 0. Operationally, a reduction step on 𝑎 involves first picking a rule 𝑎 -→ 𝛿 (among possibly many) and then sampling the reduct from 𝛿. To allow for non-uniform costs, we endow each rule with a weight 𝑤 ∈ R ≥0 , accounting for the cost of the corresponding reduction step, cf. [Avanzini and Yamada 2020]. Thus formally, a PARS on 𝐴 is given by ternary relation

• • - → • ⊆ 𝐴 × R ≥0 × D (𝐴)
, where in a rule 𝑎 𝑤 -→ 𝛿, the weight 𝑤 indicates the cost of the rule application. Objects 𝑎 ∈ 𝐴 with no rule 𝑎 𝑤 -→ 𝛿 are called terminal, in notation 𝑎↓. PARSs constitute a universal probabilistic model of computation well-suited to model small-step operational semantics of our probabilistic language. For instance, the program C geo from Figure 1b is modelled by the PARS --→ geo , defined by

geo(𝑥) 1 --→ geo {{ 1 /2 : 2 • 𝑥, 1 /2 : geo(2 • 𝑥)}} for all 𝑥 ∈ Z.
Following [Avanzini et al. 2020;Avanzini and Yamada 2020], we define the dynamics of a PARS → in terms of a (weight-indexed) reduction relation

• • - → → • ⊆ M (𝐴) × R ≥0 × M (𝐴)
𝜇 0 - → → 𝜇 𝑎 𝑤 -→ 𝛿 {{1 : 𝑎}} 𝑤 -→ → 𝛿 𝜇 𝑖 𝑤 𝑖 --→ → 𝜈 𝑖 𝑖 ∈𝐼 𝑝 𝑖 • 𝜇 𝑖 𝑤 -→ → 𝑖 ∈𝐼 𝑝 𝑖 • 𝜈 𝑖 .
In the second rule, distributions are lifted to multidistributions in the obvious way.

{{1 : geo(1)}} 1 --→ geo → {{ 1 /2 : 2, 1 /2 : geo(2)}} 1 /2 --→ geo → {{ 1 /2 : 2, 1 /4 : 4, 1 /4 : geo(4)}} 1 /4 --→ geo → • • • . We write 𝜇 𝑤 -→ → 𝑛 𝜈 if 𝜇 𝑤 1 --→ → • • • 𝑤 𝑛 --→ → 𝜈 for 𝑤 = 𝑛 𝑖=1 𝑤 𝑖 . Expected cost. A reduction from 𝑎 ∈ 𝐴 is a, generally infinite, sequence Δ : {{1 : 𝑎}} 𝑤 0 --→ → 𝜇 1 𝑤 1 --→ → 𝜇 2 𝑤 2 --→ → • • • . The infinite sum 𝑤 = 𝑖 ∈N 𝑤 𝑖
gives the expected cost of this specific reduction. Since the weight 𝑤 𝑖 are non-negative, this sum is always well-defined (although it may be infinite). Throughout the following, the set of costs C is given by R ∞ ≥0 . Due to the presence of non-determinism, expected costs are in general not unique. Taking a demonic view on non-determinism, we define the expected cost function, denoted as ecost[→] : 𝐴 → C, as the function that associates each 𝑎 ∈ 𝐴 with the maximal expected cost of reductions starting from {{1 : 𝑎}}. Concisely, via the monotone convergence theorem of real numbers this can be defined as

ecost[→] (𝑎) ≜ sup 𝑤 | {{1 : 𝑎}} 𝑤 -→ → 𝑛 𝜇 .
For instance, we have ecost

[--→ geo ] (geo(𝑥)) = sup{ 𝑛 𝑖=0 1 /2 𝑖 | 𝑛 ∈ N} = ∞ 𝑖=0 1 /2 𝑖 = 2.
Remark. In the literature, the operational semantics of purely probabilistic programs, are usually modelled as Markov chains over program states. Here, the 𝑖-th random variable in this chain gives the probability of being in a state after 𝑖 reduction steps. On the other hand, the operational semantics of languages with non-deterministic choice are modelled in terms of Markov Decision Processes (MDPs) (see, eg. [START_REF] Agrawal | Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs[END_REF][START_REF] Chakarov | Probabilistic Program Analysis with Martingales[END_REF][START_REF] Kaminski | Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms[END_REF]Olmedo et al. 2016]). Schedulers (aka policies) resolve non-deterministic choices based on the current history of states, thereby breaking down reductions again to Markov chains. Such MDPs 𝑀 are naturally modelled as PARSs → 𝑀 , so that the Markov chains induced by the schedulers are in one-to-one correspondence with reductions wrt. → 𝑀 . The distribution underlying the 𝑖-th random variable is represented by the 𝑖-th multidistribution in the corresponding reduction. The use of multidistributions, rather than distributions, eliminates the need for schedulers, intuitively, because multidistributions within a reduction implicitly encode histories, cf. Avanzini et al. [2020].

Particularly, Avanzini et al. [2020] proves the following correspondence.

Proposition 4.1 ([Avanzini et al. 2020;Avanzini and Yamada 2020]). Suppose each rule in the PARS → is attributed weight one. Then ecost[→] coincides with the expected time to termination under the standard MDP semantics of [START_REF] Bournez | Proving Positive Almost-Sure Termination[END_REF].

While the proposition assumes a unitary cost model, where each reduction step is attributed cost one, the proposition generalises to arbitrary (non-negative) costs as employed in the definition of ecost[→].

Expected Cost Transformers for PARSs

In this subsection, we define an expected cost transformer ect[→] for arbitrary PARSs →. This transformer, generalising the expected cost function, serves as a technical tool to prove soundness and completeness of our methods.

To this end, we quickly recap notions from program semantics, cf. [START_REF] Winskel | The Formal Semantics of Programming Languages[END_REF]. A poset (𝐴, ⊑)

is called an 𝜔-CPO, if every 𝜔-chain 𝑎 0 ⊑ 𝑎 1 ⊑ • • • has a supremum sup{𝑎 𝑛 | 𝑛 ∈ N} ∈ 𝐴. A function 𝑓 : 𝐴 → 𝐵 between two 𝜔-CPOs is called (Scott)-continuous if 𝑓 (sup 𝑛 ∈N 𝑎 𝑛 ) = sup 𝑛 ∈N 𝑓 (𝑎 𝑛
) holds for all 𝜔-chains (𝑎 𝑛 ) 𝑛 ∈N . Recall that a continuous function is monotone, wrt. the underlying orders of the poset. Kleene's Fixed-Point Theorem asserts that, if 𝑓 : 𝐴 → 𝐴 is continuous and 𝐴 features a least element ⊥, the least fixed-point lfp(𝑓 ) of 𝑓 is given lfp(𝑓 ) ≜ sup 𝑛 ∈N 𝑓 𝑛 (⊥) for 𝑓 𝑛 the 𝑛-fold composition of 𝑓 . Let C 𝐴 ≜ {𝑓 | 𝑓 : 𝐴 → C} denote the set of cost functions over 𝐴. We endow this set with the order ≤ defined by 𝑓 ≤ 𝑔 if 𝑓 (𝑎) ≤ 𝑔(𝑎) for all 𝑎 ∈ 𝐴. We also extend functions over C point-wise to cost functions and denote these extensions in bold face font, as we already did above, eg., 𝑓 + 𝑔 ≜ 𝜆𝑎.𝑓 (𝑎) + 𝑔(𝑎) for 𝑓 , 𝑔 ∈ C 𝐴 etc. In particular, 0 = 𝜆𝑎.0 and ∞ = 𝜆𝑎.∞. The proof of the following is standard. Proposition 4.2 (Cost functions form an 𝜔-CPO). For any 𝐴, (C 𝐴 , ≤) is an 𝜔-CPO, with least and greatest element 0 and ∞, respectively. The supremum of 𝜔-chains (𝑓 𝑛 ) 𝑛 ∈N is given point-wise:

sup 𝑛 ∈N 𝑓 𝑛 ≜ 𝜆𝑎. sup 𝑛 ∈N 𝑓 𝑛 (𝑎).
The following definition introduces the expected cost transformer of a PARS →. Informally, this transformer associates each 𝑎 ∈ 𝐴 with its expected cost, plus the expected value of a given cost function 𝑓 on terminal objects.

𝜒 𝑓 (𝑔) ≜ 𝜆𝑎. 𝑓 (𝑎) if 𝑎↓, sup{𝑤 + E 𝛿 (𝑔) | 𝑎 𝑤 -→ 𝛿 } else.
It can be shown that for any 𝑓 , 𝜒 𝑓 (𝑔) is a continuous functional. Hence ect[→] (𝑓 ) is well-defined. Moreover, it is continuous and hence monotone.

A PROBABILISTIC LANGUAGE

We consider an imperative language pWhile in the spirit of Dijkstra's Guarded Command Language, endowed with a non-deterministic choice operator <> and where the assignment statement is generalised to one that can sample from a distribution. A command consume(𝑒) signals the consumption of 𝑒 ≥ 0 resource units. We fix a finite set of integer-valued variables Var. Stores are denoted by

𝜎 ∈ Σ ≜ Var → Z. With 𝜙 ∈ BExp ≜ Σ → B, 𝑒 ∈ Exp ≜ Σ → Z, and 𝑑 ∈ DExp ≜ Σ → D (Z) we denote, Boolean, Integer, 𝜎 ⊲ 𝑥 𝑑 0 -→ {{𝑝 𝑖 : 𝜎 [𝑥/𝑖] | 𝑝 𝑖 = 𝑑 (𝜎)(𝑖) > 0}} 𝑖 ∈Z [Assign] 𝜎 ⊲ skip 0 -→ 𝜎 [Skip] 𝜎 ⊲ abort 0 -→ ∅ [Abort] 𝜎 ⊲ consume(𝑒) ⟨𝑒 (𝜎) ⟩ ------→ 𝜎 [Consume] 𝜎 ⊨ 𝜙 𝜎 ⊲ if (𝜙) {C} {D} 0 -→ 𝜎 ⊲ C [IfT] 𝜎 ⊭ 𝜙 𝜎 ⊲ if (𝜙) {C} {D} 0 -→ 𝜎 ⊲ D [IfF] 𝜎 ⊨ 𝜙 𝜎 ⊲ while (𝜙) {C} 0 -→ 𝜎 ⊲ C; while (𝜙) {C} [WhileT] 𝜎 ⊭ 𝜙 𝜎 ⊲ while (𝜙) {C} 0 -→ 𝜎 [WhileF] 𝑖 ∈ {1, 2} 𝜎 ⊲ {C 1 } <> {C 2 } 0 -→ 𝜎 ⊲ C 𝑖 [Choice] 𝜎 ⊲ C 𝑟 - → {{𝑝 𝑖 : 𝜎 𝑖 ⊲ C 𝑖 }} 𝑖 ∈𝐼 ⊎ 𝑞 𝑗 : 𝜎 𝑗 𝑗 ∈𝐽 𝜎 ⊲ C; D 𝑟 - → {{𝑝 𝑖 : 𝜎 𝑖 ⊲ C 𝑖 ; D}} 𝑖 ∈𝐼 ⊎ 𝑞 𝑗 : 𝜎 𝑗 ⊲ D 𝑗 ∈𝐽 [Compose]
Fig. 2. Small-step operational semantics as a PARS.

and Integer-valued distribution expression over Var, respectively. The syntax of program commands Cmd is given as follows.

C, D ::

= 𝑥 𝑑 | skip | abort | consume(𝑒) | C; D | if (𝜙) {C} {D} | while (𝜙) {C} | {C} <> {D} .
Commands are fairly standard. The assignment statement 𝑥 𝑑 samples a value from 𝑑, ie. an expression that evaluates to a distribution over integers. This command generalises the usual non-probabilistic assignment 𝑥 𝑒. The command consume(𝑒) consumes 𝑒 resource units but acts as a no-op otherwise. Here 𝑒 is a non-negative but otherwise arbitrary integer-valued expression. Particularly, the incurred cost can depend on the programs state rather than being constant. The non-deterministic choice operator {C} <> {D} executes either C or D. For brevity, we omit a probabilistic choice command and probabilistic guards as by Kaminski et al. [2016], since they do not add to the expressiveness of our language.

Semantics. We model reduction semantics of our language as a PARS over configurations Conf ≜ (Cmd × Σ) ∪ Σ. Elements (C, 𝜎) ∈ Conf are denoted by 𝜎 ⊲ C and signal that the command C is to be executed under the current store 𝜎, whereas 𝜎 ∈ Conf indicates that the computation has halted with final store 𝜎. The (infinite) PARS is depicted in Figure 2. Rules 𝜎 ⊲ C 𝑤 -→ {{1 : 𝛾 }} without probabilistic effect are written as 𝜎 ⊲ C 𝑤 -→ 𝛾 for brevity. For 𝜙 ∈ BExp and 𝜎 ∈ Σ we denote by 𝜎 ⊨ 𝜙 that 𝜙 evaluates on 𝜎 to true. Note that only in Rule (Consume) resources are consumed. Here, ⟨𝑧⟩ ≜ max(0, 𝑧) denotes Macaulay's bracket. As we had for PARSs, incurred costs are thus always non-negative.

EXPECTED COST AND EXPECTED VALUE TRANSFORMERS

We now suite the ert-transformer of Kaminski et al. [2016] to an expected cost transformer. To this end, for 𝜙 ∈ BExp, we lift Iverson brackets [•] to stores, resulting in the cost function [𝜙](𝜎) ≜ 1 if 𝜎 ⊨ 𝜙, and [𝜙](𝜎) ≜ 0 otherwise. In particular, [𝜙] • 𝑓 + [¬𝜙] • 𝑔 evaluates to 𝑓 (𝜎) on stores 𝜎 ⊨ 𝜙, and to 𝑔(𝜎) if 𝜎 ⊨ ¬𝜙. We denote by 𝑓 [𝑥/𝑣] the cost function that applies 𝑓 on the modified store where 𝑥 takes value 𝑣.

Our expected cost transformer ect[•] (•) : Cmd → C Σ → C Σ operates on cost functions over stores, that is, elements of C Σ . In the literature 𝑓 ∈ C Σ are also referred to as expectations [Kaminski et al. 2016]. As already indicated in Section 2, the cost ect[C] (𝑓 ) should be seen as the cost of evaluating C wrt. to a continuation of expected cost 𝑓 . Remark. The earlier defined expected cost transformer ect[→] wrt. PARS → (see Section 4) abstracts the above definition of the expected cost transformer wrt. programs C. As we see in in the next subsection, these are in correspondence. Hence, we take the liberty to employ the same notations.

C ect[C] (𝑓 ) evalue[C] (𝑓 ) consume(𝑒) ⟨𝑒⟩ + 𝑓 𝑓 skip 𝑓 𝑓 abort 0 0 𝑥 𝑑 𝜆𝜎.E 𝑑 (𝜎) (𝜆𝑣.𝑓 [𝑥/𝑣] (𝜎)) 𝜆𝜎.E 𝑑 (𝜎) (𝜆𝑣 .𝑓 [𝑥/𝑣] (𝜎)) C; D ect[C] (ect[D] (𝑓 )) evalue[C] (evalue[D] (𝑓 )) if (𝜙) {C} {D} [𝜙] • ect[C] (𝑓 ) + [¬𝜙] • ect[D] (𝑓 ) [𝜙] • evalue[C] (𝑓 ) + [¬𝜙] • evalue[D] (𝑓 ) while (𝜙) {C} lfp(𝜆𝐹 .[𝜙] • ect[C] (𝐹 ) + [¬𝜙] • 𝑓 ) lfp(𝜆𝐹 .[𝜙] • evalue[C] (𝐹 ) + [¬𝜙] • 𝑓 ) {C} <> {D} max(ect[C] (𝑓 ), ect[D] (𝑓 )) max(evalue[C] (𝑓 ), evalue[D] (𝑓 ))
With the above intuition in mind, most of the cases are straight forward to derive from the operational semantics given in Figure 2. In the case of a statement consume(𝑒), a cost of 𝑒 is incurred (provided 𝑒 (𝜎) ≥ 0) in addition to the cost of the continuation. While skip is a no-op, consequently ect[skip] (𝑓 ) = 𝑓 , the command abort immediately aborts the computation and thus ect[abort] (𝑓 ) = 0. Running an assignment 𝑥 𝑑 followed by a continuation amounts to first sampling a value 𝑣 for 𝑥 according to 𝑑, say with probability 𝑝 𝑣 , updating 𝑥 in the given store 𝜎 to 𝑣, and then running the continuation on the updated store. The overall expected resource consumption is thus given by the sum of expected costs 𝑓 [𝑥/𝑣] of all such runs, weighted by their probability 𝑝 𝑣 . For instance, if Bernoulli(p) denotes the Bernoulli distribution with parameter 𝑝, (yielding 1 with probability 𝑝 and 0 with probability 𝑝 -1), then ect

[𝑥 Bernoulli( 1 /3)] (𝑓 ) = 1/3 • 𝑓 [𝑥/1] + 2/3 • 𝑓 [𝑥/0]. For sequential commands C; D, ect[C; D] is given by the composition ect[C] • ect[D],
transforming the cost 𝑓 of a continuation to that of running C, then D followed by the continuation. For conditionals if (𝜙) {C} {D}, the transformer perform a case analysis on the guard. Considering loops while (𝜙) {C}, the expected cost transformer is defined as the least fixed-point of the functional 𝜆𝐹 .[𝜙] • ect[C] (𝐹 ) + [¬𝜙] • 𝑓 . We will see below that this fixed-point is always defined. The transformer ect[while (𝜙) {C}] thus in particular enjoys

ect[while (𝜙) {C}] (𝑓 ) = [𝜙] • ect[C] (ect[while (𝜙) {C}] (𝑓 )) + [¬𝜙] • 𝑓 = [𝜙] • ect[C; while (𝜙) {C}] (𝑓 ) + [¬𝜙] • 𝑓 ,
that is, it evaluates to the cost of unfolding the loop when the loop's guard 𝜙 is satisfied, and otherwise returns the cost 𝑓 , in correspondence to the semantics. Finally, the transformer on non-deterministic choices maximises over expected costs along the two branches.

Well-definedness and Soundness

Before we prove soundness, let us mention that as for the expected cost transformer on PARSs, ect[C] is continuous, and consequently also monotone, in the following sense: Lemma 6.2 (Central Properties of ect[while (𝜙) {C}]).

(1) continuity: ect

[C] (sup 𝑛 ∈N 𝑓 𝑛 ) = sup 𝑛 ∈N ect[C] (𝑓 𝑛 ) for all 𝜔-chains (𝑓 𝑛 ) 𝑛 ∈N ; (2) monotonicity: 𝑓 ≤ 𝑔 =⇒ ect[C] (𝑓 ) ≤ ect[C] (𝑔).
In particular, continuity ensures that in the case for loop C = while (𝜙) {D}, the least fixed point underlying ect[C] is well-defined. Now that we have established that ect[C] (𝑓 ), and hence ecost[C], is well-defined, the remaining objective of this section is to prove that ecost[C] (𝜎) indeed gives the expected cost of running C on store 𝜎. To this end, we show that ect[C] (𝑓 ) (𝜎) coincides with ect[→] (𝑓 ) (𝜎 ⊲ C) defined in terms of the underlying PARS in Section 4. Let us denote by ect

[→] (𝑓 ) (• ⊲ C) the function 𝜆𝜎.ect[→] (𝑓 ) (𝜎 ⊲ C). The correspondence thus becomes ect[C] (𝑓 ) = ect[→] (𝑓 ) (• ⊲ C).
Since the definition of ect[C] (𝑓 ) is guided by the semantics, for most commands C this equality is immediate. The only non-trivial cases are that of composition and loops. The following lemma links the corresponding cases. Lemma 6.3 (Composition and Loop Lemma).

(1) ect

[→] (𝑓 ) (• ⊲ C; D) = ect[→] (ect[→] (𝑓 ) (• ⊲ D)) (• ⊲ C); (2) ect[→] (𝑓 ) (• ⊲ while (𝜙) {C}) = lfp(𝐹 .[𝜙] • ect[→] (𝐹 ) (• ⊲ C) + [¬𝜙] • 𝑓 ).
Note that the right-hand side in ( 2) is well-defined by Lemma 4.4(1). Relying on this auxiliary lemma, our central soundness result follows by a standard induction on C. Theorem 6.4 (Soundness & Completeness). For every command C ∈ Cmd, we have

(1) ect[→] (𝑓 ) (• ⊲ C) = ect[C] (𝑓 ); and consequently (2) ecost[→] (• ⊲ C) = ecost[C].
The theorem thus witnesses that the expected cost transformer of this section gives a sound and complete method for reasoning about the expected cost of programs C.

Upper Invariants

To find closed-forms for the runtime of loops, Kaminski et al. [2016] propose to search for upper invariants, ie. prefix points of the loops characteristic function. The following constitutes a straight forward generalisation of Kaminski et al. [2016, Theorem 3]. For a Boolean expression 𝜙 ∈ BExp, and two cost functions 𝑓 , 𝑔 ∈ C Σ , as before let us denote by 𝜙 ⊨ 𝑓 ≤ 𝑔 that 𝑓 (𝜎) ≤ 𝑔(𝜎) holds for all stores 𝜎 with 𝜙 ⊨ 𝜎. Proposition 6.5 (Upper Invariant). For every

𝐼 ∈ C Σ , 𝜙 ⊨ ect[C] (𝐼 ) ≤ 𝐼 ∧ ¬𝜙 ⊨ 𝑓 ≤ 𝐼 ⇒ ect[while (𝜙) {C}] (𝑓 ) ≤ 𝐼 .

The two premises are equivalent to

[𝜙] • ect[C] (𝐼 ) + [¬𝜙] • 𝑓 ≤ 𝐼 , that is, 𝐼 is a pre-fixed point of the functional 𝜆𝐹 .[𝜙] • ect[C] (𝐹 ) + [¬𝜙]
• 𝑓 ; through which the expected cost transformer of the loop while (𝜙) {C} is defined. The theorem is thus a reformulation of the fact that the least fixed-point is the least among all its pre-fixed points. Via this proposition, the problem of computing ecost[C] can be reduced to a set of inequalities whose solution gives an upper bound on the expected cost of C, compare the discussion at the end of Section 2. Let us illustrate this also on a simple example.

Example 6.6. Reconsider the program C geo from Figure 1b. By Proposition 6.5, the expected cost of the loop within C geo is bounded by 𝐼 subject to the upper invariant conditions:

(i) 𝑏 = 1 ⊨ ect[D] (𝐼 ) ≤ 𝐼 ; and (ii) 𝑏 ≠ 1 ⊨ 0 ≤ 𝐼 , for D the loop's body. Define 𝐼 ≜ [𝑏 = 1] • 2. Unfolding the definition of ect[D] (𝐼 ) yields ect[D] (𝐼 ) = 1 + 1/2 • 𝐼 [𝑏/1, 𝑥/2 • 𝑥] + 1/2 • 𝐼 [𝑏/0, 𝑥/2 • 𝑥] = 1 + 1/2 • [1 = 1] • 2 + 1/2 • [0 = 1] • 2 = 2 .
It is then not difficult to see that the upper invariant conditions hold. Since the variables 𝑏 and 𝑥 are initialized to one in C geo , by Theorem 6.4(2) we conclude ecost[C geo ] = 𝐼 [𝑏/1, 𝑥/1] = 2. Proposition 6.5 suggests the following two stage approach towards an automated cost analysis of a program C via Theorem 6.4. (i) evaluate ecost[C] = ect[C] (0) symbolically and generating a constraint corresponding to the the upper invariant condition; and (ii) synthesise concrete upper invariants via the collection of generated constraints. This is akin to the common approach, where cost functions are specified as linear combination over an (arbitrary but fixed) finite vector of base functions (𝑏 1 , . . . , 𝑏 𝑘 ), itself cost functions, abstracting stores as non-negative numbers. Such cost expressions take the form 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 ), where 𝜅 (𝑟 1 , . . . , 𝑟 𝑘 ) = 𝑖 𝑞 𝑖 • 𝑟 𝑖 for rational (in particular real) numbers 𝑞 𝑖 . Upper invariants then take the form 𝜙 ⊨ ect[C] (𝜿 𝑰 (𝑏 1 , . . . , 𝑏 𝑘 )) ≤ 𝜿 𝑰 (𝑏 1 , . . . , 𝑏 𝑘 ) and ¬𝜙 ⊨ 𝜿 𝒇 (𝑏 1 , . . . , 𝑏 𝑘 ) ≤ 𝜿 𝑰 (𝑏 1 , . . . , 𝑏 𝑘 ).

By treating 𝜅 𝐼 and 𝜅 𝑓 as undetermined, these constraints can be reduced to inequalities over expressions on coefficients in such a way that the resulting set of constraints is eg. amenable to Linear Programming. A solution to these constraints, viz, particularly concrete values for the coefficients 𝑞 𝑖 occurring in 𝜅 𝐼 , then yields a concrete upper invariant. Consequently, an upper bound to the expected cost of while (𝜙) {C} in terms of the base functions ì 𝑏 is inferred.

ALTERNATING EXPECTED COST AND VALUE ANALYSIS

While the calculus developed in the previous section is indeed compositional, the cost analysis via Proposition 6.5, as described above, is not. This is most apparent in the case of nested loops, abstractly represented as follows: while (𝜙) {while (𝜓 ) {C}}. The synthesis of upper invariants 𝐼 and 𝑂 for the inner and outer loops, respectively, wrt. a cost function 𝑓 , is driven by the following inter-dependent constraints, compare the exposition of the trader example in Section 2.

𝜙 ⊨ 𝐼 ≤ 𝑂 ∧ ¬𝜙 ⊨ 𝑓 ≤ 𝑂 ∧ 𝜓 ⊨ ect[C] (𝐼 ) ≤ 𝐼 ∧ ¬𝜓 ⊨ 𝑂 ≤ 𝐼 .
These constraints cannot be considered in isolation. In particular, if we express 𝐼 and 𝑂 in terms of linear combinations 𝜿 𝐼 (𝑏 1 , . . . , 𝑏 𝑘 ) and 𝜿 𝑂 (𝑏 1 , . . . , 𝑏 𝑘 ) of base functions 𝑏 𝑖 , the undetermined combinators 𝜅 𝐼 and 𝜅 𝑂 cannot be synthesised separately. Thus, the analysis degenerates to a whole-program analysis.

As emphasised in Section 3, in the non-probabilistic setting modularity of a cost analysis is facilitated through combining cost analysis with an analysis on how stores evolve through the execution of program parts. In the following, we suit this conceptual simple idea to an expected cost analysis.

The result of a program C, run on an initial store 𝜎, is conceivable as a subdistribution 𝜇 over stores (many, in the case C is also non-deterministic). Then ect[C] (𝑓 ) (𝜎) yields the expected cost of C plus the expected value E 𝜇 (𝑓 ) of the cost function 𝑓 on the distribution of states 𝜇. When 𝑓 coincides with the cost of a continuation, we re-obtain the initial intuition that ect[C] (𝑓 ) yields the cost of running C followed by the corresponding continuation. Otherwise, if the program C is non-deterministic, then C may yield many subdistributions 𝜇. In this case, ect[C] (𝑓 ) accounts for the supremum of the expectations of 𝑓 . We make this correspondence precise. First, we define the expected value transformer evalue[C] of a command C in correspondence to ect[C], ignoring costs. A similar result, albeit restricted to purely probabilistic programs, has been observed by Kaminski et al. [2018, Thm 8.1]. Notice that if C features non-determinism, the right-hand side may overapproximate ect[C] (𝑓 ).

Example 7.3. Consider the non-deterministic program C = {consume(1)} <> {𝑥 𝑥 + 1}. Then ect[C] (𝑓 ) = max(1 + 𝑓 , 𝑓 [𝑥/𝑥 + 1]) ≤ 1 + max(𝑓 , 𝑓 [𝑥/𝑥 + 1]) = ecost[C] + evalue[C] (𝑓 ) .
When 𝑓 depends on the value of 𝑥, the two sides are thus in general not equal.

In this example, we exploit that one branch is costly in terms of consumed resources, while the other one in terms of the expected value of 𝑓 . When C doesn't contain non-deterministic choice, the inequality in Lemma 7.2 can be replaced by an equality.

Consider now a while loop, while (𝜙) {C}. As above, we express the upper invariant 𝐼 as the combination 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 ) of base functions 𝑏 𝑖 . Reconsider the first premise of Proposition 6.5: 𝜙 ⊨ ect[C] (𝜿 (𝑏 1 , . . . , 𝑏 𝑘 )) ≤ 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 ). By Lemma 7.2, this constraint is entailed by

𝜙 ⊨ ecost[C] + evalue[C] (𝜿 (𝑏 1 , . . . , 𝑏 𝑘 )) ≤ 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 ) . , (5)
Moreover, when the upper invariant 𝜅 is linear in all its arguments, it distributes over expectations and hence over the expected value transformer evalue[C]. Consequently (5) becomes

𝜙 ⊨ ecost[C] + 𝜿 (evalue[C] (𝑏 1 ), . . . , evalue[C] (𝑏 𝑘 )) ≤ 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 ) . ( 6
)
First, this decomposes the analysis of the cost of the loop's body C from the analysis of how 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 ) changes in expectation during one iteration. Second, none of the calls to evalue[C] do reference the combinator 𝜅. These can be determined in independence of the analysis of while (𝜙) {C}. We generalise this observation. As usual, we call

𝜅 concave if 𝑝 •𝜅 (ì 𝑟 ) + (1-𝑝) •𝜅 (ì 𝑠) ≤ 𝜅 (𝑝 • ì 𝑟 + (1 -𝑝) • ì 𝑠) (where 0 ≤ 𝑝 ≤ 1) and (weakly) monotone if ì 𝑟 ≤ ì 𝑠 implies 𝜅 (ì 𝑟 ) ≤ 𝜅 (ì 𝑠).
Together, the two conditions yield the following sufficient criterion to distribute 𝜅 over expectations, which can be proven by a standard induction on evalue[C] (𝑓 ) = evalue[C] (𝑓 ).

Lemma 7.4 (Distribute over Expected Values). Suppose 𝜅 :

C 𝑘 → C is monotone. Further- more, suppose 𝜅 is concave if the command C is probabilistic. Then evalue[C] (𝜿 (𝑏 1 , . . . , 𝑏 𝑘 )) ≤ 𝜿 (evalue[C] (𝑏 1 ), . . . , evalue[C] (𝑏 𝑘 )).
Note that concavity is only needed to distribute 𝜅 over the expected value given by probabilistic statements, that is, probabilistic assignments from non-dirac distributions. The above lemmas in conjunction with Proposition 6.5 yields the main result of this section.

𝜿 ( ì 𝑏) ← ecost[E] ì 𝑏 ′ ← foreach 𝑏 ∈ ì 𝑏: evalue[D] (𝑏) return ecost[D] + 𝜿 ( ì 𝑏 ′ ) case while (𝜙) {D}: 𝑔 ← ecost[D] ì 𝑏 ← SelectBases(𝜙, 𝑔) ì 𝑏 ′ ← foreach 𝑏 ∈ ì 𝑏: evalue[D] (𝑏) 𝜅 ← LinearTemplate(length( ì 𝑏)) 𝜃 ← Solve(𝜙 ⊨ 𝑔 + 𝜿 ( ì 𝑏 ′ ) ≤ 𝜿 ( ì 𝑏)) return 𝜃 (𝜿) ( ì 𝑏) default: return SymbolicCost(C) function evalue[C](𝑓 ) switch C do case D; E where D contains a loop: 𝜿 ( ì 𝑏) ← evalue[E] ì 𝑏 ′ ← foreach 𝑏 ∈ ì 𝑏: evalue[D] (𝑏) return 𝜿 ( ì 𝑏 ′ ) case while (𝜙) {D}: ì 𝑏 ← SelectBases(𝜙, 𝑓 ) ì 𝑏 ′ ← foreach 𝑏 ∈ ì 𝑏: evalue[D] (𝑏) 𝜅 ← LinearTemplate(length( ì 𝑏)) 𝜃 ← Solve(𝜙 ⊨ 𝜿 ( ì 𝑏 ′ ) ≤ 𝜿 ( ì 𝑏) ∧ ¬𝜙 ⊨ 𝑓 ≤ 𝜿 ( ì 𝑏)) return 𝜃 (𝜿)( ì 𝑏) case 𝑥 𝑑: return Expectation(𝑑, 𝜆𝑣.𝑓 [𝑥/𝑣]) default: return SymbolicValue(C, 𝑓 )

IMPLEMENTATION

In this section, we give an overview of the implementation of our methodology within our tool eco-imp. The core of our tool is given by the algorithms ecost[C] and evalue[C] outlined in Figure 5, computing for a given program C and cost function 𝑓 , an upper bound to ecost[C] and evalue[C] (𝑓 ), respectively. As for the transformers, the two algorithms are structurally similar.

In the majority of cases, the default branch of the algorithm is executed and the implementation symbolically executes the corresponding transformer from Figure 3. Conclusively, a precise bounds is computed in these cases. Exceptions to this are the cases of loops and assignments, detailed below. Here, possibly imprecise upper bounds are derived. Due to monotonicity (Lemma 4.4(2)) soundness of the overall algorithm remains intact.

Sequential composition. For a command C = D; E, our implementation relies on Theorem 7.5, except when D does not contain a loop. In this case, the algorithms proceed by unfolding according to the rules in Figure 5 and (recursion on D). Here, modularity is not necessary; the straight-line program D can be analysed directly.

While loops. The main novel aspect from which our implementation derives its strength lies in the treatments of loops, providing an almost literal implementation of Theorem 7.5, following to recipe given on page 17. The subprocedure SelectBases, outlined below, selects a vector of base functions ì 𝑏 from the loops guard 𝜙, and the recursively computed cost 𝑔 of the loop's body or the cost function 𝑓 . For each such base function 𝑏, an upper bound 𝑏 ′ to its expectation evalue[C] (𝑏) is computed and a linear template 𝜅 ( ì 𝑥) = 𝑖 𝑞 𝑖 • 𝑥 𝑖 with undetermined coefficients 𝑞 𝑖 ∈ R ≥0 is prepared. Based on these ingredients, the subprocedure Solve is applied to the constraint dictated by Theorem 7.5. Should this procedure establish a solution 𝜃 , ie. an assignment to the undetermined coefficients 𝑞 𝑖 underlying 𝜅 that validates the supplied constraint, the instantiated cost function

𝜃 (𝜿) ( ì 𝑏) = 𝑖 𝜃 (𝑞 𝑖 ) • ì 𝑏 𝑖 is returned.
The dedicated constraint solver underlying the procedure Solve is detailed below in Section 8.1.

Selection of base functions. Our implementation selects a set of candidate base functions ì 𝑏 as a linear or non-linear combination of base functions ì 𝑏 𝜙 , ì 𝑏 𝑔 and ì 𝑏 𝑓 extracted from the loop guard 𝜙, the expected cost of the loop body 𝑔 and the continuation 𝑓 , loosely following the heuristics of [START_REF] Sinn | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis[END_REF]. Specifically, for a loop guard containing 𝑒 1 ≤ 𝑒 2 we take ⟨𝑒 2 -𝑒 1 + 1⟩ ∈ ì 𝑏 𝜙 . Further, ì 𝑏 𝑔 and ì 𝑏 𝑓 contain all maximal non-max subexpressions of 𝑔 and 𝑓 , respectively. Given ì 𝑏 𝜙 , ì 𝑏 𝑔 and ì 𝑏 𝑓 we then construct different linear and non-linear combinations, such as ì

𝑏 = ì 𝑏 𝜙 + ì 𝑏 𝑔 + ì 𝑏 𝑓 and ì 𝑏 = ì 𝑏 𝜙 × ì 𝑏 𝑔 + ì
𝑏 𝑓 where × and + extend multiplication and addition to sets of base functions element-wise. Since base functions can be extracted from a given context rather than the whole program, the number of base functions is usually low. This is one crucial aspect to the efficiency of our algorithm. The prototype implements caching and backtracking to test different base functions. In particular, non-linear base functions are employed only if the linear ones fail. This is another crucial aspect to efficiency, in contrast to a monolithic procedure. Constraint solving over linear arithmetical expressions is significantly more efficient; non-linear expressions are employed only in the analysis of those program fragments where necessary.

Assignments. Our implementation supports, on the one hand, assignments with sampling from finite, discrete distributions, of the form 𝑑 (𝜎) = {{𝑝 𝑖 (𝜎) : 𝑒 𝑖 (𝜎)}} 0≤𝑖 ≤𝑘 for a fixed constant 𝑘 and 𝑝 𝑖 = 𝑒 𝑖 /𝑓 𝑖 , such as {{ 𝑖 + 1 /10 : 𝑥 + 2𝑖}} 0≤𝑖 ≤9 . Noteworthy, probabilities of probabilistic branches are not necessarily constant. In this case, the expected cost of a probabilistic assignment 𝑥 𝑑 is given by ect

[𝑥 𝑑] (𝑓 ) (𝜎) = 1≤𝑖 ≤𝑘 𝑝 𝑖 (𝜎) • 𝑓 [𝑥/𝑒 𝑖 (𝜎)
] . Thus our system encompasses a variety of standard distributions where probabilistic branching is static, in the sense that the degree does not depend on program variables. Thus our implementation supports a variety of standard distributions, noteworthy sampling from uniform distributions with bounded support, Bernoulli, binomial and hypergeometric distributions.

On the other hand, we are able to natively support dynamic probabilistic branching, facilitated by our constraint solver for Upper Invariants. In particular, we have added support for sampling uniform distributions Uniform(𝑒 1 , 𝑒 2 ) for 𝑒 1 ≤ 𝑒 2 . This, for example, is crucial to represent the Coupon Collector's problem properly. Note, that in this case

ect[𝑥 𝑑] (𝑓 ) = [𝑒 1 ≤ 𝑒 2 ] • 𝑒 2 𝑖=𝑒 1 𝑓 [𝑥/𝑖] /(𝑒 2 -𝑒 1 + 1) .
To find a closed form for the bounded sum 𝑒 2 𝑖=𝑒 1 𝑓 [𝑥/𝑖], our implementation seeks for an upper bound 𝜿 ( ì 𝑏) subject to the constraint

𝑒 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑒 2 ⊨ 𝑓 [𝑥/𝑖] + 𝜿 ( ì 𝑏 [𝑖/𝑖 + 1]) ≤ 𝜿 ( ì 𝑏).

Constraint Solving Mechanism

In this section, we highlight the constraint solving mechanism as implemented in our prototype eco-imp, consisting of two stages: the first translates constraints over costs (with undetermined coefficients) to tests of non-negativity over polynomials; the second stage then treats this syntactically simpler form of constraints. First, we fix two syntactic categories of (non-linear) integer expressions Exp and cost expressions CExp as follows.

Exp ∋ 𝑒, 𝑓 ::= 𝒊 | 𝑥 | 𝑒 + 𝑓 | 𝑒 -𝑓 | 𝑒 • 𝑓 CExp ∋ 𝑐, 𝑑 ::= 𝑒/𝑓 | [𝜙] • 𝑐 | 𝑐 + 𝑑 | max(𝑐, 𝑑) .
In Exp, we use integer variables 𝑥 ∈ Var to denote cost functions 𝜆𝜎.𝜎 (𝑥). Cost expressions denote fractions over integer expressions, closed under guards, sum and maximum. Furthermore, we restrict BExp to Boolean formulas over atoms 𝑒 ≤ 𝑓 , in disjunctive normal form. This still permits the usual comparison operators over integer expressions, eg., 𝑒 < 𝑓 can be represented as 𝑒 + 1 ≤ 𝑓 or 𝑒 = 𝑓 as 𝑒 ≤ 𝑓 ∧ 𝑓 ≤ 𝑒. We tacitly employ such equalities below. When denoting cost expressions, we usually write 𝑒 instead of 𝑒/1. Base functions are given as a combination of expressions ⟨𝑒⟩ ≜ [0 ≤ 𝑒] • 𝑒. Not every cost expression is an expectation in C Σ though, as cost expression need not be well-formed.

We say 𝑐 ∈ CExp is well-formed wrt. store 𝜎 ∈ Σ if (i) 𝑐 = 𝑒/𝑓 such that 𝑒 (𝜎) ≥ 0 and 𝑓 (𝜎) > 0; (ii) 𝑐 = [𝜙] • 𝑑 such that 𝜎 ⊨ 𝜙 and 𝑑 is well-formed wrt. 𝜎; (iii) 𝑐 = 𝑐 1 + 𝑐 2 or 𝑐 = max(𝑐 1 , 𝑐 2 ) such Constraint solving. Given a constraint 𝜙 ⊨ 𝑐 ≤ 𝑑, the simplification rules of Figure 6 can be seen as a way to eliminate max, guards, division and disjunctions. Thus, they translate constraints over cost-expressions to a set of equivalent constraints over integer-valued expressions. Wlog., these constraints are of the form 𝑖 0 ≤ 𝑒 𝑖 ⊨ 0 ≤ 𝑒, by employing additionally the identity 𝑒 ≤ 𝑓 ⇔ 0 ≤ 𝑓 -𝑒. Any expression 𝑒 can be understood as a polynomial 𝑝 ( ì 𝑥) in the program variables ì 𝑥. Validity of constraints of the above form becomes representable as a test of nonnegativity. To this end, we make use of known approximations for certifying non-negativity of polynomial expressions, cf. [START_REF] Chatterjee | Termination Analysis of Probabilistic Programs Through Positivstellensatz's[END_REF][START_REF] Fuhs | SAT Solving for Termination Analysis with Polynomial Interpretations[END_REF][START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]. Let 𝑝 and 𝑝 1⩽𝑖 ⩽𝑚 , respectively, denote real-valued polynomials over the integers. The following proposition expresses a (gross) simplification of Handelman's theorem [START_REF] Handelman | Representing Polynomials by Positive Linear Functions on Compact Convex Polyhedra[END_REF]], which turns out to be quite effective in our context. Proposition 8.3. Let 𝑝 ( ì 𝑥) be a real-valued polynomial over the integers. Suppose there exists multi-indices (𝑖 1 , . . . , 𝑖 𝑚 ) ∈ N 𝑚 , polynomials 𝑝 1⩽𝑖 ⩽𝑚 : : Z 𝑛 → R and 𝑐 (𝑖 1 ,...,𝑖 𝑚 ) ∈ R ≥0 so that

𝑝 ( ì 𝑥) = (𝑖 1 ,...,𝑖 𝑚 ) ∈ N 𝑚 𝑐 (𝑖 1 ,...,𝑖 𝑚 ) • 𝑝 𝑖 1 1 ( ì 𝑥) • • • 𝑝 𝑖 𝑚 𝑚 ( ì 𝑥). Then 𝑚 𝑖=1 0 ≤ 𝑝 𝑖 ( ì 𝑥) implies 0 ≤ 𝑝 ( ì 𝑥).
Recall that overall, we are concerned with synthesising concrete values for the undetermined 𝑞 𝑖 ∈ R ≥0 stemming from templates 𝜅 ( ì 𝑏) ≜ 𝑞 𝑖 • 𝑏 𝑖 , so that all the generated constraints become valid. By reducing inequalities over polynomials to inequalities of the constituting coefficients and fixing indices 𝐼 , via Proposition 8.3 this synthesis can be formulated as a satisfiability problem over arithmetical expressions over variables 𝑞 𝑖 ≥ 0. In turn, this problem can be solved with an off-the-shelf SMT solver supporting QF_NRA. We illustrate this with our running example.

Example 8.4 (Example 8.2 continued). Unfolding the first premise 𝑏 = 1 to 0 ≤ 𝑏 -1 ∧ 0 ≤ 1 -𝑏 as discussed above, the final remaining constraint (7) from the running example simplifies to

0 ≤ 𝑏 -1 ∧ 0 ≤ 1 -𝑏 ∧ 0 ≤ 𝑏 =⇒ 0 ≤ 2 • 𝑞 • 𝑏 -𝑞 -2 .
We restrict to the multi-indices (1, 0, 0), (0, 1, 0) and (0, 0, 1), that is, we intend to express 2•𝑞•𝑏-𝑞-2 as a linear combination of the three functions 𝑏 -1, 1 -𝑏 and 𝑏, respectively, represent the conjuncts in the assumption. Proposition 8.3 yields the following obligation 2 • 𝑞 • 𝑏 -𝑞 -2 = 𝑐 (1,0,0) • (𝑏 -1) + 𝑐 (0,1,0) • (1 -𝑏) + 𝑐 (0,0,1) • 𝑏 , which, subject to the side-condition 0 ≤ 𝑞, holds with 𝑞 = 2, 𝑐 (1,0,0) = 4 and 𝑐 (0,1,0) = 𝑐 (0,0,1) = 0. Theorem 8.1 now translates this solution to a solution 𝜅 (𝑥) ≜ 2 • 𝑥 for the initial constraint in Example 8.2. The constraint solving mechanism established this way thus derives the (optimal) bound given by hand in Section 7.1.

Experimental Evaluation

To assess our implementation, we have conducted an experimental evaluation of eco-imp on the benchmarks of [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF][START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]]. We have elided example recursive from [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF] as we have not yet incorporated support for recursive definitions into eco-imp. This is planned for a future release of the prototype. The prototype of [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF] can also deal with some programs featuring negative costs, corresponding examples have been also removed from our testbed. We have extended the resulting testbed with the various examples from this work: In Table 2 (d) we list the program from Figure 1c as coupons-n and also instantiate 𝑛 to constants 10, 50 and 100. Similar, the example from Figure 1a has been parameterised in the number of shares, denoted as trader-n, respectively. Examples nest-i perform 𝑖 nested random walks. The example bridge performs an unbiased random walk within an interval [𝑎, 𝑏].

In Tables 1 and2, we compare our implementation (column A) to the prototypes Absynth of [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF] (column B) and [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF] (column C). On some of the examples, the tool Absynth does not provide an upper bound in a reasonable amount of time; as timeout we use 5 minutes; corresponding examples have been marked with -. Wrt. the tool by [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF], we reproduce the experimental evaluation reported in [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF] and slightly extend them by results on the example bridge. Further, we provide timing information on the accessible part of the benchmark in [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF]]. However, the tool requires extensive manual invariant annotations and various examples were not amendable to an experimental evaluation. Corresponding rows are marked with -. Execution times are obtained on an Intel i7-7600U CPU with 2.8GHz and 16GB RAM.

Precision. The bounds reported in Table 1 and 2 are to a great extent overlapping with those inferred by the Absynth tool from [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF] and, where available, by the prototype of [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]. In particular, the bounds for all but three example are on the same order of magnitude. In example prnes, eco-imp infers a quadratic rather than a linear bound. This example uses nondeterminism in a way non-beneficial to a separated cost and value analysis, similar to Example 7.3. Concerning example C4B_t30 our tool infers an asymptotic optimal linear bound, while Absynth yields a quadratic one. Whereas Absynth uses a combination of linear and non-linear base functions, our backtracking-based algorithm for selecting base functions succeeds on this example using purely linear base functions. A similar observation carries over to example queueing-network (depicted in Figure 4a). While the bound derived by eco-imp equals the one from [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF] upto a constant, it is significantly more precise than the bound obtained by the Absynth tool.2 These results are remarkable, as the precision of Absynth is outstanding. It is well-understood that a modular analysis, like ours, often comes with the drawback of less precision. Noteworthy is our analysis of rejection_sampling depicted in Figure 4b, due to Kaminski et al. [2016], where eco-imp's precision equals the measured expected cost, cf. Figure 7.

Speed. Across the benchmark, where we have annotated the speedup in parenthesis besides execution times, eco-imp outperforms the other tools. While our tool achieves already significant speedups in the linear benchmark from [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF], the gains are most pronounced in examples with nested loops and non-linear bounds (Table 2 (b)-(c)). The only exception to this assessment are the examples queueing-network and prnes, both single-loop programs. Concerning the former, our tool performs several backtracking steps to derived the asymptotic optimal bound mentioned above. Also the use of large constants within the SMT-solving stage explains the longer execution time. Concerning prnes, while our tool performs significantly faster than the implementation [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]. Note however that differences in execution times are even stronger pronounced.

Scalability. In Figure 8, we show the results of eco-imp on parametric examples in comparison to the prototypes of [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF] and [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]. The left figure plots execution times in relation to the number of nested loops. Similarly, the figure on the right depicts the effects on extending the number of shares in C trader . See also Table 1 (d). Our results are competitive and highlight sharply the prime benefit of our implementation, viz, its modularity. As clear indication of the scalability of our tool, the execution times of eco-imp are barely visible in the charts in contrast to runtime of existing tools, if the tools can handle the examples at all. Deterministic Programs. Finally, we also point out that eco-imp is competitive with regards to automated complexity analysis tools on deterministic programs. For illustration, we complemented the experimental evaluation from [START_REF] Carbonneaux | Compositional Certified Resource Bounds[END_REF], comparing their tools 𝐶 4 𝐵, KoAT [START_REF] Brockschmidt | Alternating Runtime and Size Complexity Analysis of Integer Programs[END_REF], Rank [START_REF] Alias | Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs[END_REF] and Speed [START_REF] Gulwani | SPEED: Precise and Efficient Static Estimation of Program Computational Complexity[END_REF], on the 34 deterministic integer programs from their benchmark.3 Here, 𝐶 4 𝐵 outperforms the mentioned tools by a great margin, as 𝐶 4 𝐵 can solve at least 10 more examples in each comparison. In comparison eco-imp can derive bounds for all examples but t62. However, since 𝐶 4 𝐵 is constrained to linear bounds and consequently the testbed features only examples with linear cost, eco-imp cannot benefit from its modularity on this benchmark.

RELATED WORKS

We restrict our focus on related work concerned with the analysis of bounded expected resource usage of (non-deterministic) probabilistic imperative programs.

Very briefly, we refer to the extensive literature of analysis methods for (bounded) or almost-sure termination for (non-deterministic) probabilistic programs that have been introduced in the last years. These have been provided in the form of abstract interpretations [START_REF] Chakarov | Expectation Invariants for Probabilistic Program Loops as Fixed Points[END_REF][START_REF] Monniaux | An Abstract Analysis of the Probabilistic Termination of Programs[END_REF]; martingales, eg., ranking super-martingales [START_REF] Agrawal | Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs[END_REF][START_REF] Brázdil | Runtime Analysis of Probabilistic Programs with Unbounded Recursion[END_REF][START_REF] Chakarov | Probabilistic Program Analysis with Martingales[END_REF][START_REF] Chatterjee | Termination Analysis of Probabilistic Programs Through Positivstellensatz's[END_REF]Chatterjee et al. , 2017a,b;,b;[START_REF] Esparza | Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances[END_REF][START_REF] Takisaka | Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs[END_REF][START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]; or equivalently Lyapunov ranking functions [START_REF] Bournez | Proving Positive Almost-Sure Termination[END_REF]; model checking [START_REF] Katoen | The Probabilistic Model Checking Landscape[END_REF]]; program logics [START_REF] Kaminski | Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms[END_REF][START_REF] Mciver | A New Proof Rule for Almost-sure Termination[END_REF][START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF][START_REF] Wang | PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs[END_REF]; proof assistants [START_REF] Barthe | Formal Certification of Code-based Cryptographic Proofs[END_REF]; recurrence relations [START_REF] Sedgewick | An Introduction to the Analysis of Algorithms[END_REF]; methods based on program analysis [START_REF] Celiku | Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs[END_REF][START_REF] Katoen | Linear-Invariant Generation for Probabilistic Programs: -Automated Support for Proof-Based Methods[END_REF][START_REF] Kozen | A Probabilistic PDL[END_REF]; or symbolic inference [START_REF] Gehr | PSI: Exact Symbolic Inference for Probabilistic Programs[END_REF]; and finally type systems [START_REF] Avanzini | Type-Based Complexity Analysis of Probabilistic Functional Programs[END_REF][START_REF] Breuvart | On Intersection Types and Probabilistic Lambda Calculi[END_REF].

Probabilistic resource analysis. Kaminski et al. generalises Dijkstra's wp-calculus to an expected runtime transformer ert. The obtained resource analysis expresses is smoothly applicable in a variety of case studies, in particular to the program C coupons . Our expected cost transformer constitutes a generalisation of the ert-calculus. In particular, note that evalue[C] coincides with the weakest precondition transformer wp[C] by [START_REF] Kaminski | Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms[END_REF] on fully probabilistic programs, ie. those without non-deterministic choice. In the presence of mixed-sign, unbounded updates, the ertcalculus has been extended by exploiting an absolute convergence criterion, cf. [START_REF] Kaminski | A Weakest Pre-expectation Semantics for Mixed-sign Expectations[END_REF]. A bulk of research in the literature concentrates on specific forms of martingales or Lyapunov ranking functions. Central to our work is the observation, that these approaches can be suited to a variety of quantitative program properties, see [START_REF] Takisaka | Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs[END_REF] for an overview. We also mention Chatterjee et al. [2017a] where inference procedures to solve recurrences stemming from probabilistic programs are proposed.

Automation. Notably, the Absynth prototype by [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF], implements a weakest precondition calculus for reasoning about expected costs. Our tool eco-imp generalises this implementation and provides a modular and thus a more efficient and scalable alternative. Also martingale based techniques have been implemented, eg., by [START_REF] Chatterjee | Termination Analysis of Probabilistic Programs Through Positivstellensatz's[END_REF] and more recently by [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]. A novelty of [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF] is the established polynomial-time analysis and incorporation of a cost model which allows for unbounded negative and positive costs, as long as the variable updated are bounded, while demands (almost-sure) termination as prerequisite. Exploiting the approach by [START_REF] Kaminski | A Weakest Pre-expectation Semantics for Mixed-sign Expectations[END_REF], we expect the extensibility of our approach to negative costs as well. Our work overcomes the whole-program analysis established by these tools and provides a modular and scalable framework. Further, dynamic distributions are supported. As vindicated by the above provided experimental assessment, modularity significantly speeds up the analysis (see Section 8).

CONCLUSION

We established an automated expected resource analysis of non-deterministic, probabilistic imperative programs. As indicated by the formal hardness of this problem by [START_REF] Kaminski | On the Hardness of Almost-Sure Termination[END_REF], this is challenging. While previous approaches only feature a whole-program analysis to synthesis precise cost functions, we present a novel modular framework for the automated analysis. Our prototype eco-imp is more efficient and scales better than existing tools. Its algorithmic superiority is eg. attested by the fact that the motivating example by [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF] can be handled three orders of magnitudes faster.

To establish these highlights, (i) we exploit a novel operational semantics in terms of weighted probabilistic abstract reduction systems Avanzini et al. [2020]; Avanzini and Yamada [2020]; (ii) we establish modularity by generalising a weakest precondition calculus pioneered by [START_REF] Kaminski | Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms[END_REF] to an alternating expected cost and value analysis; and (iii) painstaking attention to detail in the implementation with a focus on efficiency.

Future theoretical advances are needed to incorporate the treatment of presence of mixed-sign, unbounded updates, in order to properly deal with negative costs. Practical goals are the extension of the synthesis capabilities of our prototype towards lower bounds (following [START_REF] Ngo | Verifying and Synthesizing Constant-Resource Implementations with Types[END_REF]) and further, real-world examples.

Table 1. Automatically derived bounds on the expected cost and execution times via eco-imp (A), [START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF]] (B), and [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]

  Fig. 1. Motivating Examples.

  [𝑥 𝑑] (𝑓 ) ≜ 𝜆𝜎. 𝑖 ∈Z 𝑝 𝑖 • 𝑓 (𝜎 [𝑥/𝑖]). Ie. the expected cost is set as the mean value of 𝑓 on stores 𝜎 with 𝑥 updated by the sampled value 𝑖. Expected cost of two sequentially composed commands C; D becomes expressible via composition of the transformer: ect[C; D] ≜ ect[C] • ect[D]. For straight line programs, expected costs can thus be derived simply by unfolding definitions. On the other hand, the expected cost of a loop while (𝜙) {C}, wrt. the cost of a continuation 𝑓 , is definable as 𝜙 ⊨ ect[while (𝜙) {C}] (𝑓 ) = ect[C; while (𝜙) {C}] (𝑓 ) ¬𝜙 ⊨ ect[while (𝜙) {C}] (𝑓 ) = 𝑓 , (2)

  Here, ecost[C] amounts to the cost of executing the loop's body C once; evalue[C] (𝑏 𝑖 ) gives the mean value of measures 𝑏 𝑖 after executing C. In other words, evalue[C] (𝑏 𝑖 ) amounts to the expected value of the base function 𝑏 𝑖 on the distribution of final states obtained from executing the loop's body C. For instance, evalue

  Definition 4.3 (Expected Cost Transformer for PARSs). The expected cost transformer ect[→] : C 𝐴 → C 𝐴 for a PARS → is given by ect[→] (𝑓 ) ≜ lfp( 𝜒 𝑓 ), where the functional 𝜒 𝑓 : C 𝐴 → C 𝐴 is defined as

  Lemma 4.4 (Central Properties of ect[→]).(1) continuity: ect[→] (sup 𝑛 ∈N 𝑓 𝑛 ) = sup 𝑛 ∈N ect[→] (𝑓 𝑛 ) for all 𝜔-chains (𝑓 𝑛 ) 𝑛 ∈N ; (2) monotonicity: 𝑓 ≤ 𝑔 =⇒ ect[→] (𝑓 ) ≤ ect[→] (𝑔).A standard induction reveals that 𝜒 𝑛 𝑓 (0) = 𝜆𝑎. sup{𝑤 | 𝑎 𝑤 -→ → 𝑛 𝜇}, where 𝜒 𝑛 𝑓 denotes the 𝑛-fold composition of 𝜒 𝑓 . Consequently, the next result follows by Kleene's Fixed-Point Theorem. Theorem 4.5 (Expected Cost via Cost Transformer). ecost[→] = ect[→] (0) .

Fig. 3 .

 3 Fig. 3. Definition of expected cost transformer ect[C] and expected value function evalue[C]. Notice that their definition coincides up to the case C = consume(𝑒).

  Definition 7.1(Expected Value Transformer). The expected value transformer evalue[C] : C Σ → C Σ for commands C is defined through the rules given in the third column in Figure3.Concerning the program C geo from Figure1bfor instance, we obtain evalue[C geo ] (𝑓 ) = 𝜆𝜎. ∞ 𝑖=0 1 /2 𝑖 • 𝑓 ({𝑏 ↦ → 1, 𝑥 ↦ → 2 𝑖+1 }). Note that evalue[C] (𝑓 ) = ect[costFree(C)] (𝑓 )holds, where the cost-free program costFree(C) is obtained from C by dropping all cost annotations consume(𝑒). Particularly, Proposition 6.5 remains intact if we substitute evalue[•] for ect[•]. The next lemma establishes a separation of the expected cost and value computation, which underlies the expected cost transformer ect[C]. Lemma 7.2 (Separating Expected Cost and Value). ect[C] (𝑓 ) ≤ ecost[C] + evalue[C] (𝑓 ) .

  Theorem 7.5 (Modular Upper-Invariants). Let C and 𝜅 be as in Lemma 7.4. Then 1. 𝜙 ⊨ ecost[C] + 𝜿 (evalue[C] (𝑏 1 ), . . . , evalue[C] (𝑏 𝑘 )) ≤ 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 ) ⇒ ecost[while (𝜙) {C}] ≤ 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 ); and function ecost[C] switch C do case D; E where D contains a loop:

Fig. 5 .

 5 Fig. 5. Pseudocode detailing cost-inference.

Fig. 7 .

 7 Fig. 7. Comparison of inferred expected cost and measured expected cost using a sample size of 10000, for (from left to right) examples (a) trader 2, (b) coupons and (c) rejection_sampling. The box plot depicts the minimum, lower-and upper quartile, and maximum cost measured. For trader we fix 𝑚𝑖𝑛 to 100.

Fig. 8 .

 8 Fig. 8. Execution times of the three analysers on parametric examples (a) nest-i consisting of 𝑖 nested loops, each performing a biased random walk and (b) trader-n from Figure 1a with number of shares fixed to 𝑛.

  Program. Lang., Vol. 4, No. OOPSLA, Article 172. Publication date: November 2020.

  over multidistributions M (𝐴). These are countable multisets {{𝑝 𝑖 : 𝑎 𝑖 }} 𝑖 ∈𝐼 over pairs 𝑝 𝑖 : 𝑎 𝑖 of probabilities 0 < 𝑝 𝑖 ≤ 1 and objects 𝑎 𝑖 ∈ 𝐴 with 𝑖 ∈𝐼 𝑝 𝑖 ≤ 1. Multidistributions are denoted by 𝜇, 𝜈, . . . . The notion of expectation of a function 𝑓 : 𝐴 → R ∞ ≥0 is extended to multidistributions 𝜇 in the natural way: E 𝜇 (𝑓 ) ≜ (𝑝:𝑎) ∈𝜇 𝑝 • 𝑓 (𝑎). Finally, the reduction relation is inductively find by

  In the last rule, 𝑤 = 𝑖 ∈𝐼 𝑝 𝑖 • 𝑤 𝑖 and 𝑝 𝑖 > 0 are probabilities with 𝑖 ∈𝐼 𝑝 𝑖 ≤ 1. Scalar multiplication is performed component-wise on probabilities, refers to the usual notion of multiset union. Ie. 𝜇 𝑤 -→ → 𝜈 indicates that some elements 𝑎 𝑖 with associated probability 𝑝 𝑖 are replaced by 𝛿 𝑖 , re-weighted with probability 𝑝 𝑖 , according to rules 𝑎 𝑖 𝑤 𝑖 --→ 𝛿 𝑖 . The overall cost 𝑤 is given by the sum 𝑝 𝑖 • 𝑤 𝑖 , corresponding to the expected cost of the single reduction step 𝜇 𝑤 -→ → 𝜈. Eg. the PARS --→ geo gives rise to the reduction

  ofWang et al., it is slightly less performant than Absynth. Due to non-determinism underlying the example, as outlined above, eco-imp has to resort to non-linear bounding functions, making the constraint solving stage more involved.This assessment remains intact when comparing to the implementation of Wang et al. on the subset of examples treated by

Table 2 .

 2 Automatically derived bounds on the expected cost and execution times via eco-imp (A),[START_REF] Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF]] (B), and[START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF]] (C).

	Runtime in secs. (speedup)	C A B C		-0.006 0.045 (7) -	2(𝑛 -𝑥) 0.001 0.019 (19) 6.155 (6155)	-0.002 0.052 (26) -		-0.029 0.809 (28) -	-0.013 2.190 (168) -	3.125𝑥 2 + 5.31𝑥 0.007 0.261 (37) 8.626 (1232)	0.5𝑥 2 + 2.5𝑥 0.007 0.150 (21) 8.480 (1211)	-0.040 1.567 (39) -	-0.015 0.561 (37) -	𝑛 2 + 𝑛 0.006 0.092 (15) 9.374 (1562)	10(𝑝 2 -𝑚 2 -2𝑝 + 4𝑚 + 1) 0.030 119.464 (3982) 10.420 (347)		+ 1.73𝑏 2 -31.45𝑎 + 126.52 1.760 1.73𝑎 2 -3.46𝑎𝑏 + 31.45𝑎 -11.621 (7)	0.049𝑛 2.215 1.286 (1) 78.191 (35)		𝑎𝑥 + 𝑏𝑥 + 𝑎 -𝑥 2 -𝑏 -𝑎𝑏 + 1 0.005 -8.173 (1635)
	Inferred Bound	Program A B	(a) linear benchmark from [Ngo et al. 2018] (continued)	2 ⟨𝑥 + 1⟩ simple_game 2 ⟨𝑥 + 1⟩	2⟨𝑛 -𝑥 ⟩ sprdwalk 2⟨𝑛 -𝑥 ⟩	7.5⟨𝑛⟩ trapped_miner 15 /2⟨𝑛⟩	(b) Non-linear benchmark from [Ngo et al. 2018]	⟨𝑤 ⟩ + 18⟨𝑀 ⟩ ⟨𝑁 ⟩ + 9⟨𝑁 ⟩ + 3⟨𝑦 ⟩ complex ⟨𝑤 ⟩ + 18⟨𝑀 • 𝑁 + 𝑁 ⟩ ⟨𝑁 ⟩ + 3⟨𝑦 ⟩	2⟨𝑚⟩ ⟨𝑛⟩ + 4⟨𝑛⟩ multirace ⟨𝑚 + 1⟩ ⟨𝑛⟩	7.5 ⟨𝑥 ⟩ + 4.5⟨𝑥 ⟩ 2 pol04 15 /2⟨𝑥 ⟩ + 9 /2⟨𝑥 ⟩ 2	⟨𝑥 ⟩ + ⟨𝑥 ⟩ 2 pol05 3 /4⟨𝑥 ⟩ + 3 /2⟨𝑥 ⟩ 2	+ ⟨𝑝 -𝑚⟩ ⟨𝑝 ⟩ + ⟨𝑝 -𝑚⟩ 2 0.5⟨𝑝 -𝑚⟩ pol06 ⟨1 + 𝑚⟩ ⟨1 + 𝑝 ⟩ + ⟨𝑝 -𝑚⟩ ⟨1 + 𝑝 ⟩	1.5⟨𝑛 -1⟩ ⟨𝑛 -2⟩ pol07 3 /2⟨𝑛 -1⟩ 2	3⟨𝑛⟩ 2 rdbub 3⟨𝑛⟩ 2	+ 10⟨𝑝 -𝑚⟩ 20⟨𝑚⟩ ⟨𝑝 -𝑚⟩ trader(-20) 10⟨𝑝 -𝑚⟩ 2 + 20⟨1 + 𝑚⟩ ⟨𝑝 -𝑚⟩ + 10⟨𝑝 -𝑚⟩ 2	(c) additional examples from [Wang et al. 2019]	-2drobot 1 /2 ⟨1 + 𝑎 -𝑏 ⟩ ⟨𝑎 -𝑏 ⟩ ⟩ 2 + 2⟨1 + 𝑎 -𝑏 + 1267 /18⟨6 + 𝑎 -𝑏 ⟩	1⟩ 2 1⟩ + 0.014⟨𝑛 + 0.05⟨𝑛 + queueing-network 1.132.981 /244 /243 + 125 1⟩ + 125 7.411.500 ⟨𝑛 +	(d) examples from this work	-⟩ ⟨𝑏 -𝑥 ⟨𝑥 -𝑎⟩ bridge	nest-1

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 172. Publication date: November 2020.

When C features also non-deterministic choice, as we do later on in this work, this equality turns into an inequality, see Lemma 7.2. Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 172. Publication date: November

Note that the bound reported in[START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF] and also produced by their tool contains terms depending on constant values 𝑙1, 𝑙2, and 𝑖, representing the length of the queues and the loop counter, respectively. In our presentation, however, we have set these values to their initial values to ease comparability.Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 172. Publication date: November 2020.

Full experimental evidence is available from the homepage of eco-imp.Proc. ACM Program. Lang., Vol.

4, No. OOPSLA, Article 172. Publication date: November 2020.

* This work is partially supported by the French ANR: "Agence National de Recherche" under Grant "PPS: Probabilistic Program Semantics", No. ANR-19-CE48-0014, and the Inria associated team TC(Pro) 3 .

2. 𝜙 ⊨ 𝜿 (evalue[C] (𝑏 1 ), . . . , evalue[C] (𝑏 𝑘 )) ≤ 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 ) ∧ ¬𝜙 ⊨ 𝑓 ≤ 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 )

⇒ evalue[while (𝜙) {C}] (𝑓 ) ≤ 𝜿 (𝑏 1 , . . . , 𝑏 𝑘 ).

Concerning (2), we exploit evalue[while (𝜙) {C}] (𝑓 ) = ect[while (𝜙) {costFree(C)}] (𝑓 ) and ecost[costFree(C)] = 0. The theorem gives a modular recursive procedure to infer upper bounds on costs of loops, as follows, cf. Section 8.

(1) Estimate the cost of one iteration of the body C.

(2) Analyse how the expected value of the base functions 𝑏 𝑖 is changed by one iteration of the body changes, as formalises in the expected value transformer.

(3) Solve the recurrence, given by the implication, where 𝜿 is to be determined. Crucially the loop's body C becomes treatable in complete independence of the loop itself. Via Lemma 7.2 and Lemma 7.4, sequential composition can be treated similarly to Theorem 7.5. Theorem 7.6 (Modular Seqential Analysis). Let C and 𝜅 be as in Lemma 7.4. Then

Analysis of Examples

We conclude the section, by discussing the analysis of the running examples of Section 2 using our methodology. Further, we present an interesting example by [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF] modelling a fork-join queues. Noteworthy, all displayed bounds are derived via our implementation eco-imp as detailed in the following section.

Geo. Reconsider the program C geo (Figure 1b), where the cost is given by the number of loop iterations. Since loop-iterations depend on the value of 𝑏, we choose the base function ⟨𝑏⟩. This is sufficient to handle C geo via Theorem 7.5(1). The body D of the loop changes ⟨𝑏⟩ to 1/2•⟨0⟩+1/2•⟨1⟩ = 1/2 in expectation. Moreover, the cost of a single loop iteration ecost[D] is one, which follows by unfolding the definition. By Theorem 7.5(1), 𝜿 (⟨𝑏⟩) is an upper bound to the cost of the loop if

A case analysis on 𝑏 = 1 shows that the constraint is satisfied with 𝜅 (𝑥) ≜ 2 • 𝑥. Finally, since 𝑏 1 before entering the loop we derive the optimal bound 𝜅 (⟨1⟩) = 2 for C geo .

Trader. Recall program C trader from Figure 1a. As we have seen in Section 3, the cost of the inner loop is given by ⟨𝑛⟩ • ⟨𝑝⟩. This then yields ecost

, as bound the cost of the body D of the outer loop. Wrt. the outer loop itself, consider the base functions

Note that the loop body D increments and decrements the price with probabilities 1 /4 and 3 /4, respectively, whereas 𝑚𝑖𝑛 remains unchanged. Formally,

which can be derived by unfolding evalue[D] and applying Theorem 7.5(2). In turn, the above constraint holds with 𝜅 (𝑥, 𝑦) ≜ 10

Our implementation selects, among others, the base functions 𝑏 1 ≜ ⟨𝑛 -𝑐𝑜𝑢𝑝𝑜𝑛𝑠⟩ 2 and 𝑏 2 ≜ ⟨𝑛 -𝑐𝑜𝑢𝑝𝑜𝑛𝑠⟩ • ⟨𝑐𝑜𝑢𝑝𝑜𝑛𝑠 + 1⟩ from the loop guard, for which it derives bounds

, describing the cost of the loop, is then shown satisfiable by taking 𝜅 (𝑥, 𝑦) ≜ 𝑥 + 1 /2 • 𝑦. Substituting 0 for 𝑐𝑜𝑢𝑝𝑜𝑛𝑠 in the bound 𝜿 (𝑏 1 , 𝑏 2 ) due to the initial assignments yields the overall estimate ⟨𝑛⟩ + 1/2 • ⟨𝑛⟩ 2 for the expected cost of C coupons . This analysis was performed in 195ms with our tool.

Queuing Network. Fork-join queues (see [START_REF] Kim | Analysis of the Fork-join Queue[END_REF]) have been used to model various systems [START_REF] Dean | MapReduce: Simplified Data Processing on Large Clusters[END_REF][START_REF] Hill | Amdahl's Law in the Multicore Era[END_REF][START_REF] Menascé | Response-Time Analysis of Composite Web Services[END_REF]. They consist of 𝑛 processors, each of which is equipped with a dedicated queue. On arrival at the fork point, a job is probabilistically split into 𝑛 sub-jobs, which are then served by each of the 𝑛 servers commanding the respective queues. After completion, the sub-jobs wait until all other sub-jobs have also been processed. The sub-jobs are then rejoined and the job is completed.

Following [START_REF] Wang | Cost Analysis of Nondeterministic Probabilistic Programs[END_REF], we represent fork-join queues for 2 servers as a probabilistic program with a unitary cost model, that measures progress of the sub-jobs in the respective queues, cf. Figure 4a on page 18. A fixed probability ( 1 /50) is employed to model the arrival of new jobs, while 𝑛 jobs are processes by the two servers. With probability 1 /5 the job is handled by the first server. Otherwise, with equal probability the job is handled either by the second server, or, passed to both servers. Server 1 takes 3 time units for completion, while Server 2 takes 2 units. If the job is split on the servers, the Server 1 and 2 require 2 and 1 units, respectively. This is modelled by enlarging the queues respectively. Each server can handle one queue entry per time unit. The cost for the fork-join queue is given by the expected time of completion of each job, equally representable as the length of the longest queue. Our prototype computes the (asymptotically) optimal bound 113 /741⟨𝑛 + 1⟩ + 125 /243 + 125 /244 in 2.215s.

Simplification Rules

Logical Rules

Fig. 6. Constraint simplification rules.

that both 𝑐 1 and 𝑐 2 are well-formed wrt. 𝜎. Well-formedness of 𝑐 under 𝜎 guarantees that 𝑐 (𝜎) is defined and non-negative. We call 𝑐 well-formed wrt. a Boolean expression 𝜙, if 𝑐 is well-formed for all stores 𝜎 such that 𝜎 ⊨ 𝜙. Apart from the lack of fixed points, the syntax of cost expression is rich enough to express our expectation transformers. Division is included to express the built-in distributions outlined above. Cost expressions form a commutative semigroup under +, with 0 the unit element. Thus, it is justified to consider cost expressions equal up to associativity and commutativity of +, as well as the unit law 0 + 𝑐 = 𝑐 + 0 = 𝑐.

For 𝑐 ∈ CExp and 𝑒 ∈ CExp, we define multiplication 𝑐 ★ (𝑒 1 /𝑒 2 ) with a fraction 𝑞 = 𝑒 1 /𝑒 2 by recursion on 𝑐 in the natural way as follows:

Note that this operation preserves well-formedness. Due to the last clause, 𝑐 ★ (𝑒 1 /𝑒 2 ) does in general not equal 𝑐 • (𝑒 1 /𝑒 2 ), namely, on stores 𝜎 where the fraction is negative. However, for well-formed cost expression 𝑒 1 /𝑒 2 , the equality holds.

Constraint simplification. In Figure 6, we present an inference system over constraints 𝜙 ⊨ 𝑐 ≤ 𝑑, where 𝑐, 𝑓 ∈ CExp and 𝜙,𝜓 ∈ BExp. This system eliminates max, guards and disjunctions by case analysis. We elide a rule for max occurring in right-hand sides, as this can be easily prevented in the constraint solving setup. We say a constraint 𝜙 ⊨ 𝑐 ≤ 𝑑 is well-formed, if 𝑐, 𝑑 are well-formed under 𝜙. It is valid if for all stores 𝜎 ∈ Σ with 𝜎 ⊨ 𝜙, we have 𝑐 (𝜎) ≤ 𝑑 (𝜎). It is easy to see that the rules preserve well-formedness. The system is sound and complete in the following sense. Theorem 8.1. Let Δ be a derivation of a well-formed constraint 𝜙 ⊨ 𝑐 ≤ 𝑑. Then this constraint is valid if and only if all premises in Δ are.

This statement is proven by induction on the derivation Δ. The rules concerning division, rule (divL) and (divR), are sound because the divisor 𝑓 is positive on all stores 𝜎 satisfying 𝜙, due to the well-formedness assumption.

Example 8.2. Recall that the analysis of program C geo in Section 7.1 required solving the constraint 𝑏 = 1 ⊨ 1+𝜿 (1/2) ≤ 𝜿 (⟨𝑏⟩). Fix 𝜅 (𝑥) ≜ 𝑞•𝑥 for undetermined 𝑞 ∈ R ≥0 and note that ⟨𝑏⟩ = [0 ≤ 𝑏]•𝑏 by definition. By unfolding 𝜅, the cost of the loop in C geo is given by 𝜿 (⟨𝑏⟩) if 𝑏 = 1 ⊨ 1 + 𝒒/2 ≤ [0 ≤ 𝑏] • 𝒒 • 𝑏, is valid for some 𝑞 ∈ R ≥0 . Eliminating guards yield several constraints, but only the constraint 𝑏 = 1 ∧ 0 ≤ 𝑏 ⊨ 1 + 𝒒/2 ≤ 𝒒 • 𝑏, is not subject to rule (triv) or rule (contr). Rule (divL) then yields 𝑏 = 1 ∧ 0 ≤ 𝑏 ⊨ 2 + 𝒒 ≤ 2 • 𝒒 • 𝑏 . (7) By Theorem 8.1, this constraint is equi-satisfiable with the initial one above, in the sense that any value for 𝑞 for the latter makes also the former valid.