Hi Edgar,
>>Would it be possible to get the source code of TLA+ models you mentioned in the paper?
Two of the specs are available here:
The paper(s) also mention specs for systems at Amazon (e.g. parts of DynamoDB, S3, EC2). Those specs are not available outside of Amazon.
That sounds very interesting. Please could you send me a copy?
>>I would like to explore ways to prove your code correct using VCC (or other automated deductive techniques).
That would be great. I did not attempt a proof, because a formal proof of the most interesting of the two algorithms (serializable snapshot isolation) probably requires finding an inductive invariant that implies that the algorithm never creates a cycle in the multi-version conflict graph established by the read and write dependencies between transactions[1]. I suspect that finding the inductive invariant is very difficult (e.g. may involve an induction argument due to use of the transitive closure operator in the property), but I have not tried. I suspect that the easiest (well, least difficult) way to do the proof would be to use TLC or the ProB constraint checker (via the TLA+-to-B translator) to 'debug' the inductive invariant, and then use TLAPS for the proof, rather than proving the low-level code correct. (E.g. Even expressing the correctness property may be quite tricky in VCC.) However, I hope I'm wrong about that; it would be great to have a proof of an implementation.
FYI, at least three different C implementations of serializable snapshot algorithm are available. Recent versions of the PostgreSQL database use the algorithm for SERIALIZABLE isolation level [2], and research implementations are available as patches for older versions of Berkeley DB and MySQL (InnoDB) from the author of the algorithm, Michael Cahill. If you are interested in the latter, I can put you in touch with Michael.
regards,
Chris
[1] You'll see in the specs that I actually model-checked that the MVSG was cycle free, rather than directly checking the true desired safety property. The true desired safety property is one-copy serializability; roughly, the global execution history of events over all transactions can always be permuted to a history in which the same results are observed and all transactions execute consecutively, with no interleaving of events from different transactions. There's a well known theorem that proves that absence of cycles in the MVSG implies one-copy serializability. I didn't bother to state the theorem in the specs, but the comments point to a standard reference (Phil Bernstein's book on concurrency control and recovery in transaction systems) which states the theorem and gives an informal proof.
[2] http://drkp.net/papers/ssi-vldb12.pdf
On Wednesday, October 1, 2014 3:47:32 PM UTC-7, Edgar Pek wrote:
Hello Chris,
Would it be possible to get the source code of TLA+ models you mentioned in the paper?
I am a PhD candidate from University of Illinois. I have worked with VCC in various contexts. (E.g, http://dx.doi.org/10.1145/2666356.2594325)
I would like to explore ways to prove your code correct using VCC (or other automated deductive techniques).
Thank you,
Edgar
pe...@xxxxxxxxxxxx
On Thursday, June 12, 2014 2:50:21 PM UTC-5, Chris Newcombe wrote:
> The following paper was presented at ABZ'2014 last week, and is now available in the conference proceedings:
>
>
> Newcombe,
> C., Why Amazon Chose TLA+, in
> Abstract State Machines, Alloy, B, TLA, VDM, and Z Lecture Notes in
> Computer Science Volume 8477, 2014, pp 25-39;
> http://link.springer.com/chapter/10.1007%2F978-3-662-43652-3_3
>
> I'm happy to provide copies privately on request.
>
>
>
>
> The above is a partner to our other paper, "Use of Formal Methods at Amazon Web Services", which is currently available via the TLA+ home page. See earlier post: https://groups.google.com/d/msg/tlaplus/bPlvP1V5hyk/0xPGIrpb7wUJ
>
>
> regards,
>
> Chris