Re: [tlaplus] Artificial coupling of variables

On 6 Sep 2020, at 11:11, Jedd Haberstro <jhaberstro@xxxxxxxxx> wrote:

Hi Stephan,

Thanks for the guidance.

I do believe a refinement is possible. Wherever the implementation takes an atomic step that is not mandated by the API (i.e. allowed by the API's TLA+ spec), the implementation's spec could be written such that artificial steps are inserted that behave like stuttering steps for all variables except those used in the refinement mapping. There would be as many of these steps inserted into the implementation's behaviour as is necessary for the refinement mapping variables to eventually equal the implementation's actual state while still representing valid state transitions in the the API spec. Do you disagree?

Multiple steps A1, A2, ..., An can refine a single step as long as every Ai (except perhaps the last one) only changes low-level variables that do not occur in the high-level specification. (And conversely, a single step can then also refine multiple steps, see "stuttering variables" in [1].) Your toy example had only a single variable that you would naturally consider to be visible, otherwise the spec doesn't really have much meaning.

Admittedly, this feels like it would be quite the tedious machinery to tack onto, what I anticipate to be, a non-trivial spec, so I am not keen to go down this path..

I think I agree that embracing the fact that several transitions may occur is the correct path forward. As for you specific suggestion, I suppose this would have several implications on how to write the operators that compute the result of the operation:
No use of prime variables.

Yes, I was thinking of a "functional programming" style: the operators would not be TLA+ actions but would compute the result of the operation.

Enabling predicates must be rewritten as IF or CASE expressions.

Again, these wouldn't be part of the operators but of the surrounding spec. The operators would be applied only when the enabling condition is satisfied.

More importantly, I'm failing to see how to handle multiple primed variables.

Your operator could return a tuple or a record (in principle, you can rewrite any spec into one that has a single record-valued variable whose fields correspond to the variables of the original spec).

How practical and readable all this will be is a different story. Fundamentally, you are trying to write a "non-interleaving" specification that allows several actions to occur simultaneously. These are harder to write than the standard interleaving specs, and depending on what you are trying to model it may not be worth the effort. For example, whether two transitions of different nodes in a distributed system happen at the same time or in an arbitrary order doesn't matter because no other system component can observe the difference.

Best,

Stephan

Thanks,
Jedd

[1] https://arxiv.org/abs/1703.05121

On Sunday, September 6, 2020 at 12:14:14 AM UTC-7 Stephan Merz wrote:
Hello,

TLA+ actions describe atomic transitions, and this excludes the first option that you mention:

1. Define a refinement mapping that somehow shows that, e.g., 1 state transition of the implementation that unblocks N processes, is equivalent to N state transitions in the API spec where the transitions unblock processes one by one.

The sequence of N transitions contains (visible) states that do not exist in the execution having a single transition. Therefore refinement simply does not hold.

I'd recommend that your specification fully embrace the fact that several transitions may occur. In your toy example, you could do so by writing

EXTENDS Integers
VARIABLES s

Init ==
  s = [i \in 1..2 |-> 0]

Inc(S) ==
  s' = [i \in 1..2 |-> IF i \in S THEN s[i]+1 ELSE s[i]]

Next == \E S \in SUBSET (1..2) : Inc(S)

In a more realistic example, you'd replace s[i]+1 by an operator that computes the result of the operation that the action represents, based on the current state.

Regards,
Stephan

On 6 Sep 2020, at 05:32, Jedd Haberstro <jhabe...@xxxxxxxxx> wrote:

Hello,

Consider this simple module

EXTENDS Integers
VARIABLES s

Init ==
s = [i \in 1..2 |-> 0]

Inc(i) ==
s' = [s EXCEPT ![i] = s[i] + 1]

Next == Inc(1) /\ Inc(2)

Next can never be enabled because Inc(i) is enabled when just 1 element of the array increments. This artificial coupling is a byproduct of my choice to represent logically independent variables with a function(/array).

In this particular module the coupling could be removed by replacing s with variables s1 and s2 and using an IF or CASE conditioned on i to select which variable to increment. In the general case, however, this is not a practical solution as the number of variables may be parameterized by a CONSTANT.

To contextualize the issue, I am writing a specification for an API and trying to show that a particular system implements this API. The implementation allows for multiple processes to take "steps of execution" in parallel (e.g. two processes blocked on the same condition may unblock in one state transition), whereas the API is defined only in terms of local steps of execution each process may take; the potential for parallelism of the system has no impact on semantics of the API.

The way I see it, I have two options:

1. Define a refinement mapping that somehow shows that, e.g., 1 state transition of the implementation that unblocks N processes, is equivalent to N state transitions in the API spec where the transitions unblock processes one by one. Being new to TLA+, I'm not confident in my ability to figure out how to actually express this.. :D

2. At the cost of clarity, model the potential for parallelism explicitly in the API spec, which will mean changing the definition of every sub-action.

What I wish I could do is change my API spec without having to change its sub-actions by formulating the top-level Next state action like this:

\E stepping \in SUBSET Threads :
/\ stepping # {}
/\ \A t \in stepping :
\/ MethodA(t)
\/ MethodB(t)
\/ .... etc ...

but, of course, this does not work because each Method sub-action contains a predicate of the form

controlState' = [controlState EXCEPT ![t] = .... ]

So, to recap, unless there is some other option I haven't thought of, I am forced to introduce complexity into my spec to workaround syntactic deficits of the TLA+ language. It seems that if there were a macro system built into the language, it would be possible to express what I wish without the additional complexity.

Have I correctly understood the situation or is there an idiom or feature of the TLA+ language that will help my situation?

Thank you,
Jedd

--
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/734edefa-87e0-4f29-8cb4-f3d0e71c5672n%40googlegroups.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/26e4fbb6-100d-4d5c-8e23-da31d6d4bbf3n%40googlegroups.com.