Science of Concurrent Programs: 3.4.1.4 Error in Composition?

[Dave Hughes]

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

[Andrew Helwer]

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

--
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...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/c36ba172-2f6e-40e8-9ec3-5f47db63ddd9n%40googlegroups.com.

[Stephan Merz]

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

[Dave Hughes]

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 3^rd conjunct is easier (for me) - but that is not what he is trying to show - I think.  

Dave 

---

From: tla...@googlegroups.com <tla...@googlegroups.com> on behalf of Stephan Merz <stepha...@gmail.com>
Sent: Monday, November 24, 2025 20:22
To: tla...@googlegroups.com <tla...@googlegroups.com>
Subject: Re: [tlaplus] Science of Concurrent Programs: 3.4.1.4 Error in Composition?

 

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/3F39D6C4-274D-4369-A0EB-7B78A4389C04%40gmail.com.

[Andrew Helwer]

Your programmer's intuition isn't wholly misplaced. If you were to write an interpreter for this action, you would have to identify that the value of x' relies on the value of t' and thus you have to evaluate t' before x', even though your interpreter encounters x' in the conjunction list first. Of course this is getting away from Lamport's intended perspective that you view actions as predicates on pairs of states pulled out of the mathematical ether, but when we want to check this on actually existing physical computers we have some practical constraints. I've found that a lot of TLA+ familiarity requires smoothly shifting between these different perspectives depending on the context.

Andrew 

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/MN2PR12MB318446FF96AE120E1B960D72F2D0A%40MN2PR12MB3184.namprd12.prod.outlook.com.

[Dave Hughes]

If someone is updating this work then two other lesser things might want to be fixed:

1.   on page 50  the reference to the definition of except is incorrectly cited as 2.8.2 - it is actually introduced at he top of page 47 in 3.3 introduction.
2. The abstract program in fig. 3.5 on page 54 is missing the definition of TypeOk and NumberDone, which may be cut and pasted from page 51.

Dave

---

From: tla...@googlegroups.com <tla...@googlegroups.com> on behalf of Andrew Helwer <andrew...@gmail.com>
Sent: Monday, November 24, 2025 20:49

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUUCbzt-ffxoYGfeu%3DTiQdDLQ0D9Wt5114LTaMy0Lj5vxA%40mail.gmail.com.

[Chris Ortiz]

Hi,

On another side project we are working on, we are experimenting with Java option: -Dtlc2.tool.impl.Tool.cdot=true for action composition. Moving from the science to the usage on the tool, have anyone tried this on TLC? I got some errors which I am trying to get sense of.

---- MODULE ActionComposition ----
EXTENDS Naturals
CONSTANTS Procs, NumberDone

VARIABLES x, t, pc
vars == << x, t, pc >>

Init ==
    /\ x = 0
    /\ t = [ p \in Procs |-> 0 ]
    /\ pc = [ p \in Procs |-> "a" ]

aStep(p) ==
    /\ pc[p] = "a"
    /\ x' = x
    /\ t' = [ t EXCEPT ![p] = x ]

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

bStep(p) ==
    /\ pc[p] = "b"
    /\ x' = t[p] + 1
    \*/\ x' = t'[p] + 1 \*Suggested errata is causing error
    /\ t' = t
    /\ pc' = [ pc EXCEPT ![p] = "done" ]

aStep_bStep(p) ==

    /\ pc[p] = "a"

    \*/\ x' = t[p] + 1
    \*/\ x' = t'[p] + 1 \*Causing error if before the next line

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

    /\ x' = t'[p] + 1 \*Passing if you put this here

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

PgmStep == \E p \in Procs:
                    \*\/ aStep(p)
                    \*\/ bStep(p)
                    \/ aStep_bStep(p) \*Alternative action composition

Stutter ==
    /\ \A p \in Procs: pc[p] = "done"
    \*/\ <<x',t',pc'>> = << x, t, pc >> \*does not work
    \*/\ vars' = vars                   \*does not work
    /\ UNCHANGED vars \*This works

Next == PgmStep \/ Stutter

TypeOK ==
    /\ x \in Nat
    /\ t \in [Procs -> Nat]
    /\ pc \in [Procs -> {"a", "b", "done"}]

Inv ==
    /\ TypeOK
    /\ \A p \in Procs: (pc[p] = "b" => (t[p] =< NumberDone))
    /\ x =< NumberDone


Composition ==
    /\ TRUE
    \*/\ [][\A p \in Procs: aStep(p) \cdot bStep(p) => pc[p] = "done"]_vars
    \*/\ [][\A p \in Procs: aStep_bStep(p) => pc[p] = "done"]_vars
    \*/\ [][\A p \in Procs: aStep(p) \cdot bStep(p) => aStep_bStep(p)]_vars
    \*/\ [][\A p \in Procs: aStep_bStep(p) => aStep(p) \cdot bStep(p)]_vars

Thanks and best regards,

Chris (Zitro)

[Andrew Helwer]

A lot of these are things which could be implemented in TLC but currently are not. With regard to the tuple priming one, Will Schultz opened an issue for it back in 2019. I thought TLC implemented conjunct reordering as I described above but I guess not.

Both of these would be easy to implement statically through pre-check AST rewrites but that functionality (and translation of error messages across AST rewrites) does not (yet?) exist in TLC.

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/b13d8fef-57cc-4aaf-970c-036e142f76acn%40googlegroups.com.

[Markus Kuppe]

The pull request https://github.com/tlaplus/tlaplus/pull/805 mentions the limitation of the current prototype and explains how this limitation can appear in practice. I estimate that it would take approximately one month to implement https://github.com/tlaplus/tlaplus/pull/805#issuecomment-1492385553.

M.