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

[John Lång]

Hi Brett,

> And, thanks to Bill Torpey's reply, I should clarify I only had TCP
> transport in my mind.
I also only had TCP in my mind. I should have said that.
> Wow, that's some modeling! I don't at all grasp how this formal
> modeling works but I guess in most practical applications a HWM of 1
> would not be very,... well,... "practical". 

I believe the large state space of my model comes from the data and 
redundant processes I'm modelling. I have lots of buffering going on. Of 
course, 0MQ and another protocol that I'm modelling are also 
contributing factors. Model checking usually works best for 
control-intensive and not data-intensive applications.

> Hmm, actually I see zmq_socket_monitor() has[2] a ZMQ_EVENT_DISCONNECTED
> event.  It seems it would allow an app with a SUB to react directly to a
> PUB death without the need to maintain an app-level timeout.
>
> I have never used the socket monitor so don't know its subtleties.  In
> particular, I'd wonder if the "disconnected" event is generated after
> some internal timeout and if so if that would need to be featured in
> your modeling.

This socket monitor thing sounds like something I should look into if I 
ever get to upgrade my system.

0MQ is a mere complication in my model, though. The main focus is in my 
overall distributed system. I think that 0MQ PUB-SUB deserves a model in 
its own right. I think it would be a great topic for a research paper to 
build a formal model of 0MQ PUB-SUB...

Cheers,
John