47 Proofs about locks — where heavy tools are really needed

47.1 The vocabulary of separation logic#

In ordinary logic, A ∧ B is “both are true”. Separation logic adds one more connective. A ∗ B reads “A and B are true, and they are about separate pieces of memory”. Claims about memory must imply ownership. x ↦ 3 does not mean “x holds 3” but “I own x and its value is 3”. So x ↦ 3 ∗ y ↦ 4 says x and y are different places, and writing x does not spoil the claim about y. That is local reasoning.

It is the same idea as chapter 12′s exclusivity rule. Actually the order is the reverse — Rust’s borrow checker moved the idea of separation logic into a type system, and this language’s exclusivity rule is in that lineage. chapter 42 is this chapter’s idea brought down to translation time.

The one-line invariant is the whole lock. R cannot be in two places at once, so only one flow holds R.

          acquire — the CAS turns false into true
   ┌────────────────────────────────────────────┐
   │                                            ▼
 open    lk ↦ false ∗ R                  locked  lk ↦ true
         R sits inside the invariant             R and the token locked γ are in the holder's hands
   ▲                                            │
   └────────────────────────────────────────────┘
          release — hand back both the token and R

47.2 There cannot be two tokens#

If two flows acquired at once there would be two tokens, which is false. One release specification stops two defects. Releasing without acquiring lacks locked γ and cannot meet the precondition; using the resource after releasing fails because R was already returned.

The proofs share a three-step shape: open the invariant, run the CAS (splitting into success and failure), close the invariant. That the invariant may be opened only at an atomic moment is Iris’s rule, and thanks to it “no other flow can see the invariant briefly broken” is guaranteed.

47.3 Tools only as needed#

This is also why Coq was chosen. Iris is Coq-only and Lean has no mature counterpart. Where the tools that would one day be needed lived decided the proof language.

47.4 rwlock — two proofs of the same sentence#

For the classic rwlock packing three meanings into one word — 0 empty, n > 0 n readers, −1 write-locked — exclusivity of the write lock was proven directly (wlocked_exclusive, wlock_spec, wunlock_spec in LowentRWLock.v). Because CAS succeeds only from 0, “a writer enters while readers are present” is stopped. Most real rwlock defects are exactly that.

Fractional ownership on the read side was already in Iris. Its rwlock interface is written with a fractional predicate Φ : Qp → iProp, and rw_spin_lock is a verified instance. Readers get a fraction Φ q (several at once), writing and reading cannot coexist, and a writer gets all of Φ 1. What is valuable is that “writing and reading are exclusive” has two proofs of the same sentence. Ours shows it by “CAS succeeds only from 0” (close to the implementation); the borrowed one by ghost state (general, and covering fractions). The principle of building two ways and cross-checking (chapter 31) holds once more at the proof level.

47.5 Deadlock freedom and no starvation#

 ascending order kept (A < B)          discipline broken
 flow 1   holds A → wants B            flow 1   holds A → wants B
 flow 2   wants A (waits)              flow 2   holds B → wants A
 → flow 1 takes B and goes on          → each waits for the other (deadlock)

Honestly — the tool does not enforce this discipline. So it is “written this way it is safe”, not “the compiler stops it”. Making it a check would require static orders on locks. And the lock’s own specification (acquiring gives the resource) does not prevent deadlock, because it says “acquiring gives” and not “it will be acquired”. Acquire a lock twice and release once, and the second acquire never arrives.

The limits are clear. Cooperative scheduling assumes yielding. Before a task looping forever without yield, the scheduler can do nothing. Priorities and blocking are outside this model too.

47.6 A borrowed proof in weak memory — spsc#

Iris’s language (heap_lang) is a sequentially consistent model. Proving code that writes weak memory orderings needs iRC11 and gpfsl, the Iris logics over RC11. LowentIRC11.v built the first theorem on them — in a message-passing program written with a release write and an acquire read, the reader always sees the data under RC11. It does not assume sequential consistency. chapter 46′s E4 rose from one execution to a whole program.

With that tool one standard library module was built.

module ring .
rem run: main

use spsc .

proc main input k cap atomic . input al cap allocator . output u8 . effects atomic alloc .
do
  let gc option mut slice u8 be alloc_bytes al capacity 16 .
  let gb option mut slice u8 be alloc_bytes al capacity 32 .
  let go option mut slice u8 be alloc_bytes al capacity 8 .
  guard is_some gc . else return 255 .
  guard is_some gb . else return 254 .
  guard is_some go . else return 253 .
  var ctl mut slice u64 be view_array u64 (some_value gc) .
  var buf mut slice u64 be view_array u64 (some_value gb) .
  var out mut slice u64 be view_array u64 (some_value go) .
  let a u64 be spsc.spsc_push k ctl buf 10 .
  let b u64 be spsc.spsc_push k ctl buf 32 .
  let got u64 be spsc.spsc_pop k ctl buf out .
  guard eq got 1 . else return 252 .
  let first u64 be index out 0 .
  let again u64 be spsc.spsc_pop k ctl buf out .
  return narrow u8 (add first (index out 0)) .
end

$ lowentc --run main ring.low
main() = 42

The producer first fills the slot and then publishes the index with release. The consumer reads that index with acquire before reading the slot. lowent_spsc_push_is_correct and lowent_spsc_pop_is_correct say this pair is correct under RC11 (including full and empty checks).

 producer                                 consumer
 buf[i] ← x          (fill the slot first)
 tail ← i+1  release ─────────────────▶   tail  acquire  sees i+1, then
                                          reads buf[i] → it must see x (under RC11)

47.7 What is not proven#

• The lock model is sequentially consistent. Weak memory orderings are not in the heap_lang lock proofs. But since the default ordering is seq_cst (chapter 46), level 3 code written with defaults is inside that model, and only code writing weak orderings is left to iRC11. Containment holds here too.
• There is no guarantee the implementation is this spinlock.
• two_threads_spec does not state the exact total.
• Deadlock freedom relies on a discipline people keep. No starvation assumes yielding; priorities and blocking are outside.
• There is no guarantee our compiler emits that spsc program. One-to-one emission of memory orderings and not reordering them are confirmed by tests.
• Borrowed proofs enter the trusted base. Two checkers (Coq 8.20.1 · Rocq 9.2) giving the same answer reduces the chance of checker defects, but the two files needing gpfsl are confirmed only under Rocq 9.2.