Interleaving Graph

concurrency computer-architecture

Definition

Interleaving Graph

An interleaving graph is a directed acyclic graph whose paths represent all interleavings of threads with statement sequences .

The nodes are prefix states , where is the number of statements already executed by thread . The edge

means that thread executes its next statement.

The start node is and the end node is .

Combinatorics

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

If , then the number of paths is

For two threads of equal length , this becomes .

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 and . The interleaving graph is a grid. Node records that has executed statements and has executed statements.

The highlighted path corresponds to the interleaving .