mempool: formal specs in Quint and TLA+ of mempool with cache #800
Conversation
There was a problem hiding this comment.
The Quint specification is accurately following the golang codebase (mempool/reactor.go, mempool/clist_mempool.go) in a very nice and elegant manner.
In the few things, I would recommend to amend/add:
- asynchronous ABCI calls
- the behavior of consensus upon commit as in
state/execution.go - differentiate txs and txsMap (although this one is not really mandatory imho because
tx in txs iff tx in txsMap)
Would it be also possible to relate this specification to the high-level one which is in the knowledge base? (See here and PR#7.) There is also a refined version that includes caching.
| // block it created and rechecks outstanding txs. | ||
|
|
||
| // This node is not the proposer: take the block from the chain. | ||
| action BlockExecutor_MempoolUpdate_nonProposer(node) = all { |
There was a problem hiding this comment.
Strictly speaking, upon commit the following logic is applied: mempool.Lock, mempool.FlushAppConn, proxyApp.Commit, mempool.Update then mempool.Unlock. (See state/execution.go#Commit.) I wonder if it would be possible to follow exactly these steps.
There was a problem hiding this comment.
Right. I will add the following to the update actions, to make sure all ABCI requests are processed before updating.
require(node.ABCI::checkTxRequests().isEmpty()),
require(node.ABCI::recheckTxRequests().isEmpty()),
This won't make the flush-commit-update steps atomic, as when they are hold by the lock, but it will work.
| // Auxiliary variables | ||
| //-------------------------------------------------------------------------- | ||
| type Step = str | ||
| var _step: { node: NodeId, name: Step, args: str -> str } |
There was a problem hiding this comment.
Tracking which step was taken during a run is really nice (e.g., to understand why an invariant got broken). I wonder if this could be included as a feature in Quint.
|
|
||
| val noMempoolTx = { tx: "", height: 0, senders: Set() } | ||
|
|
||
| var mempool: NodeId -> Set[MempoolTx] |
There was a problem hiding this comment.
If we follow to the letter the codebase, then maybe add both txs and txsMap there.
There was a problem hiding this comment.
That would be a deeper level of abstraction. We would need also to refine Set[MempoolTx] to List[MempoolTx]. We will need to do it if we want to find if txs and txsMap are implemented correctly.
|
|
||
| /* The reactor sends at once a tx in the mempool to all its peers. */ | ||
| // [Reactor.broadcastTxRoutine]: https://github.com/CometBFT/cometbft/blob/5049f2cc6cf519554d6cd90bcca0abe39ce4c9df/mempool/reactor.go#L132 | ||
| action P2P_BroadcastTx(node: NodeId): bool = all { |
There was a problem hiding this comment.
Strictly speaking, there is no such atomic action in mempool/reactor.go.
There was a problem hiding this comment.
Initially I had a P2P_SendTx action but it introduced a lot of additional, unnecessary steps to the trace, one for each peer. Since each peer process the received message when they need to, it doesn't make any real difference to put the message in the peer's inbox all at once.
|
|
||
| val __Txs = Set("tx1", "tx2", "tx3", "tx4") | ||
|
|
||
| def __isValidAt(tx, h) = or { |
There was a problem hiding this comment.
Neat idea which permits to introduce some complexity in the execution of transactions at low cost.
There was a problem hiding this comment.
Yeah, though now that we agreed that CheckTx is not deterministic, this is not correct anymore 😅
| (rs) => rs.put(req, (senderId, h, resp))) | ||
|
|
||
| // For "Recheck" we send multiple requests at once. | ||
| action sendRequestRecheckTxs(nodeId, txs, h) = |
There was a problem hiding this comment.
If the end goal is to model the golang implementation, then I would go for asynchronous ABCI calls.
There was a problem hiding this comment.
This is another case that can be specified with a deeper level of abstraction.
|
Closing this PR as this work is moved to another repo and PR: cometbft/knowledge-base#11. Comments by @otrack are addressed there. Though this spec is certainly useful for eventually applying model-based testing, it's too tied to the v0 implementation, so we would need to keep it up to date with the changes in the code if we maintain it in this repo. |
Contributes to #614
PR checklist
.changelog(we use unclog to manage our changelog)docs/orspec/) and code comments