Interleaving

concurrency

Definition

Interleaving

Given $n$ threads with statement sequences $S_1,S_2,\dots ,S_n$, an interleaving is a total order $\sigma$ on ${\bigcup }_i{S}_i$ such that

$$x{<}_{i}y⟹x{<}_{\sigma }y(\text{for all }{T}_i,x,y\in S_i).$$

The set $\mathcal{I}(S_1,\dots ,S_n)$ of all interleavings is the exhaustive space of executions under any memory model that serialises memory operations.

Examples

Two threads

Let $T_1=(a,c)$ and $T_2=(b,d)$. The local program orders are $a{<}_{1}c$ and $b{<}_{2}d$.

All interleavings:

$$\mathcal{I}(T_1,T_2)=\{(a,c,b,d),(a,b,c,d),(a,b,d,c),(b,a,c,d),(b,a,d,c),(b,d,a,c)\}.$$

For $n$ threads with $k_1,\dots ,k_n$ statements each,

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

For two equal-length threads this is $\left(\genfrac{}{}{0ex}{}{2k}{k}\right)$; here $k=2$ gives $\left(\genfrac{}{}{0ex}{}{4}{2}\right)=6$.

Because different runtimes, scheduling, and hardware can realise any interleaving, correctness arguments must account for all of them.