Interleaving Graph

concurrency computer-architecture

Definition

Interleaving Graph

An interleaving graph is a directed acyclic graph $G=(V,E,v_s,v_t)$ whose paths represent all interleavings of $n$ threads with statement sequences $S_1,\dots ,S_n$.

The nodes are prefix states $(i_1,\dots ,i_n)$, where $i_j$ is the number of statements already executed by thread $T_j$. The edge

$$(i_1,\dots ,i_j,\dots ,i_n)\to (i_1,\dots ,i_j+1,\dots ,i_n)$$

means that thread $T_j$ executes its next statement.

The start node is $v_s=(0,\dots ,0)$ and the end node is $v_t=(|S_1|,\dots ,|S_n|)$.

Combinatorics

Every path from $v_s$ to $v_t$ corresponds to exactly one interleaving, and every interleaving corresponds to exactly one path.

If $k_i=|S_i|$, then the number of paths is

$$\frac{\left({\sum }_i{k}_i\right)!}{k_1!k_2!\cdots k_n!}.$$

For two threads of equal length $k$, this becomes $\left(\genfrac{}{}{0ex}{}{2k}{k}\right)$.

Verification

Interleaving graphs are used to enumerate all candidate executions in concurrent software verification. A property such as mutual exclusion must hold on every path.

Examples

Two threads, two statements each

Let $T_1=(a,c)$ and $T_2=(b,d)$. The interleaving graph is a $3\times 3$ grid. Node $(i,j)$ records that $T_1$ has executed $i$ statements and $T_2$ has executed $j$ statements.

The highlighted path corresponds to the interleaving $(a,c,b,d)$.