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/
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.
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.
What is a binary comparison? Is it the same as bitwise comparison? 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.
Best regards,
John Lång
_______________________________________________
zeromq-dev mailing list
zeromq-dev@lists.zeromq.org
https://lists.zeromq.org/mailman/listinfo/zeromq-dev
