[tlaplus] Re: A Science of Concurrent Programs is now published!

[Lorin Hochstein <lorinh@xxxxxxxxx>]

It was a while ago, but I did read through it, and I thought it was worth it. One thing I took away from it: it explains how to use prophecy variables to do the refinement mapping of the linearizable queue in the Herlihy and Wing paper on Linearizability. Before reading this, I was aware of prophecy variables, but I couldn't figure out the right way to apply them in this case.

I ended up writing a blog post at the time:  https://surfingcomplexity.blog/2024/09/22/linearizability-refinement-prophecy/

Lorin

On Sunday, May 3, 2026 at 8:35:53 PM UTC-7 Andrew Helwer wrote:

Just noticed this - although A Science of Concurrent Programs has long been available for free on Lamport's website, it is now officially published by Cambridge in hardcover & ebook form!

https://www.cambridge.org/us/universitypress/subjects/computer-science/distributed-networked-and-mobile-computing/science-concurrent-programs?format=HB

Have people been reading it? Personally I have read up to section 6.3, the presentation of the Paxos algorithm as a hierarchical refinement of TLA+ specs (basically another presentation of Lamport's Turing Award lecture). I have stalled out there but recently Alex Kladov has been posting comments about Paxos on lobste.rs, specifically about how going through this presentation really solidified his knowledge about why Paxos works instead of it just being an elegant method of dodging all the stuff that can go wrong, which is how I usually think of it. So I think I will try to read through it in the near future.

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/91e77798-3fbd-408c-8af2-72a372bc7dd7n%40googlegroups.com.