[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: "A. Jesse Jiryu Davis" <jesse@xxxxxxxxxxxxxxx>*Date*: Sat, 9 Mar 2019 08:31:38 -0800 (PST)*References*: <15ade3f5-b044-4796-95dd-4d22c10963dc@googlegroups.com> <e4e19ec7-36c4-b22d-96d7-7a9a9ac6183a@gmail.com> <CAFRUCtYr2CwMZV3F6pR9OnrYCx4RZa1dN1=U9PsjEw57r9i0LQ@mail.gmail.com>

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."

On Sunday, February 24, 2019 at 3:53:47 PM UTC-5, A. Jesse Jiryu Davis wrote:

-- 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!

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 somethingmight notever 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@googlegroups.com .

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@googlegroups.com .

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.

**Follow-Ups**:

**References**:**[tlaplus] How to test a process eventually succeeds after indefinite number of retries?***From:*A. Jesse Jiryu Davis

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

**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?***From:*A. Jesse Jiryu Davis

- Prev by Date:
**[tlaplus] Re: Procedure in PlusCal** - Next by Date:
**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Previous by thread:
**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Next by thread:
**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Index(es):