Rely-Guarantee Reasoning

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.

Below, two threads share an integer counter $x$. Each thread increments $x$ by its own amount. Assign a rely (what each thread assumes the other can do to $x$) and a guarantee (what each thread promises it will do to $x$), 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.

<!-- {{c_intro}} -->
<div class="rg-container">
  <div class="intro-line">{{intro_label}}</div>
  <div class="shared-box">
    <span class="shared-label">{{shared_var_label}}</span>
    <span class="shared-val" id="shared-val">x = 0</span>
    <span class="shared-range" id="shared-range"></span>
  </div>

  <!-- {{c_threads}} -->
  <div class="threads">
    <div class="thread" id="thread-a">
      <div class="thread-title">{{thread_a_title}}</div>
      <div class="thread-op" id="op-a">x += 1</div>
      <div class="row-label">{{label_rely}}</div>
      <select id="rely-a" class="sel">
        <option value="inc1">{{opt_inc1}}</option>
        <option value="inc2">{{opt_inc2}}</option>
        <option value="noop" selected>{{opt_noop}}</option>
      </select>
      <div class="row-label">{{label_guarantee}}</div>
      <select id="guar-a" class="sel">
        <option value="inc1" selected>{{opt_inc1}}</option>
        <option value="inc2">{{opt_inc2}}</option>
        <option value="noop">{{opt_noop}}</option>
      </select>
    </div>

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

    <div class="thread" id="thread-b">
      <div class="thread-title">{{thread_b_title}}</div>
      <div class="thread-op" id="op-b">x += 2</div>
      <div class="row-label">{{label_rely}}</div>
      <select id="rely-b" class="sel">
        <option value="inc1">{{opt_inc1}}</option>
        <option value="inc2">{{opt_inc2}}</option>
        <option value="noop" selected>{{opt_noop}}</option>
      </select>
      <div class="row-label">{{label_guarantee}}</div>
      <select id="guar-b" class="sel">
        <option value="inc1">{{opt_inc1}}</option>
        <option value="inc2" selected>{{opt_inc2}}</option>
        <option value="noop">{{opt_noop}}</option>
      </select>
    </div>
  </div>

  <div class="btns">
    <button id="btn-verify" type="button">{{btn_verify}}</button>
    <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
  </div>

  <!-- {{c_result_area}} -->
  <div id="result" class="result"></div>
  <div id="steps" class="steps"></div>
</div>

/* {{c_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; }

// Code not found

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

Classical Hoare logic uses a triple $\{P\}\; C\; \{Q\}$: if precondition $P$ holds before command $C$, postcondition $Q$ 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$ — precondition (what must hold before $C$ starts).
• $R$ — rely: a relation on states that the environment is allowed to make; $C$ may assume the environment only takes $R$-steps.
• $G$ — guarantee: a relation on states that $C$ itself is allowed to make; every atomic action of $C$ must be a $G$-step.
• $Q$ — postcondition (what must hold after $C$ finishes, accounting for any environment $R$-steps in between).

The composition rule says: given two threads $C_1$ with $(R_1, G_1)$ and $C_2$ with $(R_2, G_2)$, running them in parallel is safe as long as $G_1 \subseteq R_2$ and $G_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 $C_1 \parallel C_2$ is verified without examining individual interleavings.

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

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.

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.