Baradb/docs/en/distributed.md

Distributed Systems

BaraDB supports distributed deployment with Raft consensus, sharding, and replication.

⚠️ Multi-Database Limitation The distributed modules (Raft, sharding, and replication) are currently wired to the default database only. If you use multiple databases (CREATE DATABASE, USE DATABASE), distributed features do not yet span across them. Each database would need its own cluster setup.

Raft Consensus

Leader election and log replication over TCP. Enable with:

Env	Meaning
BARADB_RAFT_ENABLED=true	Turn on Raft
BARADB_RAFT_NODE_ID	This node's id
BARADB_RAFT_PORT	Raft TCP port
BARADB_RAFT_PEERS	Comma-separated id@host:port (include self)
BARADB_RAFT_WRITE_TIMEOUT_MS	Max wait for majority commit on SQL writes (default 5000)

When Raft is enabled, SQL DML (INSERT/UPDATE/DELETE/MERGE and transactional COMMIT) is accepted only on the leader: each write's KV pairs are appended to the Raft log and the client waits until the entry is majority-committed. Followers reject writes with not leader; leader is '…'. Followers apply committed entries via applyCommand into the default database. DDL (e.g. CREATE TABLE) is not replicated yet — apply schema on every node.

import barabadb/core/raft

var cluster = newRaftCluster()
cluster.addNode("node1")
cluster.addNode("node2")
cluster.addNode("node3")

let n1 = cluster.nodes["n1"]
n1.becomeCandidate()
n1.becomeLeader()
let entry = n1.appendLog("SET key1 value1")

Sharding

Distribute data across nodes:

import barabadb/core/sharding

var router = newShardRouter(ShardConfig(
  numShards: 4,
  replicas: 2,
  strategy: ssHash
))
router.rebalance(@["node1", "node2", "node3"])
let shard = router.getShard("user_123")

Sharding Strategies

Strategy	Description
ssHash	Hash-based sharding
ssRange	Range-based sharding
ssConsistent	Consistent hashing

Replication

import barabadb/core/replication

var rm = newReplicationManager(rmSync)
rm.addReplica(newReplica("r1", "10.0.0.1", 9472))
rm.connectReplica("r1")
let lsn = rm.writeLsn(@[1'u8, 2, 3])
rm.ackLsn("r1", lsn)

Replication Modes

Mode	Description
rmSync	Synchronous replication
rmAsync	Asynchronous replication
rmSemiSync	Semi-synchronous replication

Gossip Protocol

Membership and failure detection:

import barabadb/core/gossip

var g = newGossipManager()
g.addNode("node1")
g.addNode("node2")
g.tick()  # Exchange membership info

Distributed Transactions

Two-phase commit across nodes:

import barabadb/core/disttxn

var dt = newDistributedTxn()
dt.prepare(@["node1", "node2"])
dt.commit()

Formal Verification

Core distributed algorithms are formally specified in TLA+ and model-checked:

• Raft Consensus — formal-verification/raft.tla
  • Verified: ElectionSafety, StateMachineSafety
• Two-Phase Commit — formal-verification/twopc.tla
  • Verified: Atomicity, NoOrphanBlocks
• Replication — formal-verification/replication.tla
  • Verified: MonotonicLsn, AcksRemovePending

Run TLC locally:

cd formal-verification
java -cp tla2tools.jar tlc2.TLC -config models/raft.cfg raft.tla
java -cp tla2tools.jar tlc2.TLC -config models/twopc.cfg twopc.tla
java -cp tla2tools.jar tlc2.TLC -config models/replication.cfg replication.tla