Specifying Systems fig 3.2 : is my understanding correct?

[lthibault]

Hello,

Apologies for the rather broad question, but as a newcomer to formal methods, figure 3.2 (see attachement) has left me scratching my head.

This spec describes an asynchronous channel interface, which is particularly interesting to me as the engineering problem that led me to learn TLA+ involves asynchronous broadcast.  As such, I'm trying to conceptually anchor my own problem to this very simple spec.  What's "bothering" me is that this spec seems to define a system in which

1. a channel is initially only able to send
2. a channel is able to receive only after having sent
3. a channel oscillates between an "able to send"-state and an "able to receive"-state, which precludes (e.g.) being able to receive twice in a row

I believe 1 to be true because Init states that chan.ack = chan.ready, which is a precondition for entering a Send state.

I believe 2 to be true because Send transitions to a state where ack != rdy and Rcv  transitions to a state where ack = rdy.

I believe 3 to be true because, Rcv requires chan.rdy != chan.ack.

My questions are as follows:

1. Is my reading of the spec correct, or have I missed something?
2. Is this a toy example of an asynchronous send/recv interface that was simplified for pedagogical purposes, or is there some reason why such an interface must behave in this way?

Thank you very much in advance for your insight.  In the meantime, thank you very much, Dr. Lamport, for your extremely helpful book and video series!

Regards,

[Stephan Merz]

Hello,

you are not misreading the specification: the explanation at the beginning of chapter 3 clearly states:

The sender must wait for an acknowledgement [...] for one data item before it can send the next.

Specifications are definitions, they are not right or wrong in themselves, but they are written for a purpose. It sounds like the system that you are thinking about must be able to buffer several (an unbounded number of?) messages. Chapter 4 contains a specification of a FIFO buffer (still using the elementary channels of chapter 3 for communicating between the sender and the buffer, and between the buffer and the receiver). There are many other possible specifications. For example, the FIFO buffer is not appropriate if you do not assume that the order of messages is preserved. At a high level of specification, perhaps you do not wish to make the buffer explicit as a component linked to the sender and receiver processes by channels, but rather let the sender(s) and receiver(s) put and retrieve messages into the buffer directly. So, don't be afraid to deviate from the specs you find in the book.

Regards,

Stephan

--
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 https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
<Screen Shot 2017-11-04 at 16.07.01.png>

[lthibault]

Hi Stephen,

Thanks very much for your reply.  This does indeed clarify things.

>Specifications are definitions, they are not right or wrong in themselves, but they are written for a purpose

Yes, this makes perfect sense (and was very well explained in the book)!  I was mainly trying to determine if I hadn't properly understood the spec, or whether this wasn't quite the spec that matched my needs -- apparently it's the latter, which is encouraging.

In any case, thank you for the detailed answer.  I'm sure I'll be back with more questions very soon!

Best regards,