8b520284cb
#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.
267 lines
9.2 KiB
Text
267 lines
9.2 KiB
Text
speck SQLiteWAL {
|
|
// 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.
|
|
|
|
// --- 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 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
|
|
|
|
// 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 // 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 // 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
|
|
errorCode: Nat
|
|
}
|
|
|
|
init {
|
|
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
|
|
checkpointMode == 0
|
|
walResetNeeded == false
|
|
dbContents == {0: 0}
|
|
errorState == false
|
|
errorCode == 0
|
|
}
|
|
|
|
// ============================================================
|
|
// Actions
|
|
// ============================================================
|
|
|
|
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
|
|
}
|
|
|
|
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
|
|
}
|
|
|
|
action EndRead(readerId: Nat) {
|
|
require readerEndMark[readerId] > 0 // reader is active
|
|
require not errorState
|
|
|
|
readerEndMark[readerId] := 0
|
|
nReaders := nReaders - 1
|
|
}
|
|
|
|
action BeginWrite() {
|
|
require not writerActive
|
|
require not checkpointActive
|
|
require not errorState
|
|
require nFrames < maxFrames // room for at least one frame
|
|
|
|
writerActive := true
|
|
writerFrameCommit := false
|
|
}
|
|
|
|
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
|
|
|
|
nFrames := nFrames + 1
|
|
walFrames[nFrames] := pageId
|
|
walFrameSeq[nFrames] := nFrames
|
|
writerFrames[nFrames] := pageId
|
|
}
|
|
|
|
action CommitWrite() {
|
|
require writerActive
|
|
require not writerFrameCommit
|
|
require not errorState
|
|
|
|
writerFrameCommit := true
|
|
writerActive := false
|
|
}
|
|
|
|
action BeginCheckpoint(mode: Nat) {
|
|
require not checkpointActive
|
|
require not errorState
|
|
require mode >= 0 and mode <= 3 // valid mode
|
|
|
|
checkpointActive := true
|
|
checkpointMode := mode
|
|
checkpointAttempted := 0
|
|
}
|
|
|
|
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])
|
|
|
|
// Move frame to database
|
|
dbContents[walFrames[frameId]] := nFrames
|
|
checkpointAttempted := checkpointAttempted + 1
|
|
}
|
|
|
|
action FinishCheckpoint() {
|
|
require checkpointActive
|
|
require not errorState
|
|
|
|
checkpointSeq := nFrames // all frames checkpointed
|
|
checkpointActive := false
|
|
walResetNeeded := true
|
|
}
|
|
|
|
action ResetWAL() {
|
|
require walResetNeeded
|
|
require nReaders == 0 // no active readers
|
|
require not checkpointActive
|
|
require not writerActive
|
|
require not errorState
|
|
|
|
nFrames := 0
|
|
walFrames := {0: 0}
|
|
walFrameSeq := {0: 0}
|
|
checkpointSeq := 0
|
|
checkpointAttempted := 0
|
|
walResetNeeded := false
|
|
}
|
|
|
|
action InjectError(err: Nat) {
|
|
require not errorState
|
|
errorState := true
|
|
errorCode := err
|
|
}
|
|
|
|
action RecoverFromError() {
|
|
require errorState
|
|
errorState := false
|
|
errorCode := 0
|
|
// Reset to safe state
|
|
writerActive := false
|
|
checkpointActive := false
|
|
writerFrameCommit := false
|
|
}
|
|
|
|
// ============================================================
|
|
// Invariants
|
|
// ============================================================
|
|
|
|
// 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)
|
|
|
|
// I2: Write serialization — at most one writer at a time
|
|
// No concurrent writer and checkpoint
|
|
constraint WriteSerialization:
|
|
(not writerActive) or (not checkpointActive)
|
|
|
|
// 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
|
|
// ============================================================
|
|
|
|
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 }
|
|
}
|