TLA models to reproduce SQLite's WAL bug and see whether dqlite is affected

README.md

Prerequisites

Install https://github.com/tlaplus/tlaplus manually or use the provided Dockerfile.

How to run the model-checker

If you are using the provided Dockerfile:

    docker build -t tlaplus:latest .
    docker run --user $(id -u):$(id -g) --rm -v $(pwd):/w tlaplus tlc2.TLC -config /w/<model>.cfg -cleanup -checkpoint 0 /w/<model>.tla

Or, if you installed tla manually:

    java -XX:+UseParallelGC -Xmx8G -cp /opt/tla/tla2tools.jar:/opt/tla/CommunityModules-deps.jar tlc2.TLC -config <model>.cfg -cleanup -checkpoint 0 <model>.tla

Dockerfile

FROM ubuntu:24.04

ENV TLA_HOME=/opt/tla \
    PATH=$PATH:/opt/tla

RUN apt-get update && apt-get install -y \
	default-jre \
    curl \
    && rm -rf /var/lib/apt/lists/*

RUN mkdir -p $TLA_HOME && \
    curl \
    -L https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar \
    -o $TLA_HOME/tla2tools.jar && \
	curl \
	-L https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
	-o $TLA_HOME/CommunityModules-deps.jar

# Volume that needs to be mounted from the outside.
WORKDIR /w
# Change -Xmx to increase memory for bigger depths.
ENTRYPOINT ["java", "-XX:+UseParallelGC", "-Xmx32G", "-cp", "/opt/tla/tla2tools.jar:/opt/tla/CommunityModules-deps.jar"]

dqlite.cfg

INVARIANTS
    NoPageIsLost

CONSTRAINTS
    WalLength
    DbLength

SPECIFICATION Spec

CONSTANTS
    Next <- DqliteNext
    CheckPointCopyHeader <- DqliteCheckPointCopyHeader

dqlite.tla

--------------------------------- MODULE dqlite ---------------------------------
EXTENDS Sequences, SequencesExt, TLC, sqlite

SQLITE == INSTANCE sqlite

DqliteCheckpointTakeLock ==
    /\ writeLock = "notTaken"
    /\ writeLock' = "takenForCheckpoint"
    /\ UNCHANGED << wal, db, nBackfill, mxFrame, pageNumber, checkPointState, safeMxFrame, walSalt, pWalSalt >>

DqliteCheckpointReleaseLock ==
    /\ writeLock = "takenForCheckpoint"
    /\ checkPointState = "notStarted"
    /\ writeLock' = "notTaken"
    /\ UNCHANGED << wal, db, nBackfill, mxFrame, pageNumber, checkPointState, safeMxFrame, walSalt, pWalSalt >>

DqliteCheckPointCopyHeader ==
    /\ writeLock = "takenForCheckpoint"
    /\ SQLITE!CheckPointCopyHeader

DqliteNext ==
    \/ DqliteCheckpointTakeLock
    \/ DqliteCheckpointReleaseLock
    \/ SQLITE!Next

===============================================================================

sqlite.cfg

INVARIANTS
    NoPageIsLost

CONSTRAINTS
    WalLength
    DbLength

SPECIFICATION Spec

sqlite.tla

--------------------------------- MODULE sqlite ---------------------------------
EXTENDS Sequences, SequencesExt, TLC

\* files
VARIABLE wal
VARIABLE db

\* wal-index variables:
VARIABLE nBackfill
VARIABLE mxFrame
\* We will only capture the sequential part of the salt.
VARIABLE walSalt
----

\* Lock needed to write to the WAL.
VARIABLE writeLock

\* Generator for new different pages. This variable is not needed but it is
\* helpful for debugging.
VARIABLE pageNumber

\* checkpoint variables:
\* It is set using a copy of the wal-index header (pWal->hdr.mxFrame) when
\* starting the checkpoint.
VARIABLE safeMxFrame
\* It is set using a copy of the wal-index header (pWal->aSalt) when
\* starting the checkpoint.
VARIABLE pWalSalt
\* Running a checkpoint will move the state:
\*    notStarted -> copiedHeader -> waitingForLock -> (finished) -> notStarted
\* Note that only one checkpoint can happen at a time, which is why this is a
\* global variable and that appends can happen concurrently with checkpoints,
\* the exclusion zones correspond to our atomic actions.
VARIABLE checkPointState
----

checkpoint_vars == << checkPointState, safeMxFrame, pWalSalt >>
vars == << wal, db, nBackfill, mxFrame, pageNumber, checkPointState, safeMxFrame, walSalt, pWalSalt, writeLock >>

WalAppendTakeLock ==
    /\ writeLock = "notTaken"
    /\ writeLock' = "takenForAppend"
    /\ UNCHANGED << wal, db, nBackfill, mxFrame, pageNumber, checkPointState, safeMxFrame, walSalt, pWalSalt >>

WalAppend ==
    /\ writeLock = "takenForAppend"
    \* The if condition is written as an assert in the sqlite code because
    \* checking for pWal->readLock == 0 gives us the same guarantee. If the
    \* writer has taken the read lock at 0 it means there are no frames in the
    \* wal that were not checkpointed.
    /\ IF (nBackfill > 0 /\ mxFrame = nBackfill)
       THEN
        \* Restart the Wal and Append.
        \* We don't have readers so every writer after a checkpoint will
        \* restart the wal.
        /\ wal' = <<pageNumber>>
        /\ mxFrame' = 1
        /\ nBackfill' = 0
        /\ walSalt' = walSalt + 1
       ELSE
        /\ wal' = Append(wal, pageNumber)
        /\ mxFrame' = mxFrame + 1
        /\ UNCHANGED << nBackfill, walSalt >>
    /\ pageNumber' = pageNumber + 1
    /\ writeLock' = "notTaken"
    /\ UNCHANGED << db, checkpoint_vars >>

CheckPointCopyHeader ==
    /\ checkPointState = "notStarted"
    /\ safeMxFrame' = mxFrame
    /\ pWalSalt' = walSalt
    /\ checkPointState' = "copiedHeader"
    /\ UNCHANGED << wal, nBackfill, db, mxFrame, pageNumber, walSalt, writeLock >>

StartCheckpoint ==
    /\ checkPointState = "copiedHeader"
    \* Important: here backfill is read from the live header while safeMxFrame
    \* is read from the stale copy of the header.
    /\ IF nBackfill < safeMxFrame
       THEN checkPointState' = "waitingForLock"
       ELSE checkPointState' = "notStarted"
    /\ UNCHANGED << wal, nBackfill, db, mxFrame, pageNumber, safeMxFrame, walSalt, pWalSalt, writeLock >>

Checkpoint ==
    /\ checkPointState = "waitingForLock"
    \* Move pages from wal into db.
    /\ db' = db \cup { wal[j] : j \in nBackfill+1..Len(wal) }
    /\ nBackfill' = safeMxFrame
    \* Reset the checkpoint state.
    /\ safeMxFrame' = 0
    /\ pWalSalt' = 0
    /\ checkPointState' = "notStarted"
    /\ UNCHANGED << mxFrame, wal, pageNumber, walSalt, writeLock >>

Init ==
    /\ wal = <<>>
    /\ db = {}
    /\ nBackfill = 0
    /\ mxFrame = 0
    /\ pageNumber = 1
    /\ safeMxFrame = 0
    /\ walSalt = 0
    /\ pWalSalt = 0
    /\ writeLock = "notTaken"
    /\ checkPointState = "notStarted"

Next ==
    \/ WalAppendTakeLock
    \/ CheckPointCopyHeader
    \/ StartCheckpoint
    \/ Checkpoint
    \/ WalAppend

Spec == Init /\ [][Next]_vars

\* Invaritants:
NoPageIsLost ==
    \A f \in 1..Cardinality(db) : f \in db

\* Constraints to bound the model to finish quickly.
WalLength == Len(wal) <= 10
DbLength == Cardinality(db) <= 10

===============================================================================

sqlite_fixed.cfg

INVARIANTS
    NoPageIsLost

CONSTRAINTS
    WalLength
    DbLength

SPECIFICATION Spec

sqlite_fixed.tla

--------------------------------- MODULE sqlite_fixed ---------------------------------
EXTENDS Sequences, SequencesExt, TLC

\* files
VARIABLE wal
VARIABLE db

\* wal-index variables:
VARIABLE nBackfill
VARIABLE mxFrame
\* We will only capture the sequential part of the salt.
VARIABLE walSalt
----

\* Lock needed to write to the WAL.
VARIABLE writeLock

\* Generator for new different pages. This variable is not needed but it is
\* helpful for debugging.
VARIABLE pageNumber

\* checkpoint variables:
\* It is set using a copy of the wal-index header (pWal->hdr.mxFrame) when
\* starting the checkpoint.
VARIABLE safeMxFrame
\* It is set using a copy of the wal-index header (pWal->aSalt) when
\* starting the checkpoint.
VARIABLE pWalSalt
\* Running a checkpoint will move the state:
\*    notStarted -> copiedHeader -> waitingForLock -> (finished) -> notStarted
\* Note that only one checkpoint can happen at a time, which is why this is a
\* global variable and that appends can happen concurrently with checkpoints,
\* the exclusion zones correspond to our atomic actions.
VARIABLE checkPointState
----

checkpoint_vars == << checkPointState, safeMxFrame, pWalSalt >>
vars == << wal, db, nBackfill, mxFrame, pageNumber, checkPointState, safeMxFrame, walSalt, pWalSalt, writeLock >>

WalAppendTakeLock ==
    /\ writeLock = "notTaken"
    /\ writeLock' = "takenForAppend"
    /\ UNCHANGED << wal, db, nBackfill, mxFrame, pageNumber, checkPointState, safeMxFrame, walSalt, pWalSalt >>

WalAppend ==
    /\ writeLock = "takenForAppend"
    \* The if condition is written as an assert in the sqlite code because
    \* checking for pWal->readLock == 0 gives us the same guarantee. If the
    \* writer has taken the read lock at 0 it means there are no frames in the
    \* wal that were not checkpointed.
    /\ IF (nBackfill > 0 /\ mxFrame = nBackfill)
       THEN
        \* Restart the Wal and Append.
        \* We don't have readers so every writer after a checkpoint will
        \* restart the wal.
        /\ wal' = <<pageNumber>>
        /\ mxFrame' = 1
        /\ nBackfill' = 0
        /\ walSalt' = walSalt + 1
       ELSE
        /\ wal' = Append(wal, pageNumber)
        /\ mxFrame' = mxFrame + 1
        /\ UNCHANGED << nBackfill, walSalt >>
    /\ pageNumber' = pageNumber + 1
    /\ writeLock' = "notTaken"
    /\ UNCHANGED << db, checkpoint_vars >>

CheckPointCopyHeader ==
    /\ checkPointState = "notStarted"
    /\ safeMxFrame' = mxFrame
    /\ pWalSalt' = walSalt
    /\ checkPointState' = "copiedHeader"
    /\ UNCHANGED << wal, nBackfill, db, mxFrame, pageNumber, walSalt, writeLock >>

StartCheckpoint ==
    /\ checkPointState = "copiedHeader"
    \* Important: here backfill is read from the live header while safeMxFrame
    \* is read from the stale copy of the header.
    /\ IF nBackfill < safeMxFrame
       THEN checkPointState' = "waitingForLock"
       ELSE checkPointState' = "notStarted"
    /\ UNCHANGED << wal, nBackfill, db, mxFrame, pageNumber, safeMxFrame, walSalt, pWalSalt, writeLock >>

Checkpoint ==
    /\ checkPointState = "waitingForLock"
    /\ IF walSalt = pWalSalt
       THEN
        \* Move pages from wal into db.
        /\ db' = db \cup { wal[j] : j \in nBackfill+1..Len(wal) }
        /\ nBackfill' = safeMxFrame
       ELSE
        \* Salt changed, we skip the checkpoint.
        /\ UNCHANGED << nBackfill, db >>
    \* Reset the checkpoint state.
    /\ safeMxFrame' = 0
    /\ pWalSalt' = 0
    /\ checkPointState' = "notStarted"
    /\ UNCHANGED << mxFrame, wal, pageNumber, walSalt, writeLock >>

Init ==
    /\ wal = <<>>
    /\ db = {}
    /\ nBackfill = 0
    /\ mxFrame = 0
    /\ pageNumber = 1
    /\ safeMxFrame = 0
    /\ walSalt = 0
    /\ pWalSalt = 0
    /\ writeLock = "notTaken"
    /\ checkPointState = "notStarted"

Next ==
    \/ WalAppendTakeLock
    \/ CheckPointCopyHeader
    \/ StartCheckpoint
    \/ Checkpoint
    \/ WalAppend

Spec == Init /\ [][Next]_vars

\* Invaritants:
NoPageIsLost ==
    \A f \in 1..Cardinality(db) : f \in db

\* Constraints to bound the model to finish quickly.
WalLength == Len(wal) <= 10
DbLength == Cardinality(db) <= 10

===============================================================================