999ce8fb75
Adjust the probabilities based on empirical data to achieve less uneven coverage of the action space during simulation ( #6562 )
...
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Co-authored-by: Amaury Chamayou <amaury@xargs.fr>
2024-10-15 16:05:10 +00:00
b96daa8d6a
Check high-level liveness properties in simulation mode ( #6545 )
...
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>
2024-10-09 11:47:03 +00:00
d7cf62f5e1
Strengthen various *TypeInvs by defining every function's domain. ( #6544 )
...
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>
2024-10-09 11:23:54 +00:00
9e7fb2d3b0
Limiting the terms reached by ProposeVote ( #6535 )
2024-10-07 21:05:46 +00:00
2d4f690869
Remove redefinitions of Terms in refinement mapping. ( #6533 )
...
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
2024-10-07 15:12:31 +00:00
c71b7ced76
Remove `StatsFile.tla` ( #6519 )
...
Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>
2024-10-03 09:31:22 +00:00
e0a9ea3757
Remove writing state-space statistics after the demise of cimetrics. ( #6518 )
...
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
2024-10-02 16:59:53 +00:00
76b2dcfacc
Check refinement of high-level spec abs with all models ( #6509 )
...
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>
2024-10-02 15:25:08 +00:00
0ab6408da1
Assert (postcondition) that all "debug invariants" equal true in at least one state. ( #6517 )
...
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>
2024-10-02 13:28:42 +00:00
50ffc62685
Iteration on TLC wrapper script ( #6513 )
...
Co-authored-by: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
2024-10-02 11:15:32 +00:00
df6d0043cf
Format Python under tla/ ( #6515 )
2024-10-01 15:39:22 +01:00
2069c68c8a
Minimize number of TLC configuration files. ( #6511 )
...
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
2024-09-30 09:35:32 +01:00
6fb0b5f0b9
Refactor abstract consensus specification ( #6475 )
...
* Refactor (simplify) TypeOK to use (more concise) Sequences!Seq operator.
* Define InitialLogs less explicitly.
* Add assumptions about abs.tla's constants (TLAPS will likely need those assumptions should we attempt writing a proof).
* Mitigate state-space explosion during explicit-state model checking by declaring constant Servers to be symmetric.
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
2024-09-26 17:50:50 -07:00
f798800ae9
Add 2-Node consensus MC ( #6504 )
2024-09-26 21:47:12 +01:00
5e615a9c97
Revert https://github.com/microsoft/CCF/pull/5939 ( #6501 )
...
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
2024-09-26 13:00:39 +01:00
c66cbb89b5
Adding an abstract consensus spec ( #6438 )
...
Co-authored-by: Markus Alexander Kuppe <github.com@lemmster.de>
2024-09-09 11:16:57 +00:00
01af78db24
Update TLA+ dev container to include new TLA+ vscode extension ( #6460 )
2024-09-04 14:18:38 +00:00
bf4fcff670
New definition of TxID ordered speculative linearizability ( #6185 )
2024-06-14 15:00:19 +00:00
d554f451ca
Typed model values in consensus spec ( #6229 )
2024-06-06 12:42:13 +00:00
b3d0eff367
Document lack of request payload validation in ctv ( #6187 )
2024-05-17 15:23:24 +01:00
cf8aadd054
Consensus tv todo cleanup ( #6186 )
2024-05-17 09:40:26 +00:00
5765fbdb55
Additional consistency invariant ( #6184 )
2024-05-16 23:36:22 +01:00
4eedf465d4
Spring clean consistency spec ( #6182 )
2024-05-16 17:26:50 +00:00
24690d1032
Tidy up TODOs in consistency spec ( #6181 )
2024-05-16 10:23:00 +00:00
62a6a1f625
Remove inapplicable TODO in ccfraft.tla ( #6180 )
2024-05-15 15:53:06 +00:00
f871978ad0
Only log start end of committable indices in trace ( #6172 )
2024-05-09 09:20:18 +01:00
5740fa4956
Document non-linearizability of read-only transactions in rare system condition ( #6167 )
2024-05-07 09:26:51 -07:00
86e88ca61e
Use typed model values to prevent bugs like 20d89bff16 in the future.
...
See relevant section in https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/model-values.html
2024-05-04 02:49:35 -07:00
d9c6c53077
CommittedRwSerializableInvAlt ==
...
\A i,j,k,l \in DOMAIN history:
\* Event k is the committed status received for the transaction in event i
/\ history[i].type = RwTxResponse
/\ history[k].type = TxStatusReceived
/\ history[k].status = CommittedStatus
/\ history[i].tx_id = history[k].tx_id
\* Event l is the committed status received for the transaction in event j
/\ history[j].type = RwTxResponse
/\ history[l].type = TxStatusReceived
/\ history[l].status = CommittedStatus
/\ history[j].tx_id = history[l].tx_id
=> \/ IsPrefix(history[i].observed, history[j].observed)
\/ IsPrefix(history[j].observed, history[i].observed)
CommittedRwSerializableInv ==
\A i, j \in RwTxResponseEventIndexes:
\A k, l \in CommittedEventIndexes:
\* Event k is the committed status received for the transaction in event i
/\ history[i].tx_id = history[k].tx_id
\* Event l is the committed status received for the transaction in event j
/\ history[j].tx_id = history[l].tx_id
=> \/ IsPrefix(history[i].observed, history[j].observed)
\/ IsPrefix(history[j].observed, history[i].observed)
THEOREM CommittedRwSerializableInv <=> CommittedRwSerializableInvAlt
BY DEF CommittedRwSerializableInv, RwTxResponseEventIndexes, CommittedEventIndexes, CommittedRwSerializableInvAlt
2024-05-03 13:44:34 -07:00
c681de7608
Optimize for TLC:
...
InvalidNotObservedByCommittedInvAlt ==
\A i, j, k, l \in DOMAIN history:
/\ history[i].type = RwTxResponse
/\ history[j].type = TxStatusReceived
/\ history[j].status = InvalidStatus
/\ history[k].type = RwTxResponse
/\ history[l].type = TxStatusReceived
/\ history[l].status = CommittedStatus
/\ history[k].tx_id = history[l]
/\ i # k
=> history[i].tx \notin ToSet(history[k].observed)
InvalidNotObservedByCommittedInv ==
\A i, k \in RwTxResponseEventIndexes:
i # k =>
\A j \in InvalidEventIndexes:
\A l \in CommittedEventIndexes:
history[k].tx_id = history[l]
=> history[i].tx \notin ToSet(history[k].observed)
THEOREM InvalidNotObservedByCommittedInv <=> InvalidNotObservedByCommittedInvAlt
BY DEF InvalidNotObservedByCommittedInv, RwTxResponseEventIndexes, InvalidEventIndexes, CommittedEventIndexes, InvalidNotObservedByCommittedInvAlt
2024-05-03 13:44:34 -07:00
71b626d25a
Bug: `InvalidNotObservedByCommittedInv` is vacuously true.
2024-05-03 13:44:34 -07:00
a01af25eed
Fix off by one in consistency tv ( #6154 )
2024-04-29 12:57:28 +01:00
dd2012f2e5
A trivial TLA+ loc counter ( #6152 )
2024-04-29 10:29:57 +01:00
cd8b8dddcb
Consistency Trace Validation: match transaction ids, take 2 ( #6143 )
2024-04-23 16:06:20 +01:00
88cffcb2e5
Enable both Invalid and Commit on the future of the head branch ( #6142 )
2024-04-23 11:09:33 +01:00
55d51b8f23
Parameterise consistency spec on FirstView ( #6140 )
2024-04-22 16:41:41 +01:00
fe19966a72
Fix comments in TMNR ( #6135 )
2024-04-19 14:40:06 +01:00
b3705d92bb
Consistency Spec Trace Validation ( #6124 )
2024-04-18 11:14:29 +01:00
b6320fcf8b
Adding signature txn to consistency spec ( #6129 )
2024-04-17 17:46:43 +01:00
c66745d838
Refactor Traceccfraft to reuse IsRequestVoteRequest. ( #6104 )
2024-03-29 21:36:44 +00:00
8ace4aa604
Reduce noise of TLAi linter. ( #6103 )
2024-03-28 09:31:26 +00:00
c572ce32a0
Fix regression in StatsFile.tla ( #6099 )
2024-03-26 21:22:41 -07:00
e02b97addf
Periodically dump low-overhead action coverage. ( #6093 )
2024-03-26 18:19:17 -07:00
67dd047dbc
Add TLAi linter. ( #6098 )
2024-03-26 17:10:54 -07:00
a078fc954b
Action and Variable coverage collection ( #6092 )
2024-03-25 22:10:13 +00:00
aa695a6b4a
Add action number plotting script ( #6074 )
2024-03-21 12:15:42 +00:00
daf99a8c66
Lower MaxTermLimit for Atomic Reconfig ( #6076 )
2024-03-19 14:56:57 +00:00
ed3995154b
TLA comment update ( #6069 )
2024-03-18 11:42:20 +00:00
91d6ea44cc
Adopt a consistent 'ing style in TLA+ ( #6068 )
2024-03-15 17:46:34 +00:00
3a6dd6a50a
Raft: Nodes stay active later during reconfiguration to ensure liveness ( #5973 )
2024-03-15 11:10:44 +00:00
Markus Alexander Kuppe
Heidi Howard
Amaury Chamayou