Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?

On Sun, Mar 10, 2019 at 4:25 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

Hello,

as you observed, both your fairness conditions ensure that the property that you are interested in holds, but they do so for quite different reasons. The first condition, which I'll write equivalently as

UnivFairSpec ==
/\ Spec
/\ \A self \in ProcSet : SF_vars(RETRY_BEGIN(self) /\ pc'[self] = "RETRY_SUCCEED")

asserts that every process that infinitely may succeed (i.e., move from BEGIN to SUCCEED) will succeed eventually.

The second condition,

ExistFairSpec ==
/\ Spec
/\ SF_vars(\E self \in ProcSet : RETRY_BEGIN(self) /\ pc'[self] = "RETRY_SUCCEED")

asserts that if infinitely often some process may succeed, then eventually some process will.

The two conditions are equivalent for your spec because processes that succeed terminate. In particular, the first process that succeeds will never move back to BEGIN. Now, the second process will continue looping and must therefore eventually succeed. (And clearly the "universal" condition implies the "existential" one.)

In order to make this more concrete, consider the variant below of your algorithm, where a process restarts after having succeeded. For this variant, the expected correctness property would be that both processes succeed infinitely often:

EveryProcessSucceeds == \A self \in ProcSet : []<>(succeeded[self])

You will see that this property holds with the "universal" fairness hypothesis, but not with the "existential" one, and TLC generates a counter-example where only one of the processes succeeds infinitely often.

Regards,
Stephan

(*--algorithm retry_example
variables
\* Both processes have not yet succeeded.
succeeded = [p \in 1..NumProcesses |-> FALSE];

define
all_succeeded == \A p \in 1..NumProcesses: succeeded[p]
end define;

fair process retry_example \in 1..NumProcesses
begin
RETRY_BEGIN:
either
RETRY_SUCCEED:
succeeded[self] := TRUE;
or
RETRY_ERROR:
goto RETRY_BEGIN;
end either;
RESTART:
succeeded[self] := FALSE;
goto RETRY_BEGIN;
end process;
end algorithm *)

On 9 Mar 2019, at 17:31, A. Jesse Jiryu Davis <jesse@xxxxxxxxxxxxxxx> wrote:

I've resumed playing with this spec and I'd like to check my understanding. I've added a TLA+ strong fairness formula as Leslie explained above, and that eliminates the deadlock error as expected. I think I've extended the idea to a 2-process spec but I want to make sure I'm still testing what I think I'm testing. The property I want to verify is something like, "Given the strong fairness property that each process eventually succeeds after some number of retries, all processes eventually succeed."

I'll show the PlusCal spec, the TLA+ translation, and then two ways of expressing the strong fairness property in TLA+. I think both ways are correct, but I'm very uncertain about them and I'd appreciate any comments.

EXTENDS Naturals, TLC
NumProcesses == 2
(*--algorithm retry_example
variables
  \* Both processes have not yet succeeded.
  succeeded = [p \in 1..NumProcesses |-> FALSE];

define
  all_succeeded == \A p \in 1..NumProcesses: succeeded[p]
end define;

fair process retry_example \in 1..NumProcesses
begin
  RETRY_BEGIN:
  either
  RETRY_SUCCEED:
  succeeded[self] := TRUE;
  or
  RETRY_ERROR:
  goto RETRY_BEGIN;
  end either;
end process;
end algorithm *)
\* BEGIN TRANSLATION
VARIABLES succeeded, pc

(* define statement *)
all_succeeded == \A p \in 1..NumProcesses: succeeded[p]
vars == << succeeded, pc >>
ProcSet == (1..NumProcesses)

Init == (* Global variables *)
  /\ succeeded = [p \in 1..NumProcesses |-> FALSE]
  /\ pc = [self \in ProcSet |-> "RETRY_BEGIN"]

RETRY_BEGIN(self) == /\ pc[self] = "RETRY_BEGIN"
     /\ \/ /\ pc' = [pc EXCEPT ![self] = "RETRY_SUCCEED"]
  \/ /\ pc' = [pc EXCEPT ![self] = "RETRY_ERROR"]
     /\ UNCHANGED succeeded

RETRY_SUCCEED(self) == /\ pc[self] = "RETRY_SUCCEED"
     /\ succeeded' = [succeeded EXCEPT ![self] = TRUE]
     /\ pc' = [pc EXCEPT ![self] = "Done"]

RETRY_ERROR(self) == /\ pc[self] = "RETRY_ERROR"
     /\ pc' = [pc EXCEPT ![self] = "RETRY_BEGIN"]
     /\ UNCHANGED succeeded

retry_example(self) == RETRY_BEGIN(self) \/ RETRY_SUCCEED(self)
  \/ RETRY_ERROR(self)

Next == (\E self \in 1..NumProcesses: retry_example(self))
     \/ (* Disjunct to prevent deadlock on termination *)
  ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars
  /\ \A self \in 1..NumProcesses : WF_vars(retry_example(self))

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

Here's the bit I'd like your help with. These are two ways to express "each process succeeds after some number of retries":

\* Hacky way
FairSpec == Spec /\ SF_vars(RETRY_BEGIN(1) /\ pc'[1] = "RETRY_SUCCEED") /\ SF_vars(RETRY_BEGIN(2) /\ pc'[2] = "RETRY_SUCCEED")
\* Nice way?
FairSpec == Spec /\ SF_vars(\E self \in ProcSet: RETRY_BEGIN(self) /\ pc'[self] = "RETRY_SUCCEED")

When I tell the Model Checker to check the FairSpec model, with either of these formulations, it works and terminates, and this temporal property is true:

<>[](all_succeeded)

Is what I'm doing correct?

Thank you!

On Sunday, February 24, 2019 at 3:53:47 PM UTC-5, A. Jesse Jiryu Davis wrote:
Indeed. I've found the sections of "Specifying Systems" I should read and I'll work up to them.

On Sat, Feb 23, 2019 at 7:20 PM Hillel Wayne <hwayne@xxxxxxxxx> wrote:
Another thing you can do is use the "leads to" operator (~>), where P ~> Q ≡ [](P => <>Q):
succeeded ~> accomplished_work
This is useful if you want to express that something might not ever succeed, but if it does, then you will eventually accomplish work.

I'd also recommend spending some time building an intuition for the difference between weak fairness and strong fairness.

H

On 2/23/19 10:10 AM, A. Jesse Jiryu Davis wrote:
Hello! I'm modeling a process that will retry indefinitely until it succeeds. A toy version of the process looks like:

variables
  succeeded = FALSE;

fair process retry_example = "retry_example"
begin
  RETRY_BEGIN:
  either
  RETRY_SUCCEED:
  succeeded := TRUE;
  or
  RETRY_ERROR:
  goto RETRY_BEGIN;
  end either;
end process;

Is there a useful way to test that such a process "eventually" succeeds? Right now, the following temporal property fails because the process could retry forever:

[]<>(succeeded)

It seems like I should be able to modify this spec so that TLC can check useful things about it. For example I could add a counter to the process, just for TLC's sake, that limits the number of times it fails.

Or I could assert that if it has ever succeeded at its first step, then it has accomplished some subsequent work:

variables
  succeeded = FALSE,
  accomplished_work = FALSE;

fair process retry_example = "retry_example"
begin
  RETRY_BEGIN:
  either
  RETRY_SUCCEED:
  succeeded := TRUE;
  DO_MORE_WORK:
  \* Imagine further steps between these lines.
  accomplished_work := TRUE;
  or
  RETRY_ERROR:
  goto RETRY_BEGIN;
  end either;

end process;

And then test this property, that if the process ever succeeded then it accomplished work:

<>[](succeeded => accomplished_work)

My general question is this: there are lots of algorithms that include indefinite retries, I'm curious how people test that they are correct, if there is a concept like "eventually succeeds" that can be tested with such specs?
--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.