Re: Why Amazon Chose TLA+

[ernie...@xxxxxxxxx]

Hi Leslie,

I absolutely agree that a refinement map provides a lovely way to explain why a protocol implements a specification. I also agree that someone who cannot write a refinement map for their TP protocol won't be able to verify serializability using TLC (which was really all I was trying to say about TLA in the original post). I've generally failed in my efforts to get engineers to write down refinement maps (or even document serialization points in their code), but armed with the TLC carrot, you have perhaps had better success.

    Putting a monkey at a keyboard who has no idea why the program he's 
    writing might work may be common practice, and it might be satisfactory for
    programs that compute an answer and are easy to test, but it doesn't work 
    too well for protocols. 

Many interesting protocol specifications don't require existential quantifiers (and hence don't require abstaction maps), or can be verified with the trivial abstraction map (obtained by simply deleting the existential quantifier). This enables monkeys to verify consensus protocols, philosopher protocols, durable queues, caching for single-threaded clients, various kinds of recovery, etc. This is the sense in which I was saying that TP really is a step up from what many (most?) engineers do with TLC.