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

Re: [tlaplus] Science of Concurrent Programs: 3.4.1.4 Error in Composition?

Thanks for your comprehensive responses - they helped me understand better - i think Lamport's intended solution was the t'(p)+1 because that makes the footnote 5 make sense! Until I saw this i could not understand the point of the footnote. As a programmer it is uncomfortable - and just removing the 3rd conjunct is easier (for me) - but that is not what he is trying to show - I think.  

Dave 



From: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> on behalf of Stephan Merz <stephan.merz@xxxxxxxxx>
Sent: Monday, November 24, 2025 20:22
To: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx>
Subject: Re: [tlaplus] Science of Concurrent Programs: 3.4.1.4 Error in Composition?
 
You are correct to point out that this definition is wrong. Logically, action composition of two actions A(x, x’) and B(x,x’) where x denotes a tuple of all state variables corresponds to the conjunction \E x’’ : A(x, x’’) /\ B(x’’, x’) where x’’ is a fresh tuple of variables. In the example we get

aStep(p) . bStep(p) = \E x’’, t’’, pc’' :
  /\ pc(p) = a
  /\ x’’ = x
  /\ t’’ = (t EXCEPT p |-> x)
  /\ pc’’ = (pc EXCEPT p |-> b)
  /\ pc’’(p) = b
  /\ x’ = t’’(p) + 1
  /\ t’ = t’'
  /\ pc’ = (pc’’ EXCEPT p |-> done)

Some simplification, in particular using the "one-point rule" (\E y : y = t /\ A(y)) = A(t), yields

aStep(p) . bStep(p) =
  /\ pc(p) = a
  /\ x’ = x+1    \* alternatively: x’ = t’(p)+1
  /\ t’ = (t EXCEPT p |-> x)
  /\ pc’ = (pc EXCEPT p |-> done)

Stephan

On 24 Nov 2025, at 18:34, Dave Hughes <dbahughes@xxxxxxxxx> wrote:


The composition of steps a and b from figure 3.5 is listed in 3.4.1.4 on page 58 as:

aStep(p). bStep(p) =  

/\ pc(p) = a

/\  x’  = t(p) + 1

                /\ t’  =  (t EXCEPT p |->  x )

                /\ pc’ = (pc EXCEPT p |-> done)

This to me seems wrong since t is only changed when that process is about to be set to done and hence is never accessed. So as far as i can see this will only ever set x' to one of the initial values of t (+1) - so will always end at one since t is initialized to zero for all processes.

I am fairly new to TLA and a little terrified to question this so i apologize in advance if i am wasting peoples time - but all my efforts to make sense of this have failed.

In some ways this is a bit of a weird example since the temporary variable was introduced to illustrate issues of concurrency - and when you compose the steps it becomes irrelevant- naturally.

Thanks for any help!

Dave Hughes




--
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 visit https://groups.google.com/d/msgid/tlaplus/c36ba172-2f6e-40e8-9ec3-5f47db63ddd9n%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 visit https://groups.google.com/d/msgid/tlaplus/3F39D6C4-274D-4369-A0EB-7B78A4389C04%40gmail.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 visit https://groups.google.com/d/msgid/tlaplus/MN2PR12MB318446FF96AE120E1B960D72F2D0A%40MN2PR12MB3184.namprd12.prod.outlook.com.