Adding note to TLA+ spec on message ordering assumptions (#5613)

microsoft · Sep 5, 2023 · ff4402c · ff4402c
1 parent f6e0e34
commit ff4402c
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla
@@ -153,6 +153,8 @@ ReconfigurationVarsTypeInv ==
 \* to another. With CCF, we have message integrity and can ensure unique messages.
 \* Messages only records messages that are currently in-flight, actions should
 \* removed messages once received.
+\* We model messages as a single (unsorted) set and do not assume ordered message delivery between nodes.
+\* Node-to-node channels use TCP but out-of-order delivery could be observed due to reconnection or a malicious host.
 VARIABLE messages
 
 Messages ==