Re: Why Amazon Chose TLA+

[ernie...@xxxxxxxxx]

>(E.g. Even expressing the correctness property may be quite tricky in VCC.) 

Roughly speaking, the normal way to specify and verify transaction processing in VCC is to 
1) specify the semantics of transactions (easy)
2) introduce a ghost copy of the state, in which transactions execute atomically
3) prove a coupling invariant between the abstract state and the concrete state, which at least behaves as expected wrt I/O and when transactions quiesce.

For a system like Hekaton, which is essentially strictly serializable (or whatever strict serializability is called in the context of snapshot isolation), this is relatively easy (except that you have to hack around VCC's lack of prophecy variables, which you need to to guess whether a transaction will end up aborting for some unforseeable reason). However, for techniques that are based on just looking for cycles in dependency graphs, the coupling invariant can indeed be  quite painful (though the use of transitive closure is not itself necessarily problematic). 

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.

ernie