Re: Why Amazon Chose TLA+

[ernie...@xxxxxxxxx]

On Monday, March 30, 2015 at 2:03:27 PM UTC-4, Leslie Lamport wrote:
> Ernie writes,
>    Note that while you can specify strict serializability in TLA, it
>    requires use of temporal existential quantification, which you won't
>    be able to check with TLC unless you can provide a suitable witness.
> I'm puzzled by this.  If you don't want to limit what you can express
> to simple properties, you have to be able to specify one system by a
> more abstract system.  And writing a philosophically correct spec of
> that form requires variable hiding, which is represented in TLA by
> temporal existential quantification.  So it's not just
> serializability; you can't even specify a FIFO queue in TLA without
> temporal quantification.  Clearly this isn't a practical issue, and
> surely Ernie realizes this.

My point wasn't about writing the specification (you're right that this philosophically requires temporal existential quantification), it had to do with the practical issue of checking with TLC that a model satisfies the specification, which requires eliminating the temporal existential quantifier. For this, a FIFO queue and strict serializability seem to be rather different. For the FIFO queue implementation, you can obtain a witness by simply removing the temporal existential quantifier from the FIFO queue specification. (This is because, for any interface action of a FIFO queue, there is only one way to update the abstract queue state.) So checking a FIFO queue with TLC presents no problem.

But for a transaction processor providing strict serializability, the hidden state can change in many different ways (any pending transaction might execute atomically in any step), so you can't just delete the temporal existential quantifier and get a witnessed model to check; you have to write a witnessing formula, which requires understanding why the protocol works (or at least where the serialization points are). Moreover, even for strict serializability, this instantiation might require prophecy, which you can't put directly into a TLC model (though I assume you can code it up by choosing the right property to check).