Shared state and safety properties.
In the previous post of this series, we built a tiny model-checker core: a cooperative scheduler capable of enumerating all possible interleavings of a set of tasks. At that stage, tasks had no shared state and there was nothing to check. Executions were merely different, not correct or incorrect.
In this post, we extend that core in order to check the correctness of simple but real algorithms: a shared counter and a single-producer single-consumer (SPSC) ring buffer.
To do that, we need to add two orthogonal ingredients:
We deliberately do not add blocking, waiting, fairness assumptions, or search-space reduction yet.
Throughout this post we restrict ourselves to safety properties. Informally, a safety property states that
“something bad never happens.”
If a safety property is violated, there exists a finite execution prefix that demonstrates the violation. This is exactly what systematic exploration is good at: we can stop as soon as we find such a prefix and report it as a counterexample.
We do not check liveness properties (“something good eventually happens”). Liveness reasoning typically requires fairness assumptions and reasoning about infinite executions. It is also unclear to me whether and how meaningful liveness guarantees can be expressed within a stateless model checker of the kind we are building here. We therefore deliberately exclude liveness from the scope of this post.
We will use two closely related kinds of safety checks:
Implementation-wise, both are treated the same way: if the predicate evaluates to false, the current execution is rejected.
(define (ASSERT cnd msg)
(unless cnd
(error "ASSERT" msg)))
Assertions are checked during execution and fail fast. They are intended to be called from within tasks.
An important limitation is that an assertion can only observe the shared state and the local state of the task executing the assertion. It cannot inspect the local state of other tasks.
This is in stark contrast to specification languages such as TLA+, where both shared state and per-process local state are explicitly modeled by the user, and invariants can quantify over the entire global state. Our tiny checker is much more restrictive: local task state lives in the host language and is not reified as part of the model. This keeps the executable model simple and close to real code, at the cost of reduced observational power.
(define (check-postconds postconds)
(for-each
(lambda (p)
(when (not (p))
(error "postcondition failed")))
(reverse postconds)))
(define (EXPLORE . postconds)
(explore postconds))
; usage
(EXPLORE
(lambda () (= 1 1))
(lambda () (= 2 2)))
Postconditions are thunks registered with EXPLORE and evaluated once an
execution terminates normally, that is, once all tasks have finished. Each
postcondition returns a boolean indicating success or failure.
If any postcondition evaluates to false, the current execution is rejected in the same way as an assertion failure.
Postconditions are particularly useful when correctness is most naturally expressed as a predicate over the final shared state, rather than as an invariant that must hold at every intermediate step.
Even in a tiny checker, it is worth being disciplined about where state lives.
The easiest mistake is to let tasks mutate arbitrary top-level Scheme variables
using set!. While this works for a single execution, it quickly becomes
problematic once we start enumerating many executions: such mutations are not
mediated by the model checker and are therefore hard to reset cleanly between
runs.
Instead, we adopt the convention of routing all shared state through a small, explicit interface. This keeps state accesses visible to the checker and easy to reason about when exploring executions. In this way, each execution starts from the same initial store, rather than accumulating unrelated global mutations across runs.
Note that the user might still circumvent this convention and simply define and modify top-level Scheme variables; a more restrictive environment would be a good improvement to our tiny model checker.
The underlying memory model is intentionally minimal:
- a single global store,
- sequentially consistent reads and writes,
- explicit interleaving points at shared-state accesses (unless suppressed
by ATOMIC).
No buffering, access reordering, or blocking is modeled at this stage.
We start by extending the model checker with a thin memory component wrapping a hash table. Locations are represented symbolically and normalized to strings before being stored.
(import (srfi 69))
(define hash-table-buckets 1024)
(define *memory* (make-hash-table equal?
string-hash
hash-table-buckets))
(define (init-location loc val)
(let ((loc (location->string loc)))
(if (hash-table-exists? *memory* loc)
(error "reinitialized location" loc val)
(hash-table-set! *memory* loc val))))
(define (write-location loc val)
(let ((loc (location->string loc)))
(if (not (hash-table-exists? *memory* loc))
(error "write to uninitialized location" loc val)
(hash-table-set! *memory* loc val))))
(define (read-location loc)
(let ((loc (location->string loc)))
(if (not (hash-table-exists? *memory* loc))
(error "read from uninitialized location" loc)
(hash-table-ref *memory* loc))))
Next, we introduce user facing extensions of the DSL.
;;; Initialiazes location `loc` with value `val`.
;;; Cannot be called from within a task.
(define (INIT loc val)
(init-location loc val))
Initialization is treated as a separate phase that happens before execution
begins. (INIT ...) is called at the top-level of the program, for example,
(INIT 'x 0)
(SPAWN (lambda ()
(print "hello")))
(EXPLORE)
This avoids implicit defaults and makes all shared state explicit.
;;; Writes value `val` to location `loc`.
;;; Can only be called from within a task.
;;;
;;; The current task yields *before* the writing if the operation
;;; is not in an atomic block.
;;;
;;; The location must be initialized before being written.
(define (WRITE loc val)
(YIELD)
(write-location loc val))
A WRITE represents a single, instantaneous update to shared state. By
yielding before the write, we make each write an explicit scheduling point.
;;; Returns value in location `loc`.
;;; Can only be called from within a task.
;;;
;;; The current task yields *before* the reading if the operation
;;; is not in an atomic block.
;;;
;;; The location must be initialized before being read.
(define (READ loc)
(YIELD)
(let ((val (read-location loc)))
(print "READ " loc " " val)
val))
A READ is also an interleaving point: the task yields before observing the
value. Reads are instantaneous and observe the globally visible state.
So far, every shared-memory access is an interleaving point. This keeps the
model maximally general. However, many algorithms rely on compound operations
that should not be interleaved internally. To support this, we introduce an
ATOMIC construct:
(ATOMIC
(READ ...)
(WRITE ...)
...)
Semantically, ATOMIC temporarily disables YIELD for the extent of its
body. No other task can interleave while the atomic block executes.
Importantly, ATOMIC does not imply blocking, and does not guarantee
fairness. It is purely a scheduling restriction.
The atomic block implementation follows: ```scheme (define in-atomic-block (make-parameter #f)) (define (in-atomic-block?) (in-atomic-block)) (define-syntax atomic-block (syntax-rules () ((_ SEXP …) (parameterize ((in-atomic-block #t)) SEXP …))))
(define (YIELD) (unless (in-atomic-block?) (yield)))
(define-syntax ATOMIC (syntax-rules () ((_ SEXP …) (begin (YIELD) (atomic-block SEXP …))))) ```
One alternative approach would be to let users explicitly annotate non-atomic steps, as is done in specification languages such as TLA+. We instead choose the opposite default:
let, arithmetic, pure functions) is atomic by
default.This matches programmers’ intuition, keeps models concise, and most importantly
makes shared-state interference explicit. If a block must execute without
interleaving, the user must state this explicitly using ATOMIC.
An equally valid modeling choice would be message passing. Conceptually, the implementation is almost identical: instead of mapping a location to a value, we could map a channel name to a queue (for example, a list).
The scheduler integration is also the same: sends and receives are interleaving points just like reads and writes.
A minimal wrapper DSL can be built directly on top of READ, WRITE, and
INIT:
;;; Define a channel as a list of messages
(define (CHAN name)
(INIT name '()))
;;; Append a message to the channel
(define (SEND ch v)
(WRITE ch (append (READ ch) (list v))))
;;; Receive one message (fail-fast on empty)
(define (RECV ch)
(let ((q (READ ch)))
(when (null? q)
(error "channel empty" ch))
(WRITE ch (cdr q))
(car q)))
This highlights that “shared memory vs message passing” is largely a semantic choice about how values are interpreted, not a fundamental change to the checker.
At this point in the development, the model assumes that:
These assumptions will be relaxed in later posts, but keeping them here makes the effect of shared-state interference maximally explicit.
The explore procedure enumerates executions by repeatedly replaying the
program under different scheduling histories. To do so, it takes a snapshot of
the shared memory content after all INIT calls but before tasks are started.
Once an execution runs to completion, returning from (run), we check the
postconditions and restore the memory and task queue for the upcoming execution.
(define (explore postconds)
(let ((initial-taskqueue (snapshot-taskqueue))
(initial-memory (snapshot-memory)))
(let loop ((execution-count 0))
(if (or (zero? execution-count)
(has-future? (extract-history)))
(let ((prev-hist (swap-history!)))
(print "\n=== EXECUTION " (+ 1 execution-count) " ===")
(set! *prev-hist* prev-hist)
(run)
(print "== HISTORY: " (extract-history))
(check-postconds postconds)
(restore-taskqueue! initial-taskqueue)
(restore-memory! initial-memory)
(loop (+ execution-count 1)))
execution-count))))
As a first example, consider the simplest shared-state bug: a lost update on a shared counter.
(INIT 'x 0)
(define (task)
(let ((v (READ 'x)))
(WRITE 'x (+ 1 v))))
(SPAWN task)
(SPAWN task)
(EXPLORE
(lambda () (= (READ 'x) 2))))
Two tasks might produce the following execution:
=== EXECUTION 2 ===
READ x 0
READ x 0
WRITE x 1
WRITE x 1
== HISTORY: ((0 . 1) (0 . 1) (1 . 1) (0 . 1) (0 . 1) (0 . 0))
READ x 1
Error: postcondition failed
Both read the value 0 from x and both write 1 to x. To make the update
atomic, we can use the ATOMIC block effectively transforming those operations
into a read–modify–write (RMW) step:
(define (task)
(ATOMIC
(let ((v (READ 'x)))
(WRITE 'x (+ 1 v)))))
We now consider a single-producer / single-consumer (SPSC) ring buffer of fixed
capacity N. Despite its simplicity, this example already exhibits real
concurrency bugs under certain interleavings, making it a good first benchmark
for our checker.
The buffer is represented using two unbounded indices:
head, pointing to the next element to be consumed,tail, pointing to the next free slot for production.The physical buffer slot is obtained by reducing these indices modulo N.
(define N 2)
;; ringbuffer helpers ----
(define (bufx i)
(cons 'buf (modulo i N)))
(define (buf-ref i)
(READ (bufx i)))
(define (buf-set! i v)
(WRITE (bufx i) v))
;; initialization ----
(INIT 'head 0)
(INIT 'tail 0)
;; The following (do ...) form is equivalent to
;; `for (i = 0; i < N; i++)`
(do ((i 0 (+ i 1))) ((= i N))
(INIT (bufx i) 'EMPTY))
The counters head and tail grow monotonically, while the modulo operation
maps them onto a fixed-size ring. This separation between logical
indices and physical slots is standard in ring-buffer implementations and
simplifies correctness reasoning.
The ring buffer helpers make it explicit that all buffer accesses go through the shared-memory interface introduced earlier.
(define (ring-enq v)
(let ((tail (READ 'tail))
(head (READ 'head)))
(if (= (- tail head) N)
'FULL
(begin
(buf-set! tail v)
(WRITE 'tail (+ tail 1))
'OK))))
(define (ring-deq)
(let ((head (READ 'head))
(tail (READ 'tail)))
(if (= (- tail head) 0)
(values 'EMPTY #f)
(begin
(WRITE 'head (+ head 1))
(values 'OK (buf-ref head))))))
Note that the following implementation contains a subtle bug in the interaction
between ring-enq and ring-deq. Can you spot it? The following code shows the
producer task enqueueing 3 values and the consumer task :
(define (producer)
(ring-enq 1)
(ring-enq 2)
(ring-enq 3))
(define (consumer)
(let loop ((expected 1))
(let-values (((status val) (ring-deq)))
(when (eq? status 'OK)
(ASSERT (= val expected) "FIFO order")
(loop (+ expected 1))))))
(SPAWN producer)
(SPAWN consumer)
(EXPLORE)
Like this:
=== EXECUTION 87 ===
READ head 0
READ tail 0
READ head 0
WRITE (buf . 0) 1
WRITE tail 1
READ tail 1
READ head 0
WRITE (buf . 1) 2
WRITE tail 2
READ tail 2
READ tail 2
WRITE head 1
READ head 1
WRITE (buf . 0) 3
WRITE tail 3
READ (buf . 0) 3
Error: ASSERT: "FIFO order"
Here, the consumer observes value 3 before value 2, violating FIFO order.
In this post, we extended the tiny model checker with:
This already lets us find real concurrency bugs under realistic interleavings, without introducing blocking, fairness, or reduction.
In the next post, we will tackle blocking and waiting, and see how even
simple await loops fundamentally change the shape of the state space.
If you want to try out the code yourself, you can download the source, the counter example, and the ring buffer example.
See also other parts of this series. Feedback is welcome – please send a message to my public inbox: ~db7/public-inbox@lists.sr.ht (Archive)
© 2024-2026 db7 — licensed under CC BY 4.0.