[TechTalkFollowup] UML vs. TLA+

Philip Durbin philip_durbin at harvard.edu
Tue May 20 08:27:35 EDT 2014

I just listened to
and Leslie Lamport 's comparison of UML vs. his TLA+ system reminded
me of Michael's talk about PlantUML.

I don't think I can do TLA+ justice so it would be best to listen to
the podcast above but I'd like to point to a practical use of TLA+ he
mentioned at Amazon.

According to https://groups.google.com/d/msg/tlaplus/C7Rmka3iSGE/zLQjQh0NeSEJ
Chris Newcombe will soon be publishing a paper called "Why Amazon
Chose TLA+".

He goes on to say:

"Part of my evaluation is already available, in a talk that I gave at
HPTS (bi-annual workshop on High Performance Transaction Systems) in

         Slides including notes :

         Specifications for 2 'real world' algorithms for transaction
isolation, in both Alloy and TLA+ :
http://hpts.ws/papers/2011/sessions_2011/amazonbundle.tar.gz "

His LinkedIn profile at
http://www.linkedin.com/pub/chris-newcombe/1/a08/b33 says
"Successfully introduced formal methods to Amazon, using Leslie
Lamport's method (TLA+ and PlusCal)"

That tarball has some interesting TLA+ examples
(textbookSnapshotIsolation.tla and serializableSnapshotIsolation.tla,
attached.) They're reminiscent of Michael's PlantUML examples but more
rigorous and mathematical, I'd say...

For more on TLA+ see


On Sun, Jan 12, 2014 at 12:13 PM, Bar-sinai, Michael
<mbarsinai at iq.harvard.edu> wrote:
> Hello everyone,
> The slides and code for Thursday talk (diagrams etc.), with some internal projects mentions removed, are available here:
> http://www.mbarsinai.com/blog/2014/01/12/draw-more-work-less/
> -- Michael
> (Thanks @philip_durbin for suggesting to post it)
> _______________________________________________
> TechTalkFollowup mailing list
> TechTalkFollowup at lists.iq.harvard.edu
> This list is shared with the public. Please do not discuss Harvard Confidential business on this list.
> To unsubscribe from this list or get other information:
> https://lists.iq.harvard.edu/mailman/listinfo/techtalkfollowup

Philip Durbin
Software Developer for http://thedata.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: textbookSnapshotIsolation.tla
Type: application/octet-stream
Size: 69101 bytes
Desc: not available
URL: <http://lists.iq.harvard.edu/pipermail/techtalkfollowup/attachments/20140520/edcd276e/attachment-0002.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: serializableSnapshotIsolation.tla
Type: application/octet-stream
Size: 86129 bytes
Desc: not available
URL: <http://lists.iq.harvard.edu/pipermail/techtalkfollowup/attachments/20140520/edcd276e/attachment-0003.obj>

More information about the TechTalkFollowup mailing list