Article · MLambda.Data

No locks

What happens when you build a distributed database entirely out of actors — and specify its consistency model before you trust it.

No locks — every component an actor; correctness from message ordering; consistency checked in TLA+.

Every database you have used protects its internals with locks. Latches on pages, mutexes around the write-ahead log, reader-writer locks on the index. Locks are how shared mutable state stays sane under concurrency, and the history of database engineering is, in large part, the history of making them cheaper and holding them for less time.

MLambda.Data has none. Not fewer — none, in the data path. It is not a stunt; it is what falls out when you take the actor model seriously enough to build a storage engine from it.

Actors all the way down

An actor owns its state and talks to the world only through messages, handled one at a time. That single rule dissolves the problem locks exist to solve: if there is no shared mutable state, there is nothing to guard. So in MLambda.Data, everything that would normally be a protected data structure is an actor with a mailbox.

The write path is a WriteActor that appends to a write-ahead log (CRC32 on every record), updates a sorted in-memory memtable, and notifies the index actors. The read path is a ReadActor that consults a Bloom filter, then the memtable, then the immutable SSTables on disk. Compaction is a CompactionActor that merges SSTables in the background under a throttle, so it cannot starve foreground work. Indexes are actors too — a B-tree for range queries, a hash index for point lookups, an inverted index for full-text search — each updated by message, each answering by message. Beneath them, a distributed filesystem: a NamespaceActor for the registry, FileActors for blocks, BlockActors for physical I/O.

Ordering, not exclusion, is what keeps this correct. A message is processed after the one before it and before the one after; the actor's state at any moment is a function of the messages it has handled. Concurrency comes from having many actors, not from letting many threads into one.

Supervision instead of hope

The other thing you get from actors is a story for failure. Every storage actor has a guardian — EngineGuardian, StorageGuardian, IndexGuardian, FilesystemGuardian — and a guardian's job is to decide what happens when a child crashes: restart it, restart its siblings, or escalate. A corrupted SSTable reader does not take down the engine; it is restarted by its supervisor, and the write-ahead log is the source of truth it recovers from. The failure modes are designed, not discovered.

The cluster is the same idea, larger

Across machines, a RingManager places data on a consistent hash ring, a ClusterAdapter discovers members, and cluster metadata is replicated through gossip using CRDTs — data types that merge without coordination, so nodes converge without a leader deciding for them. The same actors run in three topologies — standalone, hybrid, cluster — chosen by configuration alone; the code does not change.

Consistency you can check, not read about

Here is the part I care about most. Every database publishes a consistency model. Almost none publish a proof. MLambda.Data's consistency model is written as a TLA+ specification and run through the TLC model checker, which enumerates every reachable state of the protocol looking for one that violates an invariant. When a document says "reads see all acknowledged writes", that sentence corresponds to a temporal property that either holds over the state space or produces a counterexample. It is not prose. It is a checked claim.

That is the same discipline the rest of the MLambda stack is built on: specify, check, then build. It is why MLambda.Data can be the data layer for systems that Turing generates — the generator can trust it for the same reason you can.


MLambda.Data is in development. Architecture, the consistency model, the formal specification and a research whitepaper are public at data.mlambda.net. Builds through early access.