Re: [tlaplus] Liveness check with at least once message delivery

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Adding to this reply, I think it is important to be clear about what you want to verify. TLC returns a counter-example to <>TransferComplete (or []<>TransferComplete) that shows how it is possible that the sum of balances is never 2 because at all points there is some wire transfer being transmitted. As pointed out below, you can check that this property holds, assuming that the network is periodically empty.

However, perhaps the property is just too strong, and it would be more reasonable to check that every transfer is eventually performed. In order to express this, you probably want to add IDs to wire transfers in order to distinguish two transfers between the same two agents with the same amount.

Finally, your fairness property is quite weak because it only assumes that some transfer will be performed as long as there is some pending transfer. This would still allow the system to never perform some specific pending transfer. Again, assuming that transfers carry a unique ID, you could write

DepositWireTransfer(id) == …

and assert the fairness property

\A id \in ID : WF_vars(DepositWireTransfer(id))

The problem with using IDs is that you’ll have to bound the set of IDs for model checking and will then run out of IDs at some point.

Finally, you use a sequence for representing the pending transfers but allow them to be performed in any order. Using a (multi-)set instead of a sequence gives you an unordered structure and may reduce the size of the state space that TLC computes.

Hope this helps,

Stephan

On Apr 10, 2024, at 08:40, divyanshu ranjan <idivyanshu.ranjan@xxxxxxxxx> wrote:

It is not clear to me what liveness property is being checked here, sorry if I have missed it. I am assuming it is  []<>TransferComplete, given that

I am able to get a similar trace as shown in the message.

As I understand you want only system behaviour in which every message is processed and adding strong or weak fairness on DepositWireTransfer

doesn't achieve it.

For this particular example one thing that can be tried is change spec to

EmptyNetwork == wire_requests = <<>>
Spec == /\ Init
        /\ [][Next]_<<balances, wire_requests>>
        /\ WF_wire_requests(DepositWireTransfer)
        /\ [](wire_requests /= <<>> => <>EmptyNetwork)

which constrains behavior to if the network is not empty eventually it will be empty (all messages are processed).

I am not sure if this is machine closed spec or not.  Better thing to do would be check following property

Prop == [](wire_requests /= <<>> => <>EmptyNetwork) => []<>TransferComplete

Regards

Divyanshu Ranjan

On Wed, Apr 10, 2024 at 5:48 AM jayaprabhakar k <jayaprabhakar@xxxxxxxxx> wrote:

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?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CA%2Bt%3DSiJW9BskRavnF3Yu6%3DTUqJx2kBrvqEZfH6YMYko8-o-91g%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAL9hw25iQdZZRU7K%2BxAgQvemiSaJZP5dsv1VrMzy0T%2BEh3x-YQ%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/EC54437A-BE72-4A65-9D78-AD9EB44C0103%40gmail.com.