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

[John Lång]

Hi Bill,

I hadn't heard about OZ when I started my project that now relies on 
0MQ. The tech stack was largely chosen by my supervisor and co-workers. 
Now the priority is to get the system verified and in production as soon 
as possible. Thus, at this point we must stick with the current 
dependencies. Anyway, this OZ does seem interesting...

About Spin, I mainly chose it because I had used it with success in my 
earlier work that relates to the thesis. I'll list some other points 
that come into my mind:

- I find the PROMELA language to be intuitive and elegant for 
formalising asynchronous systems. I like the way how PROMELA resembles a 
programming language. The TLA+ language seems to be lower level in the 
sense that I need to keep track of program counters etc. Of course 
there's the pluscal language for TLA, but I haven't tried it.
- The TLC model checker seems to be quite a bit slower than Spin. This 
is more like the first impression than an informed opinion, though. It 
could be the case that TLC just has more overhead that slows down the 
verification of small models but which becomes unnoticeable on larger 
models.
- The TLA+ IDE does feel much better than iSpin or jSpin. However, I 
personally prefer the simplicity of the Emacs PROMELA mode.
- I find the theory behind Spin and enumerative model checking (guarded 
commands language, Büchi automata) easier to understand than that of 
symbolic model checking (CSPs, SAT, SMT, DPLL, CDCL, BMC, IC3, etc.). 
Direct construction with automata feels more comfortable for me than the 
more analytical encodings and constraint satisfaction problems. Of 
course, your mileage may vary. Some understanding on how the model 
checker works helps fighting the state space explosion.
- I've read Mordechai Ben-Ari's book "Principles of the Spin Model 
Checker", and it was a great tutorial. It was much more understandable 
for me than Leslie Lamport's TLA Hyperbook and other resources.

Of the four model checkers I've tested (Spin, NuSMV, TLA+, and DIVINE) I 
find Spin the easiest to use. This is not to say that Spin itself is 
easy to use. Frankly, the output formatting of Spin verifier executables 
is horrible. Understanding counter examples can take much work.

Best regards,
John

On 15.10.2020 17.11, Bill Torpey wrote:
> 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 <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/ <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 
> <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 
>> <mailto: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/
>>
>> 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 
> <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 
> <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 <mailto:zeromq-dev at lists.zeromq.org>
>> https://lists.zeromq.org/mailman/listinfo/zeromq-dev
>
>
> _______________________________________________
> 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/20201016/b0c1a448/attachment.htm>