[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Spec Review Request

Hi Jamie,

    >>I’d hugely appreciate feedback, criticism, and advice for future specs.

I took a quick look.  Here are my comments, mostly aimed at helping with future specs.

- The spec is clear. I particularly like the pervasive use of LET ... IN ... to give useful names to intermediate values and keep the resulting expressions short.  It's worth making a habit of clarity, as it really helps when applying TLA+ to more difficult problems.

- The spec is very well commented.  I mention this because some people don't write comments in specs, and I've seen that cause confusion, bad assumptions, and errors.  So omitting comments is a big mistake when trying to apply TLA+ to difficult problems.  With tricky or complex specs, as with tricky or complex code, I've found it very helpful to follow Leslie's advice to write the comments first -- see http://www.budiu.info/blog/lamport.html

- Leslie also taught me that it's a good idea to explicitly state the purpose of a specification. For example, what aspect of the system's behavior (or perhaps its interaction with its environment) are you trying to clarify?  Alternatively, what kind of design bugs are you trying to find?   Doing this is very useful in my experience.  I've also found that writing down the purpose before starting to write the spec really helps me to choose the level of detail/abstraction for that spec.

     So, I will ask as a rhetorical question:  beyond learning TLA+, what is the purpose of this spec?  What are you trying to clarify or verify?

     From reading the spec, I might guess that the purpose is to clarify some unusual assumptions that you want to make about part of "the environment" of the system, specifically the communication medium (network).  I say that because you have a sub-action, ConsumeMsgAndBroadcastSync, that has coarse-grain concurrency: in a single atomic step it changes the inbox of every process in the system, which implies a strong assumption about the ability to send a group of messages without any concurrent interleaving (somewhat like a transaction).  However, you also have an action of the environment, LoseMsg, that can non-deterministically discard an arbitrary message from any inbox at any time.  Message loss is one of the standard assumptions about weaker communication mediums, but the other standard assumptions --duplicated messages and re-ordered messages-- are not modeled by this spec.  So, together this is an interesting mix of strong and weak assumptions, and I'm curious as to the reason.

     From reading the spec, I might also guess that the purpose is not to verify a safety or liveness property (which is fine if that's your intent).  I say that because the only property in the spec is the type invariant and I doubt that it would ever be worth writing a spec to only verify a type invariant, as they are usually very shallow.   
     Perhaps you intend to later add a property, such as some variant of 'eventual consistency' (really a family of properties).  That could well be worth verifying.  However, I doubt that the spec would satisfy such a property without some changes, as the environment can lose messages but the system (at this level of abstraction) doesn't have a mechanism to re-transmit lost messages.  (Also, the spec doesn't have a liveness assumption, so allows behaviors in which processes simply never consume any more messages from their inbox.)

     If the above guesses are wrong, and the sole purpose of the spec was to learn TLA+ then you've certainly succeeded at learning the language, apparently quite quickly.  However, I'm a little worried that you or your colleagues might feel that you've performed a ritual with no practical value.  If that's the case, I'd encourage you to suspend judgement on the value until you've applied TLA+, with purpose, to a difficult problem.  

I hope this helps,

On Mon, Feb 12, 2018 at 6:46 AM, Jamie White <ja...@xxxxxxxxxxxxx> wrote:
Hi there

As part of a recent hack week, a group of folks at Heroku set about learning TLA+. Amongst other exercises, I wrote a spec for a “toy distributed system” we created last year called HKFM. It’s a radio station/jukebox of sorts and (I think) lent itself nicely to temporal specification.

This is my first spec, so I’d hugely appreciate feedback, criticism, and advice for future specs.

You’ll find the ascii version and PDF here:

Many thanks in advance!


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...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.