Model max_uncommitted_tx_count of raft.h in abs.tla

[lemmy]

Align spec with CCF by replacing global upper bound MaxLogLength with MaxUncommittedCount (see max_uncommitted_tx_count in raft.h) that restricts the length by which a log may be extended in each step.

These two commits were previously part of #6475. @heidihoward approved them in #6475 (comment).

[achamayou]

This constraint is too simplistic, and does not accurately represent what max uncommitted tx count does.

The current behaviour is that new user and governance transactions are rejected, but signatures and nodes frontend transactions (joins, jwt refresh...) do not count towards that limit. Applying that cap to the overall committed growth per step is incorrect.

I can see that it is necessary to have a cap for model checking to work, but conflating it with max uncommitted tx is not accurate, and may result in confusion and trace validation failures.

[lemmy]

This constraint is too simplistic, and does not accurately represent what max uncommitted tx count does.

The current behaviour is that new user and governance transactions are rejected, but signatures and nodes frontend transactions (joins, jwt refresh...) do not count towards that limit. Applying that cap to the overall committed growth per step is incorrect.

The documentation of max_uncommitted_tx_count documentation could mention this behavior:

"Maximum number of uncommitted transactions allowed before the primary refuses new transactions. Unlimited if set to 0."

Regarding ccfraft, is it correct to assume that max_uncommitted_tx_count applies to TypeEntry, but does not apply to TypeSignature, TypeReconfiguration, or TypeRetired?

I can see that it is necessary to have a cap for model checking to work, but conflating it with max uncommitted tx is not accurate, and may result in confusion and trace validation failures.

Actually, unbounded sequences create one less constraint in the (pending) axiomatic definitions in abs.tla.

[lemmy]

Implementation-level issues and PRs:
#5692
#3871
#5690

[achamayou]

I'll improve the documentation, but it is not always safe to seize a sentence in the documentation and turn it into a property.

Regarding ccfraft, is it correct to assume that max_uncommitted_tx_count applies to TypeEntry, but does not apply to TypeSignature, TypeReconfiguration, or TypeRetired?

No, there at least two write transactions that commonly happen on the node frontend, and would be TypeEntry as far as the TV is concerned: join transactions (nodes becoming PENDING, a necessary pre-requisite to a TypeReconfiguration that ccfraft does not model), and JWT refresh transactions. In addition, some ledgers will have host subprocess and ACME client transactions, but that depends on the configuration.

The spec would need to be substantially more detailed to capture this correctly, but we already struggle to get useful model checking at the current level of detail, so I am very skeptical of going in that direction.

Actually, unbounded sequences create one less constraint in the (pending) axiomatic definitions in abs.tla.

Great, let's get this of this constraint then. No point having something that's both inaccurate and slows down the model checking.

[lemmy]

Actually, unbounded sequences create one less constraint in the (pending) axiomatic definitions in abs.tla.

Great, let's get this of this constraint then. No point having something that's both inaccurate and slows down the model checking.

#6509