Introduction

Imagine two threads running in parallel. Thread A reads a variable; Thread B writes a different one. Does it matter which goes first? Not at all — the end state is identical either way. Yet a naive model checker treats "A then B" and "B then A" as two separate states to explore, and with nn independent actions the blowup reaches n!n!.

This is state-space explosion: the core challenge of verifying any concurrent system. The number of possible interleavings of even a handful of threads grows so fast that exhaustive search becomes hopeless. A program with ten threads each taking ten steps could in principle generate 101010^{10} orderings.

Partial-order reduction (POR) is the elegant answer. If two actions are independent — neither one affects the other's outcome — then exploring only one of their possible orderings is enough. The technique, developed in the early 1990s by Doron Peled, Antti Valmari, and Patrice Godefroid, is now the backbone of every serious model checker.

Try It

The demo below shows a small concurrent system with two threads, each performing a sequence of actions. Independent actions (operating on different variables) can be reordered freely — their interleavings are equivalent and only one needs to be explored.

<!-- Partial-order reduction demo: collapse equivalent interleavings. -->
<p class="hint">Two threads each execute two actions. When actions operate on <b>different</b> variables they are <b>independent</b> — their order does not matter and only one interleaving needs checking. Toggle independence to see the state space shrink.</p>
<div class="controls">
  <div class="thread-labels">
    <span class="label-a">Thread A</span>
    <span class="label-b">Thread B</span>
  </div>
  <div class="actions-row" id="actions-a">
    <!-- Thread A action chips, rendered by JS. -->
  </div>
  <div class="actions-row" id="actions-b">
    <!-- Thread B action chips, rendered by JS. -->
  </div>
</div>
<div class="stats-row">
  <div class="stat-box full-box">
    <div class="stat-label">Full interleavings</div>
    <div class="stat-num" id="full-count">0</div>
  </div>
  <div class="stat-arrow">&#8594;</div>
  <div class="stat-box reduced-box">
    <div class="stat-label">POR reduced</div>
    <div class="stat-num" id="reduced-count">0</div>
  </div>
  <div class="stat-box saving-box">
    <div class="stat-label">Savings</div>
    <div class="stat-num" id="saving-pct">0%</div>
  </div>
</div>
<div id="graph-area" class="graph-area">
  <!-- State-space graph rendered here by JS. -->
</div>
<div class="btns">
  <button id="btn-toggle-indep" type="button">Make actions dependent</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>
<div class="legend">
  <span class="leg-full">&#9632; pruned (equivalent)</span>
  <span class="leg-reduced">&#9632; explored by POR</span>
</div>

/* Base layout and typography styles. */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; padding: 14px; }
.hint { font-size: .85rem; color: #444; margin: 0 0 .8rem; line-height: 1.45; }
.controls { margin-bottom: .8rem; }
.thread-labels { display: flex; gap: .5rem; margin-bottom: .25rem; }
.label-a, .label-b { font-size: .8rem; font-weight: 700; padding: .15rem .5rem;
  border-radius: 4px; }
.label-a { background: #dbeafe; color: #1e40af; }
.label-b { background: #fef9c3; color: #713f12; }
/* Action chip and thread label styles. */
.actions-row { display: flex; gap: .4rem; flex-wrap: wrap; margin-bottom: .4rem; }
.action-chip { font-size: .78rem; font-weight: 600; padding: .25rem .6rem;
  border-radius: 6px; cursor: pointer; user-select: none; border: 2px solid transparent;
  transition: all .15s; }
.action-chip.thread-a { background: #eff6ff; color: #1e40af; border-color: #bfdbfe; }
.action-chip.thread-b { background: #fefce8; color: #713f12; border-color: #fde68a; }
.action-chip.independent { opacity: 1; }
.action-chip.dependent { opacity: .5; text-decoration: line-through; }
.stats-row { display: flex; align-items: center; gap: .5rem; margin-bottom: .8rem; flex-wrap: wrap; }
.stat-box { text-align: center; padding: .4rem .7rem; border-radius: 8px; min-width: 70px; }
.full-box { background: #f1f5f9; }
.reduced-box { background: #dcfce7; }
.saving-box { background: #fef9c3; }
.stat-label { font-size: .7rem; color: #666; margin-bottom: .1rem; }
.stat-num { font-size: 1.3rem; font-weight: 700; }
.stat-arrow { font-size: 1.2rem; color: #888; }
/* State-space graph SVG styles. */
.graph-area { width: 100%; overflow-x: auto; margin-bottom: .7rem; min-height: 80px; }
svg.state-graph { display: block; }
.node circle { stroke-width: 1.5; }
.node.start circle { fill: #1e40af; stroke: #1e40af; }
.node.normal circle { fill: #f1f5f9; stroke: #94a3b8; }
.node.pruned circle { fill: #fee2e2; stroke: #fca5a5; stroke-dasharray: 3 2; }
.node text { font-size: 9px; fill: #444; text-anchor: middle; dominant-baseline: middle; }
.edge { stroke: #94a3b8; stroke-width: 1.3; fill: none; marker-end: url(#arr); }
.edge.pruned { stroke: #fca5a5; stroke-dasharray: 4 3; }
.edge.reduced { stroke: #16a34a; stroke-width: 1.8; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .5rem; }
button { font: 600 13px system-ui, sans-serif; padding: .4rem .85rem;
  border: 1px solid #1d3557; background: #1d3557; color: #fff;
  border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.legend { font-size: .75rem; display: flex; gap: 1rem; flex-wrap: wrap; color: #555; }
.leg-full { color: #94a3b8; }
.leg-reduced { color: #16a34a; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Partial-order reduction: when two actions are independent (no shared state)
// only one of their orderings needs to be explored.

// Actions for each thread (two per thread for clarity).
const ACTIONS_A = ['a1', 'a2'];
const ACTIONS_B = ['b1', 'b2'];

// Human-readable label for each action.
const ACTION_LABEL = {
  a1: 'x:=1', a2: 'x:=2', b1: 'y:=1', b2: 'y:=2'
};

// Set of independent action pairs (a-b means a and b are independent).
// By default all cross-thread pairs are independent (different variables).
let independentPairs = new Set(['a1-b1', 'a1-b2', 'a2-b1', 'a2-b2']);

function isIndep(act1, act2) {
  return independentPairs.has(act1 + '-' + act2) || independentPairs.has(act2 + '-' + act1);
}

// Generate ALL interleavings of two sequences (exponential).
function interleavings(seq1, seq2) {
  if (!seq1.length) return [seq2.slice()];
  if (!seq2.length) return [seq1.slice()];
  const r = [];
  for (const rest of interleavings(seq1.slice(1), seq2)) r.push([seq1[0], ...rest]);
  for (const rest of interleavings(seq1, seq2.slice(1))) r.push([seq2[0], ...rest]);
  return r;
}

// POR: only generate the CANONICAL interleaving for independent prefixes.
function porInterleavings(seq1, seq2) {
  // If the first actions of both threads are independent, always schedule A first.
  if (!seq1.length) return [seq2.slice()];
  if (!seq2.length) return [seq1.length ? seq1.slice() : []];
  const firstA = seq1[0], firstB = seq2[0];
  if (isIndep(firstA, firstB)) {
    // canonical order: always A before B when they are independent
    const rest = porInterleavings(seq1.slice(1), seq2.slice(1));
    return rest.map(r => [firstA, firstB, ...r]);
  }
  const r = [];
  for (const rest of porInterleavings(seq1.slice(1), seq2)) r.push([firstA, ...rest]);
  for (const rest of porInterleavings(seq1, seq2.slice(1))) r.push([firstB, ...rest]);
  return r;
}

// Render action chips with independence styling.
function renderChips() {
  const rowA = document.getElementById('actions-a');
  const rowB = document.getElementById('actions-b');
  rowA.innerHTML = '';
  rowB.innerHTML = '';
  for (const a of ACTIONS_A) {
    const chip = document.createElement('span');
    chip.className = 'action-chip thread-a independent';
    chip.textContent = ACTION_LABEL[a];
    chip.title = a;
    rowA.appendChild(chip);
  }
  for (const b of ACTIONS_B) {
    const chip = document.createElement('span');
    // Mark thread-B chip as dependent if any A action conflicts with it.
    const dep = ACTIONS_A.some(a => !isIndep(a, b));
    chip.className = 'action-chip thread-b ' + (dep ? 'dependent' : 'independent');
    chip.textContent = ACTION_LABEL[b];
    chip.title = b;
    rowB.appendChild(chip);
  }
}

// Build and render the state-space graph.
function buildGraph(seqA, seqB) {
  const full = interleavings(seqA, seqB);
  const reduced = porInterleavings(seqA, seqB);
  const reducedSet = new Set(reduced.map(s => s.join(',')));

  // Collect all reachable states as nodes.
  const nodes = new Map();
  const edges = [];
  const rootKey = '';
  nodes.set(rootKey, { id: rootKey, level: 0, pos: 0 });

  for (const seq of full) {
    for (let i = 0; i <= seq.length; i++) {
      const key = seq.slice(0, i).join(',');
      if (!nodes.has(key)) nodes.set(key, { id: key, level: i, pos: 0 });
      if (i > 0) {
        const prev = seq.slice(0, i - 1).join(',');
        const act = seq[i - 1];
        const edgeKey = prev + '|' + key;
        if (!edges.find(e => e.key === edgeKey)) {
          edges.push({ key: edgeKey, from: prev, to: key, act, inReduced: reducedSet.has(key) });
        }
      }
    }
  }
  return { nodes, edges, full, reduced };
}

function renderGraph(seqA, seqB) {
  const area = document.getElementById('graph-area');
  const { nodes, edges, full, reduced } = buildGraph(seqA, seqB);

  const maxLevel = Math.max(...[...nodes.values()].map(n => n.level));
  const byLevel = [];
  for (let l = 0; l <= maxLevel; l++) {
    byLevel[l] = [...nodes.values()].filter(n => n.level === l);
  }
  byLevel.forEach(lev => lev.forEach((n, i) => { n.pos = i; }));

  const W = Math.max(300, byLevel.reduce((m, l) => Math.max(m, l.length), 0) * 70 + 40);
  const H = (maxLevel + 1) * 60 + 20;
  const cx = (node) => {
    const lev = byLevel[node.level];
    const total = lev.length;
    const stepX = total > 1 ? (W - 40) / (total - 1) : 0;
    return total === 1 ? W / 2 : 20 + node.pos * stepX;
  };
  const cy = (node) => 20 + node.level * 60;

  const reducedEdgeKeys = new Set();
  const reducedIL = reduced;
  for (const seq of reducedIL) {
    for (let i = 1; i <= seq.length; i++) {
      const prev = seq.slice(0, i - 1).join(',');
      const key = seq.slice(0, i).join(',');
      reducedEdgeKeys.add(prev + '|' + key);
    }
  }

  let svgContent = `<defs><marker id="arr" markerWidth="6" markerHeight="6" refX="5" refY="3" orient="auto"><path d="M0,0 L6,3 L0,6 Z" fill="#94a3b8"/></marker></defs>`;

  for (const e of edges) {
    const fn = nodes.get(e.from);
    const tn = nodes.get(e.to);
    if (!fn || !tn) continue;
    const x1 = cx(fn), y1 = cy(fn), x2 = cx(tn), y2 = cy(tn);
    const isRed = reducedEdgeKeys.has(e.key);
    const cls = isRed ? 'edge reduced' : 'edge pruned';
    svgContent += `<line class="${cls}" x1="${x1}" y1="${y1}" x2="${x2}" y2="${y2}"/>`;
    const mx = (x1 + x2) / 2, my = (y1 + y2) / 2;
    svgContent += `<text x="${mx + 4}" y="${my}" font-size="8" fill="${isRed ? '#16a34a' : '#fca5a5'}">${ACTION_LABEL[e.act] || e.act}</text>`;
  }

  for (const node of nodes.values()) {
    const x = cx(node), y = cy(node);
    const isStart = node.id === '';
    svgContent += `<g class="node ${isStart ? 'start' : 'normal'}"><circle cx="${x}" cy="${y}" r="10"/></g>`;
  }

  area.innerHTML = `<svg class="state-graph" width="${W}" height="${H}" viewBox="0 0 ${W} ${H}">${svgContent}</svg>`;

  document.getElementById('full-count').textContent = full.length;
  document.getElementById('reduced-count').textContent = reduced.length;
  const saved = full.length > 0 ? Math.round((1 - reduced.length / full.length) * 100) : 0;
  document.getElementById('saving-pct').textContent = i18nFmt('%pct%%', { pct: saved });
}

function update() {
  renderChips();
  renderGraph(ACTIONS_A.slice(), ACTIONS_B.slice());
}

// Toggle independence of all cross-thread action pairs.
let allIndep = true;
document.getElementById('btn-toggle-indep').addEventListener('click', () => {
  allIndep = !allIndep;
  if (allIndep) {
    independentPairs = new Set(['a1-b1', 'a1-b2', 'a2-b1', 'a2-b2']);
    document.getElementById('btn-toggle-indep').textContent = 'Make actions dependent';
  } else {
    independentPairs = new Set();
    document.getElementById('btn-toggle-indep').textContent = 'Make actions independent';
  }
  update();
});

document.getElementById('btn-reset').addEventListener('click', () => {
  allIndep = true;
  independentPairs = new Set(['a1-b1', 'a1-b2', 'a2-b1', 'a2-b2']);
  document.getElementById('btn-toggle-indep').textContent = 'Make actions dependent';
  update();
});

update();
Result
Console

Toggle which actions are independent and watch the state space shrink. The full count is every possible interleaving; the reduced count is what partial-order reduction needs to check. Even with just a few actions the savings can be dramatic.

The Real Complexity

Partial-order reduction is a solved technique — the core theory is settled and implemented in production tools — but understanding exactly how much it saves is subtle.

  • Best case: if all nn actions in a trace are mutually independent, the full space has n!n! interleavings and POR needs only 1. The savings are superexponential.
  • Worst case: if every pair of actions is dependent (they share state), POR cannot eliminate any interleaving and the full space must be explored.
  • The catch: computing the maximum possible reduction — the largest set of interleavings that can be pruned safely — is NP-hard. In practice, tools use efficient conservative approximations:
    • Stubborn sets (Valmari, 1991): a sufficient condition that can be checked quickly.
    • Ample sets (Peled, 1993): used in the SPIN model checker; guarantees no property is missed.
    • Sleep sets (Godefroid, 1990): a complementary technique that avoids re-exploring states already seen in another order.

The beauty is that even conservative approximations yield dramatic reductions on real programs. Industrial use in SPIN and similar tools routinely cuts state spaces by factors of 10610^{6} or more.

POR preserves linear temporal logic (LTL) properties with a key restriction: the property must be stutter-invariant — it must not distinguish between a trace and the same trace with repeated states. Most safety and liveness properties of interest satisfy this, which is why POR is so broadly applicable alongside tools like model checking.

Where It Matters

Partial-order reduction is not a theoretical curiosity — it is the reason that formal verification of concurrent systems is possible at all at industrial scale:

  • Protocol verification: tools like SPIN (Gerard Holzmann, NASA) use POR to check communication protocols. It was central to verifying parts of the Mars Pathfinder mission software.
  • Hardware design: modern CPUs and memory subsystems are verified with model checkers that rely heavily on POR to handle the combinatorial explosion of cache-coherence protocols.
  • Operating systems and drivers: Microsoft's SLAM and the Linux kernel's Coccinelle-based checkers use independence-based reductions to find race conditions and deadlocks.
  • Distributed databases: correctness of consensus algorithms like Paxos and Raft is checked with tools (TLA+, P language) that incorporate POR-style reductions.
  • Teaching concurrency: POR gives students a concrete, visualizable reason why thread scheduling order is not always observable — a concept that demystifies data races and lock-free programming.

Wherever you have many small concurrent actors, the independent-action insight applies. POR is the bridge between the theoretical impossibility of exhaustive search and the practical reality of verified concurrent software.

Conclusion

Partial-order reduction rests on a beautifully simple observation: if two actions cannot affect each other, their relative order is irrelevant. That single insight — formalized as an independence relation — collapses the exponential jungle of interleavings into a manageable skeleton.

The technique does not cheat. Every property that holds in the reduced space holds in the full space too. The price is only that the property must be stutter-invariant, which almost all useful correctness properties are.

So the next time you wonder how anyone could possibly verify a real concurrent system, the answer is: they didn't explore every interleaving. They were smart about which ones are the same. That smartness has a name — partial-order reduction — and it is one of the most practically impactful ideas in the theory of model checking.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/partial-order-reduction/Content licensed under CC BY-NC 4.0.