Guarantee message passing

[Jones Martins]

Hello everyone,

Sorry for keeping this too abstract. I may give an example later on if necessary.

In a process communication network, is there any way to guarantee a process to respond to some message immediately (or as soon as possible) after receiving it?

I'm dealing with timeouts, but I'm modelling a system with perfect communication (there are no delays, no lost messages). Since there are no delays, we expect other processes to respond immediately. I tried to add Strong Fairness to this "Respond" action, but it still does not guarantee anything.

Regards,

Jones

[Stephan Merz]

A process reacting immediately to a received message is a safety property, so this should be specified as part of the next-state relation, along the lines of

Act(p) == \E q \in Procs : \E msg \in msgs[q,p] :

  /\ msgs' = [msgs EXCEPT ![q,p] = @ \ {msg},

                          ![p,q] = @ \cup Answer(p, q, msg)]

  /\ ... \* update of local variables

assuming that msgs is a two-dimensional array containing the messages in transit between processes.

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5084e198-9a83-4961-bc96-c4cc287e07dbn%40googlegroups.com.

[Jones Martins]

Hello Stephen,

I see. It's a safety property. I was worried sending and receiving a message in the same step would be incorrect in a more... concrete specification (closer to programming languages). My thinking was more in line of "how do I guarantee the next step will be a Reply step from some process after a Send step?" So it seems, in idealized networking conditions, I should Send and Receive in the same step.

Thanks,

Jones

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/Pq2V5769DTs/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/A9F2B199-99B3-4607-BC33-E32C2747E756%40gmail.com.

[Andrew Helwer]

One way of modeling this is as a real-time system, with upper-bound and lower-bound timers. See Leslie's paper Real Time is Really Simple.

Andrew

[Jones Martins]

Hi, Andrew

I read Leslie's paper and thought about it for a while. I'm now trying to implement its concepts in my system. By adding a timeout, it would still be possible for a process to timeout, which I don't want in this case. Since I'm implementing a system with no delays (unless no one is active), I think I should specify it as Send and Receive in the same action, as Stephan said.

Now I have another question: couldn't I guarantee immediate responses in a "Send(p) and Reply(p)" system (instead of the "Act(p)" system) by adding Strong Fairness to the Reply action?

Jones

[Stephan Merz]

Fairness conditions are about what must happen in the limit, they do not express urgency. If you want to separate your receive and reply events and still require that the reply happens before the receiver performs some other actions, you'll want to explicitly block these actions and write, say,

Receive(p) == \E q \in Procs : \E msg \in msgs[q,p] :

  /\ pendingReply[p] = None

  /\ msgs' = [msgs EXCEPT ![q,p] = @ \ {msg}]

  /\ pendingReply' = [pendingReply EXCEPT ![p] = msg]

  /\ ...

Reply(p) ==

  /\ pendingReply[p] # None

  /\ msgs' = [msgs EXCEPT ![p,q] = @ \union {Answer(p, pendingReply[p])}]

  /\ pendingReply' = [pendingReply EXCEPT ![p] = None]

  /\ ...

and add the precondition "pendingReply[p] = None" to all actions of process p that you wish to block.

This is a simplified version of the timeout that Andrew suggested with an immediate deadline.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d6da9462-5453-4be3-9d8f-e44de62f4741n%40googlegroups.com.

[Jones Martins]

Thank you so much, Stephan. That's a simple and super-effective solution.

I believe timeouts will be useful when I remove urgency from my model, since I don't want anything to timeout currently.

Jones

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1F386F05-54AB-4153-9EFC-AA59AAF38DDF%40gmail.com.

[Andrew Helwer]

Just because you add timeouts in your spec doesn't mean it's possible for a process to timeout (unless you want that); if you look at the implementation of the Tick operator which advances time, it will only advance by some quantity if advancing doesn't cause an upper-bound timer to reach zero. This is equivalent to encoding an assumption in your system that no process will ever timeout.

Of course if later you want to model timeout failures that is also easy to do; you just modify the Tick operator.

Andrew

[Jones Martins]

Hi Andrew,

That wasn't clear to me, then. I thought it was just a standard procedure for real-time spec actions to be enabled.

After thinking about Stephen's new solution, I believe timeouts are the way to go…

"Pending messages" in a spec where processes can deactivate at any moment wouldn't work (as intended) since these messages wouldn't be answered immediately. So we get to a situation where we can't distinguish between delay and impossibility of sending in a spec that doesn't allow "impossibility of sending messages" when there are other active processes.

Thanks,

Jones

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/abf0103d-84dc-40d8-a0a9-c9c3bca82f04n%40googlegroups.com.

[Jones Martins]

Hi,

It seems the objective of the Tick action isn't to avoid timeouts, but to avoid the clock value to count to minus infinity.

Also, related to my first question, both of your solutions are working well together.

Thank you, Andrew and Stephan.

Jones

[Jones Martins]

Hello,

(I'm recycling this thread)

I have a question related to timers and their subsequent implementation. This might be useful for other specifications as well.

On Lamport's paper Real Time is Really Simple at page 38,  the action Tick of Leader contains two conditions before updating timers:

 - \A n \in Node: timer[n] + TODelay >= d

 - \A ms \in BagToSet(msgs): ms.rcvTimer >= d

Which both avoids timer and ms.rcvTimer from decreasing forever.

How would one implement such a clock in a programming language? Or rather, how would one check the program's clock respects the spec's clock?

I understand Tick must be Strongly Fair, so it ticks infinitely often. How can we ensure the program's clock behaves... well.

Maybe this sort of question -- checking implementation follows specification -- has already been replied elsewhere, so I appreciate outside sources just as well.

Best,

Jones

[Andrew Helwer]

You program's clock (or rather, your program itself) respects the invariants if it doesn't have any timeouts. The clock in the spec represents time itself.

Andrew