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
On Thursday, 6 January 2022 at 10:49:54 UTC-3 Jones Martins wrote:
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
On Tuesday, 30 November 2021 at 15:04:31 UTC-3 Jones Martins wrote:
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
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
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
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
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
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
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
--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/5084e198-9a83-4961-bc96-c4cc287e07dbn%40googlegroups.com.
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...@xxxxxxxxxxxxxxxx.