eco-imp

• Download
• Installation
• Usage
• Experiments

Expected Cost Analysis of Probabilistic Imperative Programs

Our tool ecoimp performs an expected cost analysis for simple imperative programs featuring probabilistic sampling instructions, as outlined in our recent paper.

Download and Installation

The tool is open source and can be downloaded from here. The source code is available via our Gitlab repository. It is implemented in Haskell and relies on a recent version of the Glasgow Haskell Compiler. It requires various auxiliary libraries and tools, such as our GUBS solver. Thus, the easiest way to install ecoimp is via stack which takes care of installing all dependencies. To install ecoimp via stack, navigate to the source distribution folder in a terminal and type:

stack install

This will install an executable ecoimp together with all its requirements. Note however that GUBS solver needs an SMT-solver installed, specifically, only yices (version >= 2.6.1) is supported at the moment.

Usage

You can invoke our tool on the command line by

ecoimp <file>

where <file> is the program that should be analysed. The program should adhere to the following format. Notice that similar to Python or Haskell, the syntax of commands Cmd is block sensitive: blocks <Cmd> are delimited by whitespace and indentation, rather than braces. For examples, look here.

  Cmd := skip
       | abort
       | tick Exp
       | Var = DExp | Var = Exp
       | if BExp: <Cmd> [else: <Cmd>]?
       | while BExp: <Cmd>
       | nondet: <Cmd> [else: <Cmd>]?
       | prob (Const, Const): <Cmd> [else: <Cmd>]?
       | Cmd Cmd

  Exp := Const
       | Exp + Exp
       | Exp * Exp
       | Exp - Exp
       | -Exp
       | (Exp)

 DExp := rand(Exp)
       | unif(Const,Const)
       | ber(Const,Const)
       | hyper(Const,Const,Const)
       | bin(Const,Const,Const)

 BExp := BLit | not BExp | BExp and BExp | BExp or BExp | (BExp)

  Var := [a-zA-Z][a-zA-Z0-9_]*

Const := [0-9]+

 BLit := Exp <= Exp | Exp >= Exp | Exp < Exp | Exp > Exp | Exp = Exp

A program is given by a definition

def procedure-name():
   Cmds

where procedure-name is the name of the defined procedure and Cmds is a sequence of commands Cmd. The list of program commands may be optionally preceded by a sequence of variable declarations var Varlist. All variables range over integers and are globally scoped. Used variables are implicitly declared.

Most of the commands are self-explanatory. The command tick e consumes e >= 0 resources and defines the analysed cost-measure of the program. A command

nondet:
   C
else:
   D

implements the non-deterministic choice between C and D. In contrast, the command

prob(n,m):
   C
else:
   D

executes C with probability p = n/n+m and D with probability 1-p = m/n+m. The assignment operator = is used both for the usual assignment (as e.g. in x = x + 2) and for sampling from a distribution (as e.g. in x = rand(y + 1)). Currently, the following distributions are implemented:

• rand(e): samples an integer value uniformly in the interval [0,e] where e can be any expression Exp.

• unif(n,m): samples an integer uniformly in the interval [n,m] for constants n and m.

• ber(n,m): samples an integer from the Bernoulli distribution with probability p = n / n + m. Here n+m should be greater than zero.

• hyper(N,K,n): samples an integer from the Hypergeometric distribution for a population size of N, number K of successes in the population and n the number of draws.

• bin(n,m,N): samples an integer from the Binomial Distribution with N trials and a success probability of n / n + m (where n+m greater than zero).

An Example

The next example gives an implementation of the Coupon Collector Problem following Kaminski et al. [2018].

> cat examples/coupons-N.imp
# Coupon Collector's Problem
# Upper Bound: O(n*ln n)

def collector():
  var coupons, draw, N

  coupons = 0
  while 0 <= coupons and coupons < N:
    tick 1
    draw = rand(N)
    draw = draw + 1
    if draw > coupons:
      coupons = coupons + 1

> ecoimp examples/coupons-N.imp
ExecutionLog
|
`- [ect] 0
   |
   +- [Problem]
   |    coupons :~ {1 : 0}
   |    0:While(N ≥ 1 + coupons ∧ coupons ≥ 0)
   |        Tick(1)
   |        draw :~ rand(N)
   |        draw :~ {1 : 1 + draw}
   |        1:If(draw ≥ 1 + coupons) Then
   |            coupons :~ {1 : 1 + coupons}
   |          Else
   |            Skip
   |
   +- [While.Step]
   |  |
 [...]
   |
   `- 1/2 + [N | N ≥ 0] + 1/2·[N^2 | N ≥ 0]

[Success] 1/2 + [N | N ≥ 0] + 1/2·[N^2 | N ≥ 0]

The output of the tool consists on the one hand of an execution log detailing the analysis steps (such as derived bounds for sub-programs, chosen base-functions and their expected values) as well the overall result of the analysis, drawn in the final line. In the example above, showing a cost preserving abstraction of an a quadratic bound on the expected number of trials is derived. More precisely, an expression [p | ϕ] corresponds to p if ϕ is true, and 0 otherwise. The estimated complexity is thus given by 1/2 + N + 1/2 · N^2 for all non-negative N, and 1/2 otherwise.

Experiments

The results of our evaluation are compiled in the following Table, showing the derived upper bounds on the program’s cost as well as the execution time of our implementation. Execution times were measured on a Intel i7-7600U CPU with 2.8GHz and 16GB RAM under Linux. An expression [p | ϕ] corresponds to p if ϕ is true, and 0 otherwise.