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.
--
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.
I also would like to receive a copy.
Thanks,
Marcelo
I'd also like a copy.
Thanks!
Tim
--
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.
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.
>>... 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 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
--
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
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
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
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
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.
If you're still reading this topic, I'd like a copy of your paper too.
Best regards,
- Nikola
--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAM3xQxEevJN6EO7PEczBerLh-gtt_2694vQUFc8-g7dnFUjqrg%40mail.gmail.com.