Draft of New TLA Book

[Leslie Lamport]

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. 

[Peter Sovietov]

Hi Leslie!

In the middle of the book (p. 146) you wrote:

"In the past 40 years, I have had essentially no contact with engineers who build real-time systems. I know of *only one case* in which TLA was used to check correctness of the design of a commercial real-time system [5]. From the point of view of our science, there is nothing special about real-time programs. However, how well tools work can depend on the application domain. The TLA+ tools were not developed with real-time programs in mind, and it’s unclear how useful they are in that domain."

But at the begining (p. 10) the reader can find the following text:

"Virtuoso was a real-time operating system. It controlled some instruments on the European Space Agency’s Rosetta spacecraft that explored a comet. Its creators decided to build the next version from scratch, starting with a high-level design written in TLA+. They described their experience in a book [47]."

As far as I understand, [5] and [47] are completely different works. Thus, in reality there are at least two known real-time projects related to TLA+,  or am I missing something?

среда, 3 января 2024 г. в 22:14:24 UTC+3, Leslie Lamport:

[Sergey Bronnikov]

Hi, Leslie!

Thanks for the book!

There is a typo in "4.2.5.3 Proving Liveness" (p. 132):

> Since Λ equals 2Λ, and once 2Λ is true it is true forever, this formula is equivalent to Λ ∧ G ; H 1 ∨ . . . ∨ H j.

> (This follows from (3.32c).and propositional logic.)

seem there is an extra dot before "and"

Sergey

среда, 3 января 2024 г. в 22:14:24 UTC+3, Leslie Lamport:

[Lorin Hochstein]

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

[Leslie Lamport]

Hi Lorin,

 

Thanks for reporting this.  I don’t have time to deal with it now, but I will in a few days.

 

Cheers,

 

Leslie Lamport

 

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

 

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

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/bef439e7-6a6c-4058-8366-a544088b5666n%40googlegroups.com.

[Leslie Lamport]

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

 

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

Hi Leslie:

--

[Lorin Hochstein]

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

[Leslie Lamport]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4471dd6a-08d2-4aea-8f8f-140a81a401f4n%40googlegroups.com.

[Akash]

Hi Leslie,

I'm super interested in understanding TLA, but I don't understand the terms you use, like dense set, for example.

Which branches of math knowledge are you referring to? And prerequisite for knowing these terms.  As a CS student, I've only studied Discrete Mathematics and Calculus.

Kind regards,

Akash

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/LV2PR21MB322921E13D5EAF3419284511B87E2%40LV2PR21MB3229.namprd21.prod.outlook.com.

[Leslie Lamport]

Hi Akash,

 

The term “dense set” should appear only in the appendix, and its definition is given there.  If the definition does not give you an intuitive idea of what it means, thinking about the example of the set of ordered pairs of finite-digit numbers should help.

 

If there any things in the book that you did not learn in your classes and are not defined in the book, please let me know.

 

Cheers,

 

Lelie Lamport

 

From: tla...@googlegroups.com <tla...@googlegroups.com> On Behalf Of Akash
Sent: Tuesday, January 30, 2024 11:11
To: tla...@googlegroups.com
Subject: Re: [tlaplus] Re: Draft of New TLA Book

 

You don't often get email from akash.g...@gmail.com. Learn why this is important

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFZmCwCWFUFQW10xb%2B9HmWvqmmfSNFtrVbmP2oT_EnENPPUH%3DQ%40mail.gmail.com.

[Leslie Lamport]

An extensively revised draft of A Science of Concurrent Programs is available at the same place.  Chapter 2, which describes ordinary math, has been simplified and made much shorter.  Much of the material that used to be there has been moved later in the book to where it is first needed.  Comments and error reports are still welcome.

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

[Nine Fingers]

Hi Leslie, 

I'd like to provide a suggestion of including some of the concepts of your "Computation and State Machines" paper in the book, especially the first parts regarding state machines, they were particularly illuminating for me and they provide a nice mental model for TLA+ and a rationale for why it works the way it does.