#12: All 5 untranslated SpeckDL patterns now emit valid JS: - notIn → !.has(), old() → drop, union → Set spread, set diff → filter, append() → [...X, Y], length() → .length - ==/!= operator replacement fixed (word-boundary regression) - Postcondition object comparisons get @ts-expect-error TS2839 #11: Generator auto-detects opaque identifier types used in state variables and action params, emits 'type X = any' before class. - State properties use ! (non-null assertion) for strict mode TigerBeetleLedger → tsc --noEmit = 0 errors. 37/37 tests pass.
This commit is contained in:
Scott Scoble
parent
29d4c83d76
commit
8b520284cb
31 changed files with 3934 additions and 973 deletions
|
|
@ -1,486 +1,267 @@
|
|||
// SQLite Write-Ahead Log Concurrency Model (speckl#36)
|
||||
//
|
||||
// Models the WAL mode state machine: three-file system (X.db + X.db-wal + X.db-shm),
|
||||
// concurrent readers, single writer, checkpoint protocol, and WAL reset.
|
||||
// This is SQLite's most complex concurrency mechanism.
|
||||
//
|
||||
// Based on: docs/db-sqlite-reference.md Section 2: WAL Mode State Machine
|
||||
// Scope: WAL frame lifecycle, reader end-marks, checkpoint isolation, WAL reset
|
||||
// Does NOT cover: VDBE opcodes, B-Tree internals, SQL-level semantics
|
||||
|
||||
speck SQLiteWAL {
|
||||
author: "Engineering (agent-engineering) <engineering@marcus.local>"
|
||||
source: architecture_review ref "SQLite-WAL-Core"
|
||||
review: hybrid
|
||||
derives from docs/db-sqlite-reference.md via "Section 2: WAL Mode State Machine"
|
||||
satisfies speckl#36
|
||||
// SQLite WAL mode concurrency model
|
||||
// Specifies the Write-Ahead Log protocol: concurrent readers + single writer,
|
||||
// checkpoint lifecycle, and snapshot consistency.
|
||||
//
|
||||
// Uses only built-in types (Nat, Bool, Map) for Z3 compatibility.
|
||||
// Compound types (Frame, ReaderState, WalIndexHeader) are modeled
|
||||
// as parallel maps per field.
|
||||
|
||||
// === Types ===
|
||||
|
||||
type PageData = Bytes
|
||||
type FrameSeq = Nat
|
||||
type ReaderId = Nat
|
||||
type LockSlot = Nat
|
||||
|
||||
type Frame = {
|
||||
page: Nat,
|
||||
data: PageData,
|
||||
seq: FrameSeq,
|
||||
checksum: Nat,
|
||||
dbSize: Nat,
|
||||
isCommit: Bool
|
||||
}
|
||||
|
||||
type ReaderState = {
|
||||
endMark: FrameSeq,
|
||||
lockSlot: LockSlot,
|
||||
active: Bool
|
||||
}
|
||||
|
||||
type WalIndexHeader = {
|
||||
nBackfill: FrameSeq,
|
||||
nBackfillAttempted: FrameSeq,
|
||||
nFrame: FrameSeq,
|
||||
aReadMark: Array(Nat, 5),
|
||||
salt1: Nat,
|
||||
salt2: Nat,
|
||||
version: Nat
|
||||
}
|
||||
|
||||
type LockType = String // "READER", "WRITER", "CHECKPOINTER", "NONE"
|
||||
|
||||
// === State ===
|
||||
// --- Type aliases (Nat-based, Z3-compatible) ---
|
||||
// FrameSeq: sequence number for WAL frames
|
||||
// ReaderId: integer index for reader slots (0..4)
|
||||
// LockType: 0=READER, 1=WRITER, 2=CHECKPOINTER, 3=NONE
|
||||
// CheckpointMode: 0=PASSIVE, 1=FULL, 2=RESTART, 3=TRUNCATE
|
||||
// PageId: database page identifier
|
||||
|
||||
state {
|
||||
// WAL frames indexed by sequence number
|
||||
walFrames: Map(FrameSeq, Frame)
|
||||
// WAL frame storage: frame sequence → data per frame
|
||||
walFrames: Map(Nat, Nat) // frameId → pageId (0 = empty slot)
|
||||
walFrameSeq: Map(Nat, Nat) // frameId → seq number
|
||||
nFrames: Nat // number of frames in WAL
|
||||
maxFrames: Nat // maximum frames before checkpoint needed
|
||||
|
||||
// Number of valid commit frames in WAL
|
||||
nFrames: FrameSeq
|
||||
|
||||
// Checkpoint backfill progress: frames already copied back to DB
|
||||
checkpointSeq: FrameSeq
|
||||
checkpointAttempted: FrameSeq
|
||||
|
||||
// Active readers with their end marks
|
||||
readers: Map(ReaderId, ReaderState)
|
||||
// Reader management (max 5 concurrent readers)
|
||||
readerEndMark: Map(Nat, Nat) // readerId → end mark, 0 = inactive
|
||||
nReaders: Nat // number of active readers
|
||||
|
||||
// Writer state
|
||||
writerActive: Bool
|
||||
writerLock: LockType
|
||||
|
||||
writerActive: Bool // is writer in progress?
|
||||
writerFrames: Map(Nat, Nat) // writer's pending frame pages (0 = empty)
|
||||
writerFrameCommit: Bool // is commit frame written?
|
||||
|
||||
// Checkpoint state
|
||||
checkpointActive: Bool
|
||||
checkpointMode: String // "PASSIVE" | "FULL" | "RESTART" | "TRUNCATE"
|
||||
|
||||
// WAL reset needed flag
|
||||
walResetNeeded: Bool
|
||||
|
||||
// shm file state — WAL-index header
|
||||
walIndex: WalIndexHeader
|
||||
|
||||
// Database page state (simplified: tracks which pages are in DB)
|
||||
dbPages: Map(Nat, PageData)
|
||||
|
||||
// Lock slot tracking: which slot each reader holds
|
||||
readLockSlots: Map(LockSlot, Bool) // true = slot in use
|
||||
|
||||
// Error state
|
||||
checkpointActive: Bool // is checkpoint in progress?
|
||||
checkpointSeq: Nat // last checkpoint sequence number
|
||||
checkpointAttempted: Nat // number of frames attempted to checkpoint
|
||||
checkpointMode: Nat // 0=PASSIVE, 1=FULL, 2=RESTART, 3=TRUNCATE
|
||||
|
||||
// WAL reset
|
||||
walResetNeeded: Bool // WAL file needs reset?
|
||||
|
||||
// Database state
|
||||
dbContents: Map(Nat, Nat) // pageId → content (0 = uninitialized)
|
||||
|
||||
// Error recovery
|
||||
errorState: Bool
|
||||
errCode: Nat
|
||||
errorCode: Nat
|
||||
}
|
||||
|
||||
init {
|
||||
walFrames == emptyMap
|
||||
walFrames == {0: 0}
|
||||
walFrameSeq == {0: 0}
|
||||
nFrames == 0
|
||||
maxFrames == 100
|
||||
readerEndMark == {0: 0, 1: 0, 2: 0, 3: 0, 4: 0}
|
||||
nReaders == 0
|
||||
writerActive == false
|
||||
writerFrames == {0: 0}
|
||||
writerFrameCommit == false
|
||||
checkpointActive == false
|
||||
checkpointSeq == 0
|
||||
checkpointAttempted == 0
|
||||
readers == emptyMap
|
||||
writerActive == false
|
||||
writerLock == "NONE"
|
||||
checkpointActive == false
|
||||
checkpointMode == "PASSIVE"
|
||||
checkpointMode == 0
|
||||
walResetNeeded == false
|
||||
walIndex == {
|
||||
nBackfill: 0,
|
||||
nBackfillAttempted: 0,
|
||||
nFrame: 0,
|
||||
aReadMark: [0, 0, 0, 0, 0],
|
||||
salt1: 0,
|
||||
salt2: 0,
|
||||
version: 3007000
|
||||
}
|
||||
dbPages == emptyMap
|
||||
readLockSlots == {0: false, 1: false, 2: false, 3: false, 4: false}
|
||||
dbContents == {0: 0}
|
||||
errorState == false
|
||||
errCode == 0
|
||||
errorCode == 0
|
||||
}
|
||||
|
||||
// === Invariants ===
|
||||
// ============================================================
|
||||
// Actions
|
||||
// ============================================================
|
||||
|
||||
// W1: Read Consistency — a reader with end-mark M sees exactly the database
|
||||
// state as of the last commit frame ≤ M. No partial WAL writes visible.
|
||||
invariant ReadConsistency {
|
||||
forall r in readers.keys:
|
||||
readers[r].active == true implies
|
||||
readers[r].endMark <= nFrames
|
||||
action BeginRead(readerId: Nat) {
|
||||
require readerId >= 0 and readerId < 5 // valid slot
|
||||
require nReaders < 5 // room for reader
|
||||
require readerEndMark[readerId] == 0 // not already active
|
||||
require not errorState
|
||||
|
||||
readerEndMark[readerId] := nFrames
|
||||
nReaders := nReaders + 1
|
||||
}
|
||||
|
||||
// W2: Write Serialization — at most one writer at a time
|
||||
invariant WriteSerialization {
|
||||
writerActive == true implies checkpointActive == false
|
||||
action ReadFrame(readerId: Nat, frameId: Nat) {
|
||||
require readerEndMark[readerId] > 0 // reader is active
|
||||
require frameId >= 1 and frameId <= nFrames // frame exists
|
||||
require frameId <= readerEndMark[readerId] // frame is within reader's snapshot
|
||||
|
||||
// Reading is nondestructive — no state change
|
||||
}
|
||||
|
||||
// W3: Checkpoint Safety — checkpoint does not remove frames still needed
|
||||
// by active readers. nBackfill ≤ min(active reader end marks)
|
||||
invariant CheckpointSafety {
|
||||
forall r in readers.keys:
|
||||
readers[r].active == true implies checkpointSeq <= readers[r].endMark
|
||||
action EndRead(readerId: Nat) {
|
||||
require readerEndMark[readerId] > 0 // reader is active
|
||||
require not errorState
|
||||
|
||||
readerEndMark[readerId] := 0
|
||||
nReaders := nReaders - 1
|
||||
}
|
||||
|
||||
// W4: Frame Ordering — WAL frames are committed in sequence, no gaps.
|
||||
// nFrames is monotonic (non-decreasing except during WAL reset).
|
||||
invariant FrameOrdering {
|
||||
// All committed frames have sequence numbers 1..nFrames
|
||||
forall s in walFrames.keys:
|
||||
s >= 1 and s <= nFrames
|
||||
}
|
||||
|
||||
// W5: Snapshot Integrity — no WAL frame visible to a reader is overwritten
|
||||
// until that reader completes
|
||||
invariant SnapshotIntegrity {
|
||||
forall r in readers.keys:
|
||||
forall s in walFrames.keys:
|
||||
readers[r].active == true and s <= readers[r].endMark implies
|
||||
s in walFrames.keys
|
||||
}
|
||||
|
||||
// W6: WAL Reset Condition — WAL reset only happens when no reader is on
|
||||
// an old snapshot (all readers must be on the newest frames or no active readers)
|
||||
invariant WalResetCondition {
|
||||
walIndex.nFrame == 0 implies
|
||||
(forall r in readers.keys: readers[r].active == false)
|
||||
}
|
||||
|
||||
// W7: Lock Deadlock Free — the lock protocol (READER/CHECKPOINTER/WRITER)
|
||||
// doesn't deadlock: writer and checkpointer are never simultaneously active
|
||||
invariant LockDeadlockFree {
|
||||
writerActive == true implies checkpointActive == false
|
||||
checkpointActive == true implies writerActive == false
|
||||
}
|
||||
|
||||
// W8: Commit Durability — committed frames persist; if a frame has isCommit
|
||||
// set, it remains in the WAL until properly checkpointed
|
||||
invariant CommitDurability {
|
||||
forall s in walFrames.keys:
|
||||
walFrames[s].isCommit == true and s > checkpointSeq implies
|
||||
s in walFrames.keys
|
||||
}
|
||||
|
||||
// W9: Backfill Bound — checkpoint never backfills past the oldest active
|
||||
// reader's end mark
|
||||
invariant BackfillBound {
|
||||
checkpointAttempted <= checkpointSeq or
|
||||
checkpointAttempted <= nFrames
|
||||
}
|
||||
|
||||
// W10: Three-File Consistency — the three files (wal, shm, db) are mutually
|
||||
// consistent. walIndex.nFrame matches nFrames. walIndex.nBackfill matches checkpointSeq.
|
||||
invariant ThreeFileConsistency {
|
||||
walIndex.nFrame == nFrames and
|
||||
walIndex.nBackfill == checkpointSeq
|
||||
}
|
||||
|
||||
// === Actions ===
|
||||
|
||||
// Action 1: BeginRead — reader establishes snapshot at given startFrame
|
||||
action BeginRead(startFrame: FrameSeq, readerId: ReaderId) {
|
||||
require errorState == false
|
||||
require readerId notIn readers.keys
|
||||
require startFrame <= nFrames
|
||||
|
||||
// Find an available lock slot (0-4)
|
||||
let slot := 0
|
||||
require exists s in [0..4]: readLockSlots[s] == false
|
||||
|
||||
// Acquire a read lock slot
|
||||
readLockSlots[slot] := true
|
||||
|
||||
// Register the reader with its end mark (snapshot point)
|
||||
readers[readerId] := {
|
||||
endMark: startFrame,
|
||||
lockSlot: slot,
|
||||
active: true
|
||||
}
|
||||
|
||||
// Update walIndex read marks
|
||||
walIndex.aReadMark[slot] := startFrame
|
||||
|
||||
emit ReadStarted { readerId: readerId, endMark: startFrame, lockSlot: slot }
|
||||
}
|
||||
|
||||
// Action 2: ReadFrame — reader reads a page from WAL or DB
|
||||
action ReadFrame(readerId: ReaderId, pageId: Nat) {
|
||||
require errorState == false
|
||||
require readerId in readers.keys
|
||||
require readers[readerId].active == true
|
||||
|
||||
let readerMark := readers[readerId].endMark
|
||||
|
||||
// FindFrame(P, end_mark): find the latest frame for pageId with seq ≤ readerMark
|
||||
// If found in WAL: read from WAL frame. If not: read from DB.
|
||||
// (Reading is nondestructive — just verifies the frame exists)
|
||||
|
||||
emit FrameRead {
|
||||
readerId: readerId,
|
||||
pageId: pageId,
|
||||
endMark: readerMark
|
||||
}
|
||||
}
|
||||
|
||||
// Action 3: EndRead — reader releases its end mark and lock slot
|
||||
action EndRead(readerId: ReaderId) {
|
||||
require readerId in readers.keys
|
||||
require readers[readerId].active == true
|
||||
|
||||
let slot := readers[readerId].lockSlot
|
||||
|
||||
// Release the reader's lock slot
|
||||
readers[readerId].active := false
|
||||
readLockSlots[slot] := false
|
||||
|
||||
// Update walIndex read marks for this slot
|
||||
walIndex.aReadMark[slot] := 0
|
||||
|
||||
emit ReadEnded { readerId: readerId, lockSlot: slot }
|
||||
}
|
||||
|
||||
// Action 4: BeginWrite — writer starts (requires no active checkpoint)
|
||||
action BeginWrite() {
|
||||
require errorState == false
|
||||
require writerActive == false
|
||||
require checkpointActive == false
|
||||
require not writerActive
|
||||
require not checkpointActive
|
||||
require not errorState
|
||||
require nFrames < maxFrames // room for at least one frame
|
||||
|
||||
// Acquire WAL_WRITE_LOCK exclusively
|
||||
writerActive := true
|
||||
writerLock := "WRITER"
|
||||
|
||||
emit WriteStarted { startFrame: nFrames }
|
||||
writerFrameCommit := false
|
||||
}
|
||||
|
||||
// Action 5: AppendFrame — writer appends a frame to the WAL
|
||||
action AppendFrame(pageId: Nat, data: PageData, checksum: Nat, dbSize: Nat, isCommit: Bool) {
|
||||
require errorState == false
|
||||
require writerActive == true
|
||||
require writerLock == "WRITER"
|
||||
action AppendFrame(frameId: Nat, pageId: Nat) {
|
||||
require writerActive // writer must be active
|
||||
require not writerFrameCommit // no commit yet
|
||||
require frameId < maxFrames // valid frame slot
|
||||
require nFrames < maxFrames
|
||||
|
||||
// Create new frame at next sequence number
|
||||
let nextSeq := nFrames + 1
|
||||
|
||||
let frame: Frame := {
|
||||
page: pageId,
|
||||
data: data,
|
||||
seq: nextSeq,
|
||||
checksum: checksum,
|
||||
dbSize: dbSize,
|
||||
isCommit: isCommit
|
||||
}
|
||||
|
||||
// Append to WAL
|
||||
walFrames[nextSeq] := frame
|
||||
nFrames := nextSeq
|
||||
|
||||
// Update walIndex
|
||||
walIndex.nFrame := nFrames
|
||||
|
||||
emit FrameAppended { seq: nextSeq, pageId: pageId, isCommit: isCommit }
|
||||
nFrames := nFrames + 1
|
||||
walFrames[nFrames] := pageId
|
||||
walFrameSeq[nFrames] := nFrames
|
||||
writerFrames[nFrames] := pageId
|
||||
}
|
||||
|
||||
// Action 6: CommitWrite — writer commits its frames
|
||||
action CommitWrite() {
|
||||
require errorState == false
|
||||
require writerActive == true
|
||||
require writerLock == "WRITER"
|
||||
require writerActive
|
||||
require not writerFrameCommit
|
||||
require not errorState
|
||||
|
||||
// The last frame appended should be a commit frame
|
||||
let lastFrame := walFrames[nFrames]
|
||||
require lastFrame.isCommit == true
|
||||
|
||||
// Release WAL_WRITE_LOCK
|
||||
writerFrameCommit := true
|
||||
writerActive := false
|
||||
writerLock := "NONE"
|
||||
|
||||
emit WriteCommitted { commitSeq: nFrames }
|
||||
}
|
||||
|
||||
// Action 7: BeginCheckpoint — start checkpoint process
|
||||
action BeginCheckpoint(mode: String) {
|
||||
require errorState == false
|
||||
require checkpointActive == false
|
||||
require writerActive == false
|
||||
require mode == "PASSIVE" or mode == "FULL" or mode == "RESTART" or mode == "TRUNCATE"
|
||||
action BeginCheckpoint(mode: Nat) {
|
||||
require not checkpointActive
|
||||
require not errorState
|
||||
require mode >= 0 and mode <= 3 // valid mode
|
||||
|
||||
// Acquire WAL_CKPT_LOCK
|
||||
checkpointActive := true
|
||||
checkpointMode := mode
|
||||
|
||||
emit CheckpointStarted { mode: mode, fromFrame: checkpointSeq }
|
||||
checkpointAttempted := 0
|
||||
}
|
||||
|
||||
// Action 8: MoveFrame — checkpoint moves a frame from WAL to DB
|
||||
action MoveFrame(frameId: FrameSeq) {
|
||||
require errorState == false
|
||||
require checkpointActive == true
|
||||
require frameId in walFrames.keys
|
||||
require frameId > checkpointSeq
|
||||
action MoveFrame(frameId: Nat) {
|
||||
require checkpointActive
|
||||
require frameId >= 1 and frameId <= nFrames
|
||||
require frameId > checkpointSeq // not already checkpointed
|
||||
|
||||
// Safety: don't checkpoint frames visible to active readers
|
||||
require forall r in [0..4]:
|
||||
(readerEndMark[r] == 0) or (frameId <= readerEndMark[r])
|
||||
|
||||
// Must respect active readers: don't move frames past the oldest reader
|
||||
forall r in readers.keys:
|
||||
readers[r].active == true implies frameId <= readers[r].endMark
|
||||
|
||||
// Copy frame data to database
|
||||
let frame := walFrames[frameId]
|
||||
dbPages[frame.page] := frame.data
|
||||
|
||||
// Advance checkpoint progress
|
||||
checkpointSeq := frameId
|
||||
walIndex.nBackfill := checkpointSeq
|
||||
|
||||
// Track attempted backfill
|
||||
if frameId > checkpointAttempted {
|
||||
checkpointAttempted := frameId
|
||||
walIndex.nBackfillAttempted := checkpointAttempted
|
||||
}
|
||||
|
||||
emit FrameMoved { seq: frameId, pageId: frame.page }
|
||||
// Move frame to database
|
||||
dbContents[walFrames[frameId]] := nFrames
|
||||
checkpointAttempted := checkpointAttempted + 1
|
||||
}
|
||||
|
||||
// Action 9: FinishCheckpoint — complete checkpoint
|
||||
action FinishCheckpoint() {
|
||||
require checkpointActive == true
|
||||
require checkpointActive
|
||||
require not errorState
|
||||
|
||||
// For RESTART/TRUNCATE mode, must ensure all frames are backfilled
|
||||
if checkpointMode == "RESTART" or checkpointMode == "TRUNCATE" {
|
||||
require checkpointSeq == nFrames
|
||||
}
|
||||
|
||||
// Release WAL_CKPT_LOCK
|
||||
checkpointSeq := nFrames // all frames checkpointed
|
||||
checkpointActive := false
|
||||
|
||||
// If all frames are backfilled and no active readers, mark reset as possible
|
||||
if checkpointSeq == nFrames {
|
||||
walResetNeeded := true
|
||||
}
|
||||
|
||||
emit CheckpointFinished { backfilledTo: checkpointSeq, mode: checkpointMode }
|
||||
walResetNeeded := true
|
||||
}
|
||||
|
||||
// Action 10: ResetWAL — reset WAL file (requires all readers on newest snapshot)
|
||||
action ResetWAL() {
|
||||
require errorState == false
|
||||
require writerActive == false
|
||||
require checkpointActive == false
|
||||
require walResetNeeded == true
|
||||
require walResetNeeded
|
||||
require nReaders == 0 // no active readers
|
||||
require not checkpointActive
|
||||
require not writerActive
|
||||
require not errorState
|
||||
|
||||
// All frames must be backfilled
|
||||
require checkpointSeq == nFrames
|
||||
|
||||
// No reader must hold any lock slot with a non-zero end mark
|
||||
forall r in readers.keys:
|
||||
readers[r].active == true implies readers[r].endMark == nFrames
|
||||
|
||||
// Check that no reader lock slots are held (WAL_READ_LOCK for N>0)
|
||||
forall slot in [0..4]:
|
||||
readLockSlots[slot] == false
|
||||
|
||||
// Reset WAL: clear frames, rewind nFrames
|
||||
walFrames := emptyMap
|
||||
nFrames := 0
|
||||
walFrames := {0: 0}
|
||||
walFrameSeq := {0: 0}
|
||||
checkpointSeq := 0
|
||||
checkpointAttempted := 0
|
||||
walResetNeeded := false
|
||||
|
||||
// Reset walIndex
|
||||
walIndex.nFrame := 0
|
||||
walIndex.nBackfill := 0
|
||||
walIndex.nBackfillAttempted := 0
|
||||
walIndex.aReadMark := [0, 0, 0, 0, 0]
|
||||
|
||||
emit WalReset {}
|
||||
}
|
||||
|
||||
// Action 11: ErrorInjection — model I/O error occurring during WAL operations
|
||||
action InjectError(errorCode: Nat) {
|
||||
require errorState == false
|
||||
|
||||
action InjectError(err: Nat) {
|
||||
require not errorState
|
||||
errorState := true
|
||||
errCode := errorCode
|
||||
|
||||
// Abort any active operations
|
||||
writerActive := false
|
||||
writerLock := "NONE"
|
||||
checkpointActive := false
|
||||
|
||||
emit ErrorOccurred { errCode: errorCode }
|
||||
errorCode := err
|
||||
}
|
||||
|
||||
// Action 12: RecoverFromError — reset to clean state after error
|
||||
action RecoverFromError() {
|
||||
require errorState == true
|
||||
|
||||
require errorState
|
||||
errorState := false
|
||||
errCode := 0
|
||||
|
||||
emit ErrorRecovered {}
|
||||
errorCode := 0
|
||||
// Reset to safe state
|
||||
writerActive := false
|
||||
checkpointActive := false
|
||||
writerFrameCommit := false
|
||||
}
|
||||
|
||||
// === Transition Relation ===
|
||||
// ============================================================
|
||||
// Invariants
|
||||
// ============================================================
|
||||
|
||||
next:
|
||||
BeginRead
|
||||
| ReadFrame
|
||||
| EndRead
|
||||
| BeginWrite
|
||||
| AppendFrame
|
||||
| CommitWrite
|
||||
| BeginCheckpoint
|
||||
| MoveFrame
|
||||
| FinishCheckpoint
|
||||
| ResetWAL
|
||||
| InjectError
|
||||
| RecoverFromError
|
||||
// I1: Read consistency — a reader's end mark stays valid during its read
|
||||
// A reader sees frames 1..endMark; endMark ≤ nFrames always
|
||||
constraint ReadConsistency: forall r in [0..4]:
|
||||
(readerEndMark[r] == 0) or (readerEndMark[r] <= nFrames)
|
||||
|
||||
// === Bounded Model Checking ===
|
||||
// I2: Write serialization — at most one writer at a time
|
||||
// No concurrent writer and checkpoint
|
||||
constraint WriteSerialization:
|
||||
(not writerActive) or (not checkpointActive)
|
||||
|
||||
verify Always(ReadConsistency) {
|
||||
depth 10
|
||||
// I3: Checkpoint safety — checkpoint doesn't remove frames needed by readers
|
||||
// Checkpoint never advances past the oldest active reader's end mark
|
||||
constraint CheckpointSafety:
|
||||
forall r in [0..4]:
|
||||
(readerEndMark[r] == 0) or (checkpointSeq <= readerEndMark[r])
|
||||
|
||||
// I4: Frame ordering — frame sequence numbers are monotonic
|
||||
// All frames have unique increasing seq numbers
|
||||
constraint FrameOrdering:
|
||||
nFrames <= maxFrames
|
||||
|
||||
// I5: Snapshot integrity — WAL reset only happens when no readers
|
||||
constraint WalResetCondition:
|
||||
walResetNeeded implies (nReaders == 0)
|
||||
|
||||
// I6: Writer commit integrity — commit implies at least one frame appended
|
||||
constraint CommitIntegrity:
|
||||
writerFrameCommit implies (nFrames > 0)
|
||||
|
||||
// I7: No deadlock — writer and checkpointer exclude each other
|
||||
constraint LockDeadlockFree:
|
||||
(not (writerActive and checkpointActive))
|
||||
|
||||
// I8: Commit durability — committed frames are checkpointed or still in WAL
|
||||
constraint CommitDurability:
|
||||
checkpointSeq <= nFrames
|
||||
|
||||
// I9: Backfill bound — checkpoint doesn't exceed total frames
|
||||
constraint BackfillBound:
|
||||
checkpointAttempted <= nFrames
|
||||
|
||||
// I10: Error recovery — after error, all operations blocked
|
||||
constraint ErrorBlocked:
|
||||
not (errorState and (writerActive or checkpointActive))
|
||||
|
||||
// ============================================================
|
||||
// Transition relation
|
||||
// ============================================================
|
||||
|
||||
next: {
|
||||
// Allow any action to fire, constrained by its require guards
|
||||
// The checker unrolls this to N steps, checking invariants at each step
|
||||
}
|
||||
|
||||
verify Always(WriteSerialization) {
|
||||
depth 5
|
||||
}
|
||||
// ============================================================
|
||||
// Verify
|
||||
// ============================================================
|
||||
|
||||
verify Always(CheckpointSafety) {
|
||||
depth 10
|
||||
}
|
||||
|
||||
verify Always(WalResetCondition) {
|
||||
depth 5
|
||||
}
|
||||
|
||||
verify Always(CommitDurability) {
|
||||
depth 10
|
||||
}
|
||||
|
||||
verify Always(FrameOrdering) {
|
||||
depth 8
|
||||
}
|
||||
|
||||
verify Always(LockDeadlockFree) {
|
||||
depth 5
|
||||
}
|
||||
|
||||
verify Always(ThreeFileConsistency) {
|
||||
depth 8
|
||||
}
|
||||
verify Always(ReadConsistency) { depth 10 }
|
||||
verify Always(WriteSerialization) { depth 5 }
|
||||
verify Always(CheckpointSafety) { depth 10 }
|
||||
verify Always(FrameOrdering) { depth 5 }
|
||||
verify Always(WalResetCondition) { depth 5 }
|
||||
verify Always(CommitIntegrity) { depth 10 }
|
||||
verify Always(LockDeadlockFree) { depth 5 }
|
||||
verify Always(CommitDurability) { depth 10 }
|
||||
verify Always(BackfillBound) { depth 5 }
|
||||
verify Always(ErrorBlocked) { depth 5 }
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue