Introduction

Concurrent programs are notoriously hard to reason about. Two threads share memory, each step of one can interleave with any step of the other, and a bug may appear only in one exotic scheduling order out of millions.

In 1983 the computer scientist Cliff Jones published a strikingly simple fix. Instead of trying to enumerate every possible interleaving, he asked each thread to sign a two-clause contract:

  • Rely — what the thread assumes the environment (all other threads) will do to shared state.
  • Guarantee — what the thread promises it will do to shared state, no matter how the environment behaves within the rely condition.

If every thread's guarantee is at least as strong as every other thread's rely, the contracts are consistent and you can verify each thread in isolation — no global interleaving enumeration needed. The method is called Rely-Guarantee (R-G) reasoning, and it scales to real operating-system kernels and processor pipelines. See also program equivalence for a related angle on formal reasoning about programs.

Try It: Two Threads, One Counter

Below, two threads share an integer counter xx. Each thread increments xx by its own amount. Assign a rely (what each thread assumes the other can do to xx) and a guarantee (what each thread promises it will do to xx), then press Verify to check whether:

  1. Each thread's local invariant is preserved under its rely condition.
  2. Each thread's guarantee is at least as strong as the other thread's rely.
<!-- Rely-Guarantee demo: two threads share a counter x. -->
<div class="rg-container">
  <div class="intro-line">Each thread has a Rely (what it assumes the other does) and a Guarantee (what it promises it does). For composition to be safe, each thread’s Guarantee must be covered by the other thread’s Rely.</div>
  <div class="shared-box">
    <span class="shared-label">Shared counter:</span>
    <span class="shared-val" id="shared-val">x = 0</span>
    <span class="shared-range" id="shared-range"></span>
  </div>

  <!-- Thread A increments by 1, Thread B increments by 2. -->
  <div class="threads">
    <div class="thread" id="thread-a">
      <div class="thread-title">Thread A</div>
      <div class="thread-op" id="op-a">x += 1</div>
      <div class="row-label">Rely</div>
      <select id="rely-a" class="sel">
        <option value="inc1">increment by 1</option>
        <option value="inc2">increment by 2</option>
        <option value="noop" selected>no change (noop)</option>
      </select>
      <div class="row-label">Guarantee</div>
      <select id="guar-a" class="sel">
        <option value="inc1" selected>increment by 1</option>
        <option value="inc2">increment by 2</option>
        <option value="noop">no change (noop)</option>
      </select>
    </div>

    <div class="compose-arrow">&#x2295;</div>

    <div class="thread" id="thread-b">
      <div class="thread-title">Thread B</div>
      <div class="thread-op" id="op-b">x += 2</div>
      <div class="row-label">Rely</div>
      <select id="rely-b" class="sel">
        <option value="inc1">increment by 1</option>
        <option value="inc2">increment by 2</option>
        <option value="noop" selected>no change (noop)</option>
      </select>
      <div class="row-label">Guarantee</div>
      <select id="guar-b" class="sel">
        <option value="inc1">increment by 1</option>
        <option value="inc2" selected>increment by 2</option>
        <option value="noop">no change (noop)</option>
      </select>
    </div>
  </div>

  <div class="btns">
    <button id="btn-verify" type="button">Verify</button>
    <button id="btn-reset" type="button" class="ghost">Reset</button>
  </div>

  <!-- Result area and per-check breakdown. -->
  <div id="result" class="result"></div>
  <div id="steps" class="steps"></div>
</div>

/* Rely-Guarantee demo styles. */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; padding: .5rem; }
.rg-container { max-width: 520px; margin: 0 auto; }
.intro-line { font-size: .88rem; color: #555; margin-bottom: .8rem; line-height: 1.4; }
.shared-box { display: flex; align-items: center; gap: .6rem; background: #e8eef3;
              border: 1px solid #cdd9e3; border-radius: 8px; padding: .5rem .8rem;
              margin-bottom: 1rem; flex-wrap: wrap; }
.shared-label { font-size: .82rem; color: #555; }
.shared-val { font: 700 1.1rem ui-monospace, monospace; color: #1d3557; }
.shared-range { font-size: .8rem; color: #777; margin-left: auto; }
.threads { display: flex; align-items: flex-start; gap: .5rem; }
.thread { flex: 1; background: #f5f8fa; border: 1px solid #d0dbe4; border-radius: 10px;
          padding: .7rem .8rem; }
.thread-title { font-weight: 700; font-size: .95rem; margin-bottom: .4rem; color: #1d3557; }
.thread-op { font: 600 1rem ui-monospace, monospace; background: #dde8f0;
             border-radius: 6px; padding: .3rem .6rem; margin-bottom: .6rem;
             color: #1a3550; display: inline-block; }
.row-label { font-size: .78rem; color: #666; margin: .35rem 0 .15rem; text-transform: uppercase;
             letter-spacing: .04em; }
.sel { width: 100%; padding: .3rem .4rem; font-size: .85rem; border: 1px solid #b0bec8;
       border-radius: 6px; background: #fff; color: #222; cursor: pointer; }
.compose-arrow { font-size: 1.6rem; color: #7a9ab5; align-self: center; padding: 0 .1rem; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-top: .9rem; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem;
         border: 1px solid #1d3557; background: #1d3557; color: #fff;
         border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.result { margin-top: .8rem; font-weight: 600; font-size: .97rem; min-height: 1.4em; }
.result.ok { color: #0a7d33; }
.result.bad { color: #c92f3c; }
.result.warn { color: #b06000; }
.steps { font-size: .83rem; color: #555; margin-top: .4rem; line-height: 1.5; }
.steps .chk { margin: .15rem 0; }
.steps .chk.pass::before { content: "✓ "; color: #0a7d33; }
.steps .chk.fail::before { content: "✗ "; color: #c92f3c; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));

// Atomic operations each thread can perform.
// delta is the signed change to x; label is the display string.
const OPS = {
  inc1: { delta: 1, label: '+1' },
  inc2: { delta: 2, label: '+2' },
  noop: { delta: 0, label: '+0' }
};

// Guarantee subset-of Rely check.
// R subset G means: if G allows a change it must be allowed by R too.
// Here each op is just a delta; G subset R iff G.delta <= R.delta (both non-negative).
function subsetOf(gKey, rKey) {
  return OPS[gKey].delta <= OPS[rKey].delta;
}

// Local invariant: x stays non-negative.
// Thread A invariant: x stays >= 0. Guaranteed by any non-negative increment.
// Thread B invariant: x stays >= 0. Same.
function invariantHolds(relyKey) {
  return OPS[relyKey].delta >= 0;
}

function verify() {
  const relyA  = document.getElementById('rely-a').value;
  const guarA  = document.getElementById('guar-a').value;
  const relyB  = document.getElementById('rely-b').value;
  const guarB  = document.getElementById('guar-b').value;

  // Check 1: Thread A guarantee must be a subset of Thread B rely.
  const check1 = subsetOf(guarA, relyB); // G_A subset R_B
  // Check 2: Thread B guarantee must be a subset of Thread A rely.
  const check2 = subsetOf(guarB, relyA); // G_B subset R_A
  // Check 3: Thread A invariant holds under its own rely.
  const check3 = invariantHolds(relyA);
  // Check 4: Thread B invariant holds under its own rely.
  const check4 = invariantHolds(relyB);

  const allPass = check1 && check2 && check3 && check4;
  const resultEl = document.getElementById('result');
  const stepsEl  = document.getElementById('steps');

  const finalX = OPS[guarA].delta + OPS[guarB].delta;
  document.getElementById('shared-val').textContent = 'x = 0 → ' + finalX;
  document.getElementById('shared-range').textContent =
    i18nFmt('after both threads: x = %finalX%', { finalX: finalX });

  resultEl.className = 'result ' + (allPass ? 'ok' : 'bad');
  resultEl.textContent = allPass ? '✓ Contracts consistent — composition is safe!' : '✗ Contracts inconsistent — composition is unsafe.';

  const checks = [
    { pass: check1, text: i18nFmt('G_A (%ga%) ⊆ R_B (%rb%): Thread A’s guarantee covered by Thread B’s rely', { ga: OPS[guarA].label, rb: OPS[relyB].label }) },
    { pass: check2, text: i18nFmt('G_B (%gb%) ⊆ R_A (%ra%): Thread B’s guarantee covered by Thread A’s rely', { gb: OPS[guarB].label, ra: OPS[relyA].label }) },
    { pass: check3, text: 'Thread A invariant (x >= 0) preserved under its rely' },
    { pass: check4, text: 'Thread B invariant (x >= 0) preserved under its rely' }
  ];
  stepsEl.innerHTML = checks
    .map(c => `<div class="chk ${c.pass ? 'pass' : 'fail'}">${c.text}</div>`)
    .join('');
}

function reset() {
  document.getElementById('rely-a').value  = 'noop';
  document.getElementById('guar-a').value  = 'inc1';
  document.getElementById('rely-b').value  = 'noop';
  document.getElementById('guar-b').value  = 'inc2';
  document.getElementById('shared-val').textContent  = 'x = 0';
  document.getElementById('shared-range').textContent = '';
  document.getElementById('result').className = 'result';
  document.getElementById('result').textContent = '';
  document.getElementById('steps').innerHTML = '';
}

document.getElementById('btn-verify').addEventListener('click', verify);
document.getElementById('btn-reset').addEventListener('click', reset);
Result
Console

When both checks pass the composition rule fires and the joint invariant holds — without ever simulating all interleavings.

The Formal Core

Classical Hoare logic uses a triple {P}  C  {Q}\{P\}\; C\; \{Q\}: if precondition PP holds before command CC, postcondition QQ holds after. But Hoare triples assume no interference — the program runs alone.

Jones extended the triple to a quintuple:

{P, R}  C  {G, Q}\{P,\, R\}\; C\; \{G,\, Q\}

  • PP — precondition (what must hold before CC starts).
  • RR — rely: a relation on states that the environment is allowed to make; CC may assume the environment only takes RR-steps.
  • GG — guarantee: a relation on states that CC itself is allowed to make; every atomic action of CC must be a GG-step.
  • QQ — postcondition (what must hold after CC finishes, accounting for any environment RR-steps in between).

The composition rule says: given two threads C1C_1 with (R1,G1)(R_1, G_1) and C2C_2 with (R2,G2)(R_2, G_2), running them in parallel is safe as long as G1⊆R2G_1 \subseteq R_2 and G2⊆R1G_2 \subseteq R_1. That is, what thread 1 guarantees is a subset of what thread 2 is prepared to tolerate, and vice versa. Under this condition the parallel composition C1∥C2C_1 \parallel C_2 is verified without examining individual interleavings.

This is decidedly not trivial. For nn threads each with kk atomic steps, the number of interleavings grows as (nkk)n−1\binom{nk}{k}^{n-1} — effectively exponential. R-G cuts the cost to linear in nn.

Where It Matters

Rely-Guarantee is not just a theory exercise — it has been the backbone of several landmark verification efforts:

  • OS kernel verification: the seL4 microkernel proof and related work use R-G-style reasoning to handle concurrent system calls.
  • Processor pipeline verification: guarantees that individual pipeline stages make only their contracted writes to shared registers.
  • Concurrent data structures: lock-free queues, stacks, and hash tables are verified compositionally — each operation's rely captures what concurrent operations may do to the internal nodes.
  • Separation logic marriage: Vafeiadis and Parkinson (2007) merged R-G with separation logic to get RGSep, combining local heap ownership with global interference contracts.
  • Compiler and runtime proofs: memory-model contracts between the compiler and the hardware are naturally expressed as guarantee conditions.

Every time you write a lock-free data structure and reason "this write is safe because the other thread can only do X", you are informally doing Rely-Guarantee.

Conclusion

Concurrent programs are hard because of the exponential explosion of interleavings. Rely-Guarantee sidesteps the explosion by turning global reasoning into local reasoning: each thread writes down what it relies on and what it guarantees, and if those contracts are consistent, the whole system is correct — no scheduling enumeration needed.

The idea is elegant precisely because it mirrors how engineers already think: "my module assumes the shared bus does X, and it only writes Y back." Making that assumption explicit and checkable is what transforms informal intuition into a formal proof. It is also a reminder that the hardest problems in computer science are often solved not by smarter search but by a better way of asking the question.

Share this article

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

Comments

Loading comments...

https://www.kipuhub.com/en/article/rely-guarantee/Content licensed under CC BY-NC 4.0.