Skip to content

CONCEPT Cited by 3 sources

Compositional specification

Definition

A compositional (or modular) specification describes a system as a set of smaller specs connected by explicit interface boundaries, rather than as one monolithic spec of the whole system. Each sub-spec can be model-checked in isolation, reviewed by the team that owns that component, and — when the interface is clean — independently conformance-checked against an implementation.

The "multiple specifications model aspects of the system (not one monolithic spec)" practice of patterns/extreme-modelling is the methodology side of the same idea; this page is the property of the resulting artefact.

Why it matters

The two failure modes of non-compositional specs, both called out directly in MongoDB's retrospectives (Source: sources/2025-06-02-mongodb-conformance-checking-at-mongodb-testing-that-our-code-matches-our-tla-specs):

  1. Monolithic rot. An engineer writes one huge TLA+ spec for the whole system; it grows too complex to understand, state-space explosion defeats the TLC model-checker, the author concludes "TLA+ is impractical," and abandons it. Davis's framing in the 2025-06-02 post.
  2. No leverage for conformance. A monolithic spec offers no natural place to stop and say "this sub-component must obey this interface." Conformance has to check the whole behaviour end-to-end — which is exactly where retrofit-trace-checking breaks on multithreaded-state-snapshot cost.

Compositional structure avoids both: each sub-spec is small enough to model-check in reasonable time, and each interface boundary is a natural place to conformance-check the component below it.

The MongoDB distributed-transactions case

MongoDB's VLDB 2025 cross-shard transactions spec is the canonical compositional-TLA+ case on this wiki (Source: sources/2026-02-27-mongodb-towards-model-based-verification-of-a-key-value-storage-engine):

"We had developed a TLA+ specification of MongoDB's distributed transactions protocol in a compositional manner, describing the high level protocol behavior while also formalizing the boundary between the distributed aspect of the transactions protocol and the underlying single-node WiredTiger storage engine component."

Two modules, one interface:

  • Top-level transactions spec — cross-shard protocol behaviour, snapshot isolation properties, commit-point rules, model-checked against invariants in the large.
  • Storage.tla — the single-node storage-interface contract, extracted from the interface boundary. "Our storage layer specification itself serves as a useful and precise definition of a subset of the WiredTiger storage engine semantics."

The interface boundary is load-bearing in both directions:

  • Upward: the transactions spec relies on Storage.tla's behaviour as its model of what the single-node layer does. Proofs about the protocol compose over the storage-layer contract rather than reaching into WiredTiger internals.
  • Downward: Storage.tla can be lifted out as its own verification artefact and used to drive test-case generation against the real WiredTiger implementation. Path coverings over its reachable-state graph produce 87,143 tests for a 2-key × 2-transaction finite model in ~40 minutes — a conformance check of exactly the contract the transactions spec relies on.

This is what the post means by modular verification: verify each module against its own spec, and verify the interface contract between modules — rather than trying to verify the whole system against one spec.

Properties of a good interface boundary

MongoDB's experience surfaces a few:

  • Narrow. The interface names operations (WiredTiger's timestamp-aware API), not internal data structures. The storage layer's B-tree, page cache, journal, and checkpoint mechanisms are all below the boundary and invisible to the transactions spec.
  • State-driven, not implementation-driven. The spec captures what states the storage layer can be in from the transactions layer's point of view, not how WiredTiger gets there.
  • Directly implementable. The interface corresponds to real API calls — the WiredTiger session.begin_transaction()-style operations — so a test harness can drive the implementation through exactly the actions the spec enumerates.
  • Co-designed with the implementation. The boundary was drawn with knowledge of where WiredTiger actually breaks its work; abstractions are aligned at design time, not retrofitted years later (patterns/extreme-modelling lesson).

Relation to the 2020 RaftMongo.tla case

The compositional approach is the methodological lesson from 2020's failure (Source: sources/2025-06-02-mongodb-conformance-checking-at-mongodb-testing-that-our-code-matches-our-tla-specs). RaftMongo.tla modelled commit-point propagation in isolation but the spec's abstraction (atomic leader handoff as one step) did not match the server's concrete behaviour (step-down-then-step-up as two steps), so conformance-checking via trace-checking failed after 10 weeks. The 2025 storage-engine case got the interface right first time because:

  • The spec was co-designed with the VLDB 2025 protocol work, not a decade later.
  • The interface chosen was a real API (WiredTiger's public calls) that both layers had to respect anyway.
  • The module was small enough for TLC to enumerate at a useful finite configuration and narrow enough that test-case generation was tractable.

Seen in

Last updated · 200 distilled / 1,178 read