Hi,
I am trying to model a small example that relies on at-least once semantics of the message passing system. I am facing an issue on verifying liveness.
I even boiled down to the bare-bones version,
Sender initiates a WireRequest. It atomically deducts the sender's balance and posts a message.
On the receiving end, on seeing a message, it again atomically adds to the receiver's balance and marks the message as received. (I agree this is a massive simplification, but still couldn't get the liveness check to pass)
------
(* -- Initialization action -- *)
Init ==
/\ balances = [ Alice |-> 2, Bob |-> 0 ]
/\ wire_requests = <<>>
(* -- Helper function to compute total balance in accounts -- *)
GetTotals(accounts) == SumOfValues(accounts)
(* -- NoOverdraft assertion -- *)
NoOverdraft ==
/\ \A account \in DOMAIN balances : balances[account] >= 0
\*/\ balances["Bob"] > 0
(* -- TransferComplete assertion -- *)
TransferComplete ==
LET total == GetTotals(balances)
IN total = 2
(* -- Wire atomic action -- *)
StartWireTransfer ==
\E sender, receiver \in {"Alice", "Bob"} :
\E amount \in 1..2 :
IF sender /= receiver /\ balances[sender] >= amount
THEN
/\ balances' = [balances EXCEPT ![sender] = balances[sender] - amount]
/\ wire_requests' = Append(wire_requests, <<sender, receiver, amount>>)
ELSE
UNCHANGED <<balances,wire_requests>>
(* -- DepositWireTransfer fair action -- *)
DepositWireTransfer ==
\E i \in 1..Len(wire_requests) :
/\ balances' = [balances EXCEPT ![wire_requests[i][2]] = balances[wire_requests[i][2]] + wire_requests[i][3]]
/\ wire_requests' = Tail(wire_requests)
(* -- Next state relation -- *)
Next ==
\/ StartWireTransfer
\/ DepositWireTransfer
(* -- System specification -- *)
Spec == /\ Init
/\ [][Next]_<<balances, wire_requests>>
/\ WF_wire_requests(DepositWireTransfer)
------
This fails liveness with this trace.
<Screenshot 2024-04-09 at 5.03.57 PM.png>
Changing to Strong Fairness doesn't make a difference either.
This model should work as long as the message gets delivered at-least once AND the consumer does not ack the message unless they also credit the receiver. In real world implementation, we would have transaction id, persistent records, and periodic sync to ensure we didn't leave out a msg (due to some code bug) and so on.
I thought through various semantics and based on the semantics of fairness weak/strong, the liveness cannot be asserted.
The issue here is, weak fairness here implies, at least 1 message will be delivered at least once. But does not imply every message will be delivered at least once.
The only way to make the model checker pass seems to be, to atomically handle all the pending wire requests at once, that is not practical. If I try to model micro-batching, it would still fail.
How do others model applications that depend on at least once semantics of message passing?