Skip to content

Fix rollback-handling in consistency trace validation #8133

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Amaury Chamayou (achamayou) merged 9 commits into from
Aug 19, 2026
+61 −1
Merged

Fix rollback-handling in consistency trace validation #8133

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
c36bb6e
Fix consistency trace rollback backfill
achamayou Aug 8, 2026
5a7dc5b
Explain synthetic rollback trace
achamayou Aug 8, 2026
31c04cd
Expand consistency election traces
achamayou Aug 8, 2026
86d3fe2
Merge branch 'main' into achamayou-fix-consistency-trace-rollback
achamayou Aug 10, 2026
63faa99
Merge branch 'main' into achamayou-fix-consistency-trace-rollback
achamayou Aug 11, 2026
e434c6e
Merge branch 'main' into achamayou-fix-consistency-trace-rollback
achamayou Aug 12, 2026
1213fd1
Merge branch 'main' into achamayou-fix-consistency-trace-rollback
achamayou Aug 12, 2026
1d0565f
Merge branch 'main' into achamayou-fix-consistency-trace-rollback
achamayou Aug 19, 2026
fbda6b1
Merge branch 'main' into achamayou-fix-consistency-trace-rollback
achamayou Aug 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions .github/workflows/ci-verification.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,16 @@ jobs:
- run: cd tla && ./tlc.py mc consistency/MCMultiNode.tla
- run: cd tla && ./tlc.py mc consistency/MCMultiNodeReads.tla
- run: cd tla && ./tlc.py mc consistency/MCMultiNodeReadsAlt.tla
# These traces are hard-coded because generating rollbacks requires a
# partitions test, where election and transaction timing are difficult
# to control deterministically.
- name: Validate consistency election traces
run: |
cd tla
for trace in consistency/traces/*.ndjson; do
echo "Validating ${trace}"
JSON="${trace}" ./tlc.py --workers 1 tv --disable-dfs consistency/TraceMultiNodeReads.tla
done

- name: Upload TLC traces
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
Expand Down
9 changes: 8 additions & 1 deletion tla/consistency/TraceMultiNodeReads.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -160,8 +160,15 @@ BackfillLedgerBranches ==
\* Similar to TruncateLedgerAction, but only advances the view
/\ LET view == logline.tx_id[1]
seqno == logline.tx_id[2]
sourceBranch == Last(ledgerBranches)
prefixLength == Min({seqno - 1, Len(sourceBranch)})
IN /\ Len(ledgerBranches) < view
/\ ledgerBranches' = Append(ledgerBranches, Last(ledgerBranches))
\* A new primary may reuse seqno after rolling back an uncommitted
\* suffix. Copying that suffix would prevent the logged transaction
\* from occupying seqno in the new view.
/\ ledgerBranches' = Append(
ledgerBranches,
SubSeq(sourceBranch, 1, prefixLength))
/\ UNCHANGED history

TraceNext ==
Expand Down
8 changes: 8 additions & 0 deletions tla/consistency/traces/election_no_rollback.ndjson
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":0}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":0,"tx_id":[2,10]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":0,"tx_id":[2,10]}
{"action":"StatusCommittedResponseAction","type":"TxStatusReceived","tx_id":[2,10],"status":"CommittedStatus"}
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":1}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":1,"tx_id":[3,11]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":1,"tx_id":[3,11]}
{"action":"StatusCommittedResponseAction","type":"TxStatusReceived","tx_id":[3,11],"status":"CommittedStatus"}
8 changes: 8 additions & 0 deletions tla/consistency/traces/election_non_contiguous_view.ndjson
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":0}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":0,"tx_id":[2,10]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":0,"tx_id":[2,10]}
{"action":"StatusCommittedResponseAction","type":"TxStatusReceived","tx_id":[2,10],"status":"CommittedStatus"}
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":1}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":1,"tx_id":[5,11]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":1,"tx_id":[5,11]}
{"action":"StatusCommittedResponseAction","type":"TxStatusReceived","tx_id":[5,11],"status":"CommittedStatus"}
11 changes: 11 additions & 0 deletions tla/consistency/traces/rollback_same_seqno.ndjson
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":0}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":0,"tx_id":[2,10]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":0,"tx_id":[2,10]}
{"action":"StatusCommittedResponseAction","type":"TxStatusReceived","tx_id":[2,10],"status":"CommittedStatus"}
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":1}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":1,"tx_id":[2,11]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":1,"tx_id":[2,11]}
{"action":"StatusInvalidResponseAction","type":"TxStatusReceived","tx_id":[2,11],"status":"InvalidStatus"}
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":2}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":2,"tx_id":[3,11]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":2,"tx_id":[3,11]}
16 changes: 16 additions & 0 deletions tla/consistency/traces/rollback_two_transactions.ndjson
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":0}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":0,"tx_id":[2,10]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":0,"tx_id":[2,10]}
{"action":"StatusCommittedResponseAction","type":"TxStatusReceived","tx_id":[2,10],"status":"CommittedStatus"}
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":1}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":1,"tx_id":[2,11]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":1,"tx_id":[2,11]}
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":2}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":2,"tx_id":[2,12]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":2,"tx_id":[2,12]}
{"action":"StatusInvalidResponseAction","type":"TxStatusReceived","tx_id":[2,11],"status":"InvalidStatus"}
{"action":"StatusInvalidResponseAction","type":"TxStatusReceived","tx_id":[2,12],"status":"InvalidStatus"}
{"action":"RwTxRequestAction","type":"RwTxRequest","tx":3}
{"action":"RwTxExecuteAction","type":"RwTxExecute","tx":3,"tx_id":[3,11]}
{"action":"RwTxResponseAction","type":"RwTxResponse","tx":3,"tx_id":[3,11]}
{"action":"StatusCommittedResponseAction","type":"TxStatusReceived","tx_id":[3,11],"status":"CommittedStatus"}