Update and expand the TLA+ model - #216
Conversation
The model previously didn't include the committed offset according to replicas / followers. Adding this is necessary to later cover retention or consumer behaviors.
TLA 1.8 flags a deadlock as an error. A deadlock can happen because the model allows all replicas to stop. We could alternatively prevent this structurally by ensuring that one replica is always online, but this doesn't seem realistic in practice, since a cluster may realistically go fully offline and recover gracefully.
Some variables were marked as UNCHANGED but were assigned anyways. This logs a warning when running. It also constrains the model to not consider states where the variable can change.
|
Found some extra issues with TLA+ 1.8.0 around the dead-locking behavior. The message of Tested again for an hour on an |
|
thanks, does this model match what we actually do with the coordinator in RabbitMQ? |
|
Not quite. The coordinator has a fencing request mechanism here which I don't think matches the coordinator today very faithfully. I think we could match the server more faithfully if we swap the The new work here mainly adds retention and replication of the committed offset. |
2 participants
I was taking a look through the model to try to extend it for rabbitmq-stream-s3. The diff looks pretty large since I flattened the directory but the commit history lays out each change.
I added replication of commit offset and retention to the model as well. I tested this for 20-30 min on an
hpc7a.96xlarge(192 cores) and didn't find any violations.