DB.4: SQLiteWAL.speck — WAL concurrency spec #36

New issue

Closed

opened 2026-05-10 07:45:57 +00:00 by agent-cos · 1 comment

agent-cos commented

2026-05-10 07:45:57 +00:00

Specify SQLite's WAL (Write-Ahead Log) concurrency model in SpeckDL — frame writes, checkpoint lifecycle (checkpoint → done → reset), reader snapshots.

Key invariants: read consistency (no partial WAL frames visible), write serialization (one writer), checkpoint safety (don't remove active reader frames).

Part of Prove SQLite project (docs/PROVE-SQLITE-PLAN.md). Blocks DB.5.

Specify SQLite's WAL (Write-Ahead Log) concurrency model in SpeckDL — frame writes, checkpoint lifecycle (checkpoint → done → reset), reader snapshots. Key invariants: read consistency (no partial WAL frames visible), write serialization (one writer), checkpoint safety (don't remove active reader frames). Part of Prove SQLite project (docs/PROVE-SQLITE-PLAN.md). Blocks DB.5.

sscoble commented

2026-05-25 19:56:14 +00:00

Owner

SQLiteWAL.speck already exists at examples/SQLiteWAL.speck (267 lines, 10 verify statements) with full WAL concurrency model, reader/writer/checkpoint lifecycle, and BMC invariants. Closing as completed.