4a83eb6783
- Add multi-database limitations to distributed docs - Fix backup commands and add multi-database backup guidance - Add SQL migration section to schema docs - Update storage examples to use per-database paths
2.6 KiB
2.6 KiB
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
defaultdatabase 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:
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