[zeromq-dev] Formally modelling the publish-subscribe pattern

[Bill Torpey]

Hi John:

I’ll help where I can — pls see embedded comments.

Also, shameless plug: you may want to check out OZ (https://github.com/nyfix/OZ) — this is an “out of the box” implementation of ZeroMQ as the transport layer for OpenMAMA (https://www.openmama.org/).  It may provide a simple way to run some test code (or at least provide some implementation hints).

I’m interested in your thesis in any case — I’ve been wanting to create a formal model of OZ for some time, and have been dipping my toes into TLA+ (https://en.wikipedia.org/wiki/TLA%2B) for that purpose.  I’m curious if you’ve considered TLA+ and if so what prompted you to choose PROMELA?

Good luck with your thesis, and I’d very much like to review it when you’ve got something suitable.

Regards,

Bill Torpey

> On Oct 15, 2020, at 5:23 AM, John Lång <john.lang at mykolab.com> wrote:
> 
> Hello,
> 
> (Hopefully this message didn't get duplicated...) As part of my master's thesis, I'm building a formal model for my distributed system using PROMELA. The system I'm modelling uses 0MQ publish-subscribe pattern. I have some questions about the pattern. I'd really appreciate all answers to these questions! I'm now looking at the informal specification at https://rfc.zeromq.org/spec/29/ <https://rfc.zeromq.org/spec/29/>
> The specification mostly looks clear. However, I'm a bit confused about these two bullet points:
> 
> SHALL create a queue when initiating an outgoing connection to a subscriber, and SHALL maintain the queue whether or not the connection is established.
> SHALL create a queue when a subscriber connects to it. If this subscriber disconnects, the PUB socket SHALL destroy its queue and SHALL discard any messages it contains.
> What is the difference between initiating an outgoing connection to a subscriber and a subscriber connecting to a publisher? In the C++ source code of my system, a publisher binds to a PUB socket and a subscriber connects to the address of a publisher. I guess this sounds more like the second point, but I'm not certain.
> 
This is an implementation detail, but can be important in some use-cases.  Basically, when a SUB connects to a PUB, subscription information is exchanged between the SUB and PUB as part of the connect handshake — when a PUB connects to a SUB an additional set of messages is required to communicate subscription information from the SUB to the PUB.  This matters because, for most protocols, filtering is done by the PUB, so the PUB will not send messages until it knows that the SUB is interested in them.  In practice, this means that when a SUB connects to a PUB, the SUB will immediately start receiving messages — in the other direction, there is a “window” where some number of messages that are published immediately following the connect may not be sent to SUB.

There’s been a lot of discussion of this in the ZeroMQ community, for instance https://github.com/zeromq/libzmq/issues/2267.  Note that the canonical solution for this (calling zmq_poll after connect, as per https://gist.github.com/hintjens/7344533) is NOT reliable — there is still a window, although calling zmq_poll does often reduce the window size such that things appear to work.

> Did I understand correctly that this message queue between a publisher and a subscriber works FIFO? It says that for outgoing messages, "SHALL silently drop the message if the queue for a subscriber is full." Does this imply that those messages that fit in the queue are delivered in the order they were sent in? I take it that the queue being full means that the high water mark has been exceeded.
> 
Our testing was done not on queue full, but on socket disconnect/reconnect, but the principle is the same.  Any queued messages are delivered in order, and any messages dropped are dropped from the tail of the queue.  So a typical sequence at a subscriber would look something like this if the queue fills up after message #3 and then is drained before message #10 is sent:

1 .. 2 .. 3 .. <queue full> .. 10, 11, 12

> What is a binary comparison? Is it the same as bitwise comparison?
> 
Yes.

> To me, "binary comparison" sounds like just comparing two things with each other.
> 
> Currently, I'm modelling my 0MQ publish-subscribe connections as arrays in PROMELA. After all, the specification for the publisher says that processing outgoing messages "SHALL NOT block on sending". Another reason for my decision is that I have multiple publishers and subscribers and a fixed message queue length, so a three-dimensional array is handy for accessing the messages. Is there a way for achieving sensible channel semantics for 0MQ publish-subscribe pattern?
> 
> I wonder if there's already a formal specification for 0MQ publish-subscribe pattern out there somewhere... I should probably do some more research to see if I can find related work on this matter.
> 
If you do I’m sure that the community would love to know about it, as would I.

> Best regards,
> John Lång
> _______________________________________________
> zeromq-dev mailing list
> zeromq-dev at lists.zeromq.org
> https://lists.zeromq.org/mailman/listinfo/zeromq-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.zeromq.org/pipermail/zeromq-dev/attachments/20201015/bae1b560/attachment.htm>