RE: [tlaplus] Re: Draft of New TLA Book

Hi Lorin,

Thanks for finding all these errors. One thing you reported is not an error:

p297 A subset S of a metric space M is said to be dense iff C(S) = [M].

-> should be [S]?

This is the correct definition of a dense set. C(S) = S is the definition

of a closed set.

Cheers,

Leslie

From: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> On Behalf Of Lorin Hochstein
Sent: Sunday, January 28, 2024 21:51
To: tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Subject: Re: [tlaplus] Re: Draft of New TLA Book

You don't often get email from lorinh@xxxxxxxxx. Learn why this is important

Hi Leslie:

Thanks for the response. I also found what appear to be a few minor errors/typos. These are from version of 2 January 2024. Errors are indicated by [square brackets]:

p158, 5.1.2. Let an S-State be a state of AddS, which is an assignment of values to the variables u,v, w and [end] of AddS;

-> should be [fin]?

p162 all other steps must refine stuttering steps of [AddSeq]

-> should be [Add]?

p175 In particular, sem_LM equals 0 iff pc_LM(p) equals [pc] or exit for ...

-> should be [cs]?

p179 Figure 5.3, last row, last column: pc_OB(p) = [cs]

-> should be [exit]?

p179 By [(4.15)], we can do this by proving:

-> should be [(4.12)]?

p212 We then replace DispOrNot in [ICen2] by ...

-> should be ICen1?

p237 If our strategy has been successful thus far and qBar = [pq] at the beginning of the step, then a BeginPOEnqpq step implies qBar′ = [pq]′.

-> should be [pg]?

p237 Let's call a state in which there is a datum in elts that is not in beingAdded [] a blocked state.

-> missing [or in pg]?

p239 3. Following each BeginPOEnq pq step such that Len (pg ′ ) > Len (pg ) (which implies [eq] = ⟨⟩), s adds Len(pg′) − Len(pg) stuttering steps.

-> should be [eb]?

p296 For a metric space M , the distance \^{δ}(p, [M]) from p ∈ M ...

-> should be [S]?

p297 For any metric space M and S ⊆ M , any element p of M with [d](p,S) = 0 ...

-> should be [\^{δ}]?

p297 A subset S of a metric space M is said to be dense iff C(S) = [M].

-> should be [S]?

Take care,

Lorin

On Wednesday, January 17, 2024 at 4:33:25 PM UTC-8 Leslie Lamport wrote:

Hi Lorin,

Thank you for finding a serious error in the book. The inductive invariant Inv in the book is strong enough to prove mutual exclusion, but not deadlock freedom. That invariant allows process 1 to halt in its noncritical section with x[1] = TRUE, which will not allow process 0 to enter its critical section. A stronger inductive invariant is needed to prove liveness. This will be corrected in the next released version. Meanwhile, I suggest that you find the necessary inductive invariant yourself.

I’m embarrassed that I didn’t notice such an error. I think it happened because the TLA+ version that I model checked had the correct invariant. When I checked my proof, I must have been thinking Inv was the invariant in the TLA+ version. I believe a significant amount of time passed between when I wrote Section 4.2.5.2 that contains the invariant and the current version of Section 4.2.5.3 containing the liveness proof. That’s probably why I didn’t notice that the TLA+ version of the invariant was not the one in the book.

Cheers,

Leslie

From: tla...@xxxxxxxxxxxxxxxx <tla...@xxxxxxxxxxxxxxxx> On Behalf Of Lorin Hochstein
Sent: Sunday, January 14, 2024 21:03
To: tlaplus <tla...@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Re: Draft of New TLA Book

You don't often get email from lor...@xxxxxxxxx. Learn why this is important

Hi Leslie:

I have a question about section 4.2.5.3: Proving Liveness

On page 134, the proof sketches for edge 5 and edge 7 read:

> edge 5 This is an implication since ☐Inv implies that if process 1 is forever at ncs, then x (1) is forever false.

> edge 7 This is an implication, because Inv and pc(1) = w4 imply ¬x (1).

p130 reads:

> We define Inv to equal (4.6), with TypeOK defined by (4.17).

According to (4.6) on p122, this would mean:

Inv == /\ TypeOK

/\ \A p \in {0,1): /\ (pc(p) \in {w2, cs}) => x(p))

/\ (pc(p) = cs) => (pc(1-p)\= cs)

Given the above definition for Inv, I can't see how ☐Inv could be used to imply ☐¬x(1), given that the only place that x(p) appears in Inv (other than TypeOK) is in the consequent of an implication. What am I missing here? (Am I using the wrong Inv?)

Take care,

Lorin

On Wednesday, January 3, 2024 at 11:14:24 AM UTC-8 Leslie Lamport wrote:

A draft of a new book I have tentatively titled A Science of Concurrent Programs is available here. The book explains the scientific principles underlying the TLA+ language. It contains a lot of math. All the math beyond high school algebra is explained, but it will be tough going for readers who haven't taken an introductory university math class for computer science students that covers things like sets and logic. The book contains little discussion of how TLA+ is used in practice, but it explains why TLA+ is what it is.

This is a preliminary version and I welcome comments, suggestions, and questions. Anyone who is the first to report any error will be thanked in the final version.

--

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/bef439e7-6a6c-4058-8366-a544088b5666n%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/4471dd6a-08d2-4aea-8f8f-140a81a401f4n%40googlegroups.com.