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

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: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> On Behalf Of Lorin Hochstein
Sent: Sunday, January 14, 2024 21:03
To: tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Re: Draft of New TLA Book

You don't often get email from lorinh@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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bef439e7-6a6c-4058-8366-a544088b5666n%40googlegroups.com.