Why Amazon Chose TLA+

[Chris Newcombe]

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

[Steve Glaser]

I’d love a copy….

Thanks

Steve Glaser

sgl...@sglaser.com

sgl...@nvidia.com

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Friedrich Vogt]

I’d love a copy too!

 

Thanks

 

Fritz

 

--

[lkra...@gmail.com]

Hello,

I would appreciate a copy as well!

att,
--
Paul Eipper

[who...@gmail.com]

I would love a copy as well if possible!

[wewe...@gmail.com]

I would like a copy too. Thanks!

[awaw...@gmail.com]

I would like to have copy of the paper, too. Thanks!

[myno...@gmail.com]

Hi Chris,

I also would like to receive a copy.

Thanks,

Marcelo

[Tim Chen]

I'd also like a copy.

Thanks!

Tim

[edga...@gmail.com]

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...@illinois.edu

[Chris Newcombe]

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: 

        Specs for two algorithms for transaction isolation, in both TLA+ and Alloy : http://hpts.ws/papers/2011/sessions_2011/amazonbundle.tar.gz 

        Slides including notes : http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf

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. 

     >>I have worked with VCC in various contexts. (E.g, http://dx.doi.org/10.1145/2666356.2594325) 

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

[cit]

Hello, 

I would appreciate a copy!

Thank you

Dmitry

[Frank Hsueh]

mee too !!!

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--
Frank Hsueh | frank...@gmail.com

[assadebr...@gmail.com]

On Thursday, June 12, 2014 8:50:21 PM UTC+1, 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 
>

> I'm happy to provide copies privately on request.
>

A bit late to the party - yes please :)

Thanks,
Assad

(AssadEbrahim@gm....com)

[angeorg]

Hello,

I would really appreciate a copy.

Thank you in advance.

[sol...@gmail.com]

On Thursday, June 12, 2014 12:50:21 PM UTC-7, Chris Newcombe wrote:

I'd very much like a copy of this paper.

If you need it, I can supply a snailmail address. (I'm a retired math professor.)

Thanks,

Bob Solovay
solovay at gmail dot com

[exps...@gmail.com]

Could you please send me a copy? I would appreciate if you could.


2014년 6월 12일 목요일 오후 12시 50분 21초 UTC-7, Chris Newcombe 님의 말:

[camilo....@gmail.com]

I would love a copy of this paper. Thank you!

[marc magrans de abril]

I'd love to have a copy, too.

Thanks,
ma...@cern.ch

[eric...@gmail.com]

On Thursday, June 12, 2014 3:50:21 PM UTC-4, Chris Newcombe wrote:

I'd appreciate a copy, thanks!
Eric

[Carla Ferreira]

Can you send me a copy of your paper?

Thanks,

Carla

[ryan....@gmail.com]

Hi Chris,

I would like a copy of the paper please.

Thanks,
Ryan

[drrtal...@gmail.com]

On Thursday, June 12, 2014 at 12:50:21 PM UTC-7, 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    

Hi,

Could I please get a copy of your paper?

Thanks!

Roger Alexander

[ernie...@gmail.com]

>(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

[Leslie Lamport]

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 guess is that Ernie thinks serializability is a special case, and
it requires a spec that's quite unlike a FIFO queue spec.  He is both
wrong and right about this.  There is a simple way to specify
serializability in TLA+ whose state involves only a collection of FIFO
queues (one for each process) and a central memory.  And it has simple
fairness conditions on its action.  But he's right that although in
practice it's not fundamentally different from a FIFO queue spec, it's
fundamentally different from the FIFO queue spec because it's not
machine closed.  That difference arises because serializability is an
inherently weird spec--as evidenced by the fact that an implementation
that can predict the future can return a value for a read that hasn't
yet been written.  It could allow weird behaviors in circumstances in
which it would be possible to infer some future behavior by a process.
Anyway, the spec is in the Lazy Caching paper:

   http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#ladkin-gerth

Leslie

[Chris Newcombe]

Hi Leslie,

On this:

>>... serializability is an inherently weird spec--as evidenced by the fact 

>>that an implementation that can predict the future can return a value for 

>>a read that hasn't yet been written. 

I'm reminded of your comments in your paper, "Critique of the “Lake Arrowhead Three”" [1]

"I now regard [specifying database serializability] as a bad problem. The usual notion of serializability, which requires only that the values returned by a transaction be consistent with some serial execution of the transactions, is too weak. For example, it permits an implementation to throw away all values written by any completed transaction that only writes and does not read. The resulting execution is serializable, producing the same results as one in which all such write-only transactions are done last. A more realistic notion of serializability requires that if one transaction commits before another begins, then the first transaction appears before the second in the serialization order. ... 

"The more realistic form of serializability can be specified assertionally without using a variable to record the entire execution history. "

For the specification of database serializability that I wrote [2] (and to which Ernie is referring in his comments on my paper "Why Amazon Chose TLA+"), I did define serializability as a property of a history variable that recorded the entire execution history.  I don't know how I'd have done it without the history variable, as:

   1. The specification was actually for serializability of transactions over multi-version objects. (Multi-version concurrency control is now very common in transaction systems.) Serializability of multi-version objects is more complicated than serializability of non-versioned objects. 

   2. The property is fairly subtle to express. To get it right, I took the formulation from a textbook (actually 2 different sources; I verified their equivalence). The formulations in the textbooks are stated in terms of the execution history.

      >>you have to be able to specify one system by a more abstract system

I would very much like to be able to do this.  However, no industry spec that I'm aware of has been written as an abstraction/refinement. In all the industry specs that I know, correctness has been expressed as a bunch of properties.  Even Pamela Zave's work on finding flaws in Chord [3] follows the same pattern.  I'd like to do better, but I think much more education is needed in this area.

I did once try a small experiment with abstraction/refinement of an industry spec, just to try out the basic mechanics of expressing the relationship in TLA+ (module instantiation with substitution) and using TLC to check refinement.  I found the approach to be elegant and enticing, but my attempt was (knowingly) a worthless cheat, as my refinement mapping used an auxiliary variable.  I couldn't find the real refinement mapping in the short amount of time I tried, because I didn't understand the algorithm well enough. The algorithm was a rather subtle distributed algorithm.  It was also designed by another engineer, not me.  However, even for the algorithms that I've designed, I'm not sure that I'd be able to find refinement mappings in a reasonable amount of work.  (I can't find inductive invariants for my algorithms in a reasonable amount of work, and the two seem to be related.) Also, from my current position of ignorance it seems like like some creativity may be required in designing the 'right' abstract system, in order to make it easier to show refinement.

If you plan to write more instruction in this area, it would be very welcome.

regards,

Chris

[1] http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-critique.pdf

[2] http://hpts.ws/papers/2011/sessions_2011/amazonbundle.tar.gz

[3] http://www2.research.att.com/~pamela/chord.html

 

--

[Leslie Lamport]

Hi Chris,

I had forgotten that I had written a spec of serializability in that
paper.  The other one I mentioned is better because (a) it uses a
separate queue for each process, which seems to correspond more
closely to an implementation, and (b) it's in TLA+.  But it's the same
idea.  I don't know what transactions over multi-version objects are,
so I don't know if the same approach will work.

Using an auxiliary variable when showing that one spec refines another
need not be a cheat.  It is sometimes necessary.  (See the paper "The
Existence of Refinement Mappings" by Martin Abadi and me.

Abstraction always requires creativity.  In general, it's best to
write the simplest, clearest spec you can.  It's certainly better to
add history variables to the implementation rather than modifying the
spec to avoid them.  Prophecy variable are mindboggling enough that
I'd recommend trying to modify the spec to avoid them if you can.

Leslie

[ernie...@gmail.com]

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).

[Leslie Lamport]

Hi Ernie,

   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;

Any canonical TLA+ specification (initial predicate, next-state
relation, plus fairness) can, in principle, be model checked in
exactly this way.  Whether or not model checking is possible for a
large enough model to be useful depends on the nature of the spec.  I
don't think I've ever encountered a real TLA+ spec, written in
canonical form, that couldn't be at least simulated--checked on
randomly generated behaviors.  Of course, I'm talking here about
checking the spec, not checking that something implements the spec.
Even though a spec may allow too many behaviors for a model checker to
deal with, it is often possible for a model checker to do useful
checking that an implementation satisfies the spec.  That's because
only behaviors that satisfy the implementation have to be checked, not
all behaviors that satisfy the spec.

   you have to write a witnessing formula, which requires
   understanding why the protocol works

You have to do that for any method of verifying behavioral properties
specified with internal (hidden) variables.  And those are the only
general methods I know of that provide practical methods of verifying
arbitrary behavioral properties.  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.

   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).

This is unavoidable, unless you write the specification for the
explicit purpose of verifying your particular implementation.  With
the obvious specifications of serializability that require recording
the entire history, the use of auxiliary variables will almost always
be necessary.  With my spec of serializability, I used able to verify
safety of the lazy caching algorithm without a prophecy variable.  (I
needed a prophecy variable predicting whether or not something
eventually happened for proving liveness.)  In fact, the "witness
formula" (which in the TLA world and other places is called a
refinement mapping), provided a lovely, easy to understand explanation
of why the algorithm works.  I don't know if the same will be true for
other implementations of serializability, but I have a hunch that it
will.

Cheers,

Leslie

[ernie...@gmail.com]

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.

[Leslie Lamport]

Hi Ernie,

As expected, we are having an agreement.  Just a couple of remarks.

   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.

Engineers in industry have told me that they were interested in
checking implementation of a higher-level spec, but I don't know if
any of them have ever done it.  They generally check invariants and
perhaps simple liveness properties.

   Many interesting protocol specifications don't require existential

   quantifiers...  This is the sense in which I was saying that TP really

   is a step up from what many (most?)  engineers do with TLC.

I'd probably characterize those "interesting protocol specifications"
as high-level designs from which people code.  TP is a step up because
it's an abstract spec of what a system is supposed to do rather than a
design.  The only other industrial examples of abstract specs I know
about have been weak memory models.  They have been specified
axiomatically rather than with a real state machine as in a classic
TLA+ spec, so no one really understands them.  (Example: We once wrote
a TLA+ spec of the Itanium memory model that just added a variable to
capture the complete history and trivially built the axioms into the
state machine.  Using it, model checking discovered errors in some of the
examples in Intel's document describing the Itanium memory.)  I haven't heard
of anyone actually verifying that a chip design implements such a weak
memory model.  Engineers I knew just checked some consistency
requirements specified as invariants.

Leslie

[ernie...@gmail.com]

On Tuesday, March 31, 2015 at 8:27:02 PM UTC-4, Leslie Lamport wrote:
Hi Leslie,

> As expected, we are having an agreement. 

I agree.

>    Many interesting protocol specifications don't require existential
>    quantifiers...

> I'd probably characterize those "interesting protocol specifications"
> as high-level designs from which people code. 

Sorry for the ambiguity, I meant the parsing to be (interesting protocol) specifications, not interesting (protocol specifications). That is, there are interesting protocols (e.g. Paxos) whose specifications (at most one value chosen, and ... implies some value chosen) require at most trivial quantification. Someone who understands nothing about why Paxos works can therefore check Paxos (or any other protocol for consensus) with TLC.

[Leslie Lamport]

Hi Ernie,

   Sorry for the ambiguity, I meant the parsing to be (interesting
   protocol) specifications, not interesting (protocol specifications).
   That is, there are interesting protocols (e.g.  Paxos) whose
   specifications (at most one value chosen, and ...  implies some value
   chosen) require at most trivial quantification.  Someone who
   understands nothing about why Paxos works can therefore check Paxos
   (or any other protocol for consensus) with TLC.
  

There may be some confusion here.  One verifies a spec L by showing
that it refines some other (higher-level) spec H. Existential
quantification (variable hiding) in L is irrelevant.  It's the
existentially quantified variables in H that must be expressed in
terms of the variables (hidden or not) in L.  So quantification
is irrelevant for checking Paxos--that is, for showing that Paxos
satisfies some other property.

An implementation of Paxos that uses all the same variables as Paxos,
so the refinement mapping is trivial, is pretty uninteresting.  For
example, my specification of Paxos describes message passing in terms
of a single variable that is the set of all messages that have ever
been sent.  No one is going to implement Paxos using a set the
remembers all sent messages.  An actual implementation will describe
message passing in terms of various message queues, using
acknowledgements and retransmission to handle message loss, etc.
Since a real implementation won't remember all messages that have ever
been sent, it will need a history variable.  In simple Paxos
implementations, it's easy to add the set of all messages ever sent as
a history variable, so the part of the refinement mapping that
describes the Paxos spec's representation of the set of all previously
sent messages in terms of the implementation's variables becomes
trivial.  But that's not always the case.  For example, my proof of
correctness of the Liskov-Paxos Byzantine agreement protocol shows
that the algorithm implements ordinary Paxos.  More precisely, it
implements (a variant of) Paxos whose processes are the non-malicious
processes in the Liskov-Paxos algorithm.  The refinement mapping is
not trivial.

Leslie

[ernie...@gmail.com]

With (interesting program) = Paxos, I intended "specification of (interesting program)" to mean consensus. You can use TLC to check that any model - even Liskov-Paxos - implements consensus without having to invent a refinement map. What you can't do is check that it implements Paxos (except for those cases where it does so fairly directly).

It makes sense for someone trying to prove the correctness of Liskov-Paxos to prove that it implements Paxos. It doesn't make sense for someone who wants to check Liskov-Paxos to check that it implements Paxos, when you could instead just check that it implements consensus.

[kiss...@gmail.com]

I am do a survey on formal method.
Could i get i copy of this paper.
Thanks

Lei
2014年6月13日金曜日 4時50分21秒 UTC+9 Chris Newcombe:

> 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.
>
>
>
>

[biro...@gmail.com]

12 Haziran 2014 Perşembe 22:50:21 UTC+3 tarihinde Chris Newcombe yazdı:

> 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

If you are still honoring requests, I would like to get a copy of the paper. Thanks.

Birol Aygun
biro...@gmail.com

[yinyi...@gmail.com]

Hi Chris,

I would like a copy of the paper please.

Thanks,

yinyin

[yaakov...@gmail.com]

On Thursday, June 12, 2014 at 10:50:21 PM UTC+3, 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

Hey Chris,

Can I get a copy?

Many thanks,
Yaakov

[jarjuk]

Hello,

Could You please send a copy also to me.

jarjuk -at- gmail

BR,

Jukka

[masan...@gmail.com]

On Thursday, June 12, 2014 at 12:50:21 PM UTC-7, 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

Hello Chris,
Would you still have a copy available? I'd like to read more about TLA+ and Amazon's use of formal methods in general.

Thanks
Mark

[m...@jspha.com]

Hi Chris,

I'd love a copy of "Why Amazon Chose TLA+". Thanks!

[carl...@gmail.com]

Hi Chris, if you're still honoring requests for this paper I would love to get a copy :)

[dkk...@gmail.com]

Hello Chris,

I appreciate it has been a few years, but I have only just read your paper on "How AWS uses Formal Methods", and would be very interested to read your "Why Amazon Chose TLA+" paper, if you would kindly email me a copy.

I come from a Z background, so my interest in TLA+ is fairly straightforward :)

All the best,

Dan
dkk[dot]pub[at]gmail[dot]com

[Dan ny]

Looks like my original reply was eaten by a grue ;)

I'd love a copy of this paper please!

All the best,

Dan
dkk.pub[at]gmail.com

[niket....@sjsu.edu]

Hi Chris, I would love a copy of the paper too (niket....@sjsu.edu). I am an MS CS student at San Jose State University, working on a project on TLA+.

[Dan ny]

Thank you very much.

A highly engaging read. :)

Congratulations for writing such an interesting paper!

On Sep 29, 2017 13:57, "Chris Newcombe" <chris.n...@gmail.com> wrote:

Hi Dan,

I've attached the paper.

cheers,

Chris

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.

Visit this group at https://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/UwYW6XqyDvE/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.

Visit this group at https://groups.google.com/group/tlaplus.

[ste...@apostolou.info]

Hi Chris,

I'd love a copy of this paper too.

Kind regards,

Steven
steven[at]altheatec.com

[Pedro Paiva]

Hi Chris,

I would like a copy of the paper too (pedroarbs at gmail dot com). Thank you.

Regards,
Pedro

[aren....@gmail.com]

On Thursday, June 12, 2014 at 12:50:21 PM UTC-7, 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

I'd love a copy as well.

Thanks.

[adith...@gmail.com]

I would really appreciate a copy!

Thanks

 

Adithya

[Nikola Kasev]

Hello Chris,

If you're still reading this topic, I'd like a copy of your paper too.

Best regards,
- Nikola

[mike.vo...@gmail.com]

On Thursday, June 12, 2014 at 10:50:21 PM UTC+3, 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

I would love to have a copy too!

Thanks

Mikhail

[Khalid Labs]

hi

I would love to get a copy.

cheers,

Khalid

[Iulian Popescu]

I would like to have a copy of the paper.

Thanks,

Julian

[Matthew Liu]

I would like a copy of this paper too.

Thank you,

Matt

[Isaac DeFrain]

I’d also like a copy when you get the chance. Thanks, Chris.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/858f07da-3c19-4b8b-9e33-d98aaf2de6cfn%40googlegroups.com.

--

Isaac DeFrain

[Vadim Cargatser]

I would also like to have a look in it, if possible. Thank you!

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAM3xQxEevJN6EO7PEczBerLh-gtt_2694vQUFc8-g7dnFUjqrg%40mail.gmail.com.

[Алексей Тимаков]

Yes, it would be great to see their arguments. I also want to see the paper mentioned

среда, 17 февраля 2021 г. в 22:16:18 UTC+3, isaacd...@gmail.com:

[s nedunuri]

The paper has been publicly available for quite some time. Chris posted that announcement some 8 years ago.