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

Working through this; here are the definition of aStep and bStep being composed (given with state numbers on page 49 and then with state numbers eliminated on page 54), translated into standard TLA+; the A-step reads the value to be incremented, and the B-step actually increments it (p is a process variable, so we see a clear opportunity for multiple processes to trample on each other as they update the increment variable x with stale reads stored in their process-local memory t):

aStep(p) ==

/\ pc[p] = "a" \* Precondition: program counter indicates A-step

/\ UNCHANGED x \* Value of x is unchanged, it is only read in this step

/\ t' = [t EXCEPT ![p] = x] \* Read the value of x into process-local memory

/\ pc' = [pc EXCEPT ![p] = "b"] \* Next step for this process will be a B-step

bStep(p) ==

/\ pc[p] = "b" \* Precondition: program counter indicates B-step

/\ x' = t[p] + 1 \* Value of x is updated from value stored in process-local memory (could be stale!)

/\ UNCHANGED t \* Process-local memory is unchanged

/\ pc' = [pc EXCEPT ![p] = "done"] \* Process goes to termination state

So if we compose these two steps, by my reckoning we should get:

aStep(p) \cdot bStep(p) =

/\ pc[p] = "a"

/\ x' = t'[p] + 1

/\ t' = [t EXCEPT ![t] = x]

/\ pc' = [pc EXCEPT ![p] = "done"]

Thus I think you're right, Lamport missed a prime on the t variable in this action composition; t is initialized with all elements set to 0. Good catch!

No reason to be terrified of asking questions like this, I post braindead questions all the time (lol). What matters is we (or most likely Stephan) check each other's work and arrive somewhere near the correct conclusion.

Andrew Helwer

On Mon, Nov 24, 2025 at 9:34 AM 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.