# Monotonicity in data flow analysis

I am studying program analysis and synthesis, I was reading a presentation about some data flow analysis.

I can't seem to understand why $$\bigcap_{s'\in\text{pred (s)}}\text{Out}(s')$$ and $$\operatorname{Gen}(s)\cup(\operatorname{In}(s)\setminus \operatorname{Kill}(s))$$ is monotone, as claimed in slide 22.

I don't even understand exactly what is the function that is claimed to be monotone. Can anyone please help ? any help is greatly appreciated!

*This was cross-posted on Math.SE a couple of days ago

• More appropriate for cs.stackexchange. – Yuval Filmus Apr 14 '13 at 23:41
• slides are from a graduate level class. seems research level to me. as for your question, think it would be better to define the functions. also try reading about monotone circuit theory which has same defn – vzn Apr 15 '13 at 3:20
• A set function $f(s)$ is monotone if $s \subseteq t$ implies $f(s) \subseteq f(t)$. Oftentimes if a function is monotone then it's obvious, for example it's probably obvious that $\mathrm{Gen}(s)$ is monotone. – Yuval Filmus Apr 15 '13 at 5:01
• @vzn I stick to my claim that this question is not research level. – Yuval Filmus Apr 15 '13 at 5:02
• As someone working in the area, I can say that this is not a research question. The Gen-Kill data flow analysis is described in almost every compiler text book and the theoretical framework exists since 1973. It is undergraduate level material but is sometimes not taught because there is too much material to cram into a single compiler course and not for difficulty reasons. – Vijay D Apr 15 '13 at 10:20

You need to identify the lattices involved in each case.

Let $(\wp(S),\subseteq)$ be the lattice of all subsets of a set $S$ ordered by subset inclusion. A function $f:\wp(S) \to \wp(S)$ is monotone if for every pair of sets $x$ and $y$, if $x \subseteq y$ it also holds that $f(x) \subseteq f(y)$. The definition applies more generally to functions $f: L \to M$ between partially ordered sets $L$ and $M$.

Let $Stmt$ be the set of statements occurring in a program and let $(\wp(Stmt),\subseteq)$ be the lattice of subsets of statements ordered by subset inclusion. Let us assume for simplicity that a statement in $Stmt$ is either an assignment $x:= e$ or a Boolean expression $b$ (representing the entry of a conditional or head of a loop).

A control flow graph has the form $G = (Stmt,E)$ where $E$ is an edge relation over statements. The following definitions are extremely standard:

$succ: \wp(Stmt) \to \wp(Stmt)$ maps a set of statements to their successors.

$succ(X) = \{ y \in Stmt | \text{ there exists } x \text{ in } X \text{ such that } (x,y) \text{ is in } E\}$

$pred: \wp(Stmt) \to \wp(Stmt)$ maps a set of statements to their predecessors.

$pred(X) = \{ y \in Stmt | \text{ there exists } x \text{ in } X \text{ such that } (y,x) \text{ is in } E\}$

It is a standard exercise to show that these are monotone functions.

Consider the set $Exp$ of all arithmetic and Boolean expressions occurring in a program. The structure $(\wp(Exp),\subseteq)$ is a lattice with the subset inclusion order.

For the available expressions analysis, we can define two functions $Gen$ and $Kill$ in two steps as follows.

First define $Gen: Stmt \to \wp(Exp)$ as a function that maps a statement to the set of expressions generated by that statement. We can define $Gen$ inductively and lift it to sets as follows.

$Gen(x := e) = \{e\}$ and $Gen(b) = \{b\}$

The lifted function $Gen: \wp(Stmt) \to \wp(Exp)$ is obtained in a standard manner by taking the union of $Gen$ sets for every statement in a given set.

$$Gen(S) = \bigcup_{s \in S} Gen(s)$$

You can now ask whether this function is monotone.