# Analysis of Dynamic Message Passing Programs

PhD Defense

Damien Zufferey

IST Austria

2013.08.19

## Outline

• motivation + running example
• preliminaries
• part 1: domains of limits
• part 2: ideal abstraction
• part 3: analysis on top of the covering set
• part 4: implementation and experiments
• conclusion

## Introduction

### Concurrency is unavoidable

 Scaling up Many-core CPU from Intel Scaling out Data center from Google

### Programming abstractions for concurrent programs

 Shared memory + fast (single node) - limited scaling - hard to program Message passing + scales - slower ~ hard to program (easier ?)

### The actor model [Hewitt et al. 73]

Used as an abstraction to scale up and out.
Actors react to events (messages) by:

• performing internal computation
• sending messages (unbounded mailboxes)
• creating new actors (unbounded number of actors)

Gaining traction in the PL community and in industry: Erlang, Scala + Akka

Snippet from Akka.io, retrieved on 2013.08.10

## Example: Hollywood Map-Reduce

Simple flow

(Hint: there is a reason it is called the movie industry.)

To do verification we need a property to check, e.g.,
there should not be a winner if there are still people entering the competition.

• motivation + running example
• preliminaries
• part 1: domains of limits
• part 2: ideal abstraction
• part 3: analysis on top of the covering set
• part 4: implementation and experiments
• conclusion

## Foundation of this work

State-space exploration 101

### Well-structured transition systems (WSTS)

A well-structured transition system is a transition system 〈S, →, ≤〉  where

• ≤ is a well-quasi-ordering (wqo), i.e. well-founded + no infinite antichain
• compatibility of ≤ w.r.t. → (also called monotonicity)

 Compatibility in general Compatibility in our example

The property we check also needs to respect the ordering (upward-closed).

Some references: [Abdulla et al. 96, Finkel and Schnoebelen 01]

### Depth-bounded systems (DBS)

Depth-bounded systems are a fragment of the π-calculus identified by [Meyer 08] as an instance of WSTS. In [Bansal, Koskinen, Wies, and Zufferey 13.] we give an alternative formalization as graph rewriting system.

The states are labelled directed graphs (in families) of bounded tree-depth. (the direction of the edges is irrelevant for the depth.) More concretely, this corresponds to the family of graph where the longest acyclic path is bounded. Here is an example state for our running example:

The transitions are graph rewriting rules:

The ordering is subgraph isomorphism. This is a wqo only on families of graphs where the tree-depth is bounded. Also we assume that there is a finite number of labels.

The covering problem: can the system reach a configuration which is greater (or equal) to the target.

• motivation + running example
• preliminaries
• part 1: domains of limits
• part 2: ideal abstraction
• part 3: analysis on top of the covering set
• part 4: implementation and experiments
• conclusion

## Toward a forward analysis of DBS:domain of limits

Approach to the covering problem: saturation-based forward exploration

The goal is to compute the covering set $C$, i.e. the downward-closure of the reachable states. $C$ is an inductive invariant ($\mathrm{post}\left(C\right)\subseteq C$ and $\mathrm{init}\subseteq C$ ).

Problem: how do we represent $C$ ? (it can be infinite)

### Representing the covering set

An ideal

The covering set has special properties: wqo space, downward-closed.
It can be represented by a finite union of ideal.

Since [Karp and Miller 69] these kind of sets have been represented using some notion of limits. However, general formalizations of the concept came much later:

### Limit configurations

We represent limits by nested graphs.
The subgraphs marked by dashed-blue boxes represent an unbounded number of copies of that subgraph.
We can obtain normal graphs from nested graphs by unfolding.

Transition applied to limit configuration

### Results [Wies, Zufferey, and Henzinger 10]

Theorem: Limit configurations are the denotation of the ideals of depth-bounded systems.

ingredient of the proof:

• '!' in π-calculus,
• tree closure of graph,
• hedge automaton for unranked trees,
• etc.

• motivation + running example
• preliminaries
• part 1: domains of limits
• part 2: ideal abstraction
• part 3: analysis on top of the covering set
• part 4: implementation and experiments
• conclusion

## Bridging the gap between theory and practice:ideal abstraction

In [Zufferey, Wies, and Henzinger 12], we define an abstract interpretation framework [Cousot and Cousot 77] for the analysis of WSTS.
Try to capture the essence of acceleration with a set-widening operator.
Instantiate the framework for:

• Petri nets + monotonic extensions
• Lossy channel systems
• Depth-bounded systems

Acceleration does not terminates.

### Covering set for our running example

• motivation + running example
• preliminaries
• part 1: domains of limits
• part 2: ideal abstraction
• part 3: analysis on top of the covering set
• part 4: implementation and experiments
• conclusion

## Further analysis on top of the covering set

### Structural counter abstraction

The automaton above is a very coarse overapproximation of the original system. To recover some precision we add counters that keep track of how many copies of a nested node there are.

Extracting constraints from a transition

Results: In [Bansal, Koskinen, Wies, and Zufferey 13] we apply the structural counters abstraction to prove termination of DBS.

Using the same idea we are working on DPI.

• motivation + running example
• preliminaries
• part 1: domains of limits
• part 2: ideal abstraction
• part 3: analysis on top of the covering set
• part 4: implementation and experiments
• conclusion

## Implementation: Picasso

http://pub.ist.ac.at/~zufferey/picasso/

input: a DBS either as a graph rewriting system or written in a simple actor language.

output: the covering set, optionally a counter abstraction and proof of termination.

evaluation: examples coming from distributed systems and later shared memory.

Detailed results in the thesis and on the tool's web page.

Picasso's output on our running example.

## Conclusion

• Developed a framework for the analysis of DBS:
• Limits for DBS
• Sound and terminating analysis
• Structural counter abstraction
• Applicable to:
• distributed systems (client-server)
• shared memory (flat collection)
• Safety (covering) and liveness (termination)
• Implementation in Picasso