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

[John Lång]

Hi Brett,

Thanks again for your answers!

About HWM, do you think it would make sense assuming a HWM of 1 in the 
model? I think HWM 1 would be the worst case scenario where messages are 
most likely to be dropped. HWM 1 would mean that there can be only 
either one small or one large message in transit at a time. If the 
system satisfies (at least safety) properties in such harsh environment, 
then these properties must also hold when HWM is increased, right? 
Increasing HWM in the model would increase the size of the state space 
exponentially, if I'm not mistaken, and I already have many other 
parameters causing exponential growth. (Last time I tried, 2 TB of RAM 
wasn't enough for simulating even three messages.)

I'm not verifying real-time properties such as latency. These will have 
to be estimated through empirical trials.

Cheers,
John

Brett Viren via zeromq-dev kirjoitti 3.11.2020 klo 18.53:
> Over what bandwidth?
It's hard to estimate the actual numbers in production, but in 
simulations we've achieved data rates around 50 MB/s. Our network 
bandwidth is 10 Gb/s, so 50 MB/s (i.e. 400Mb/s) isn't even near the 
saturation point. We should have plenty of safety margin for our 
application. (This safety margin maybe even as high as 100-1000 times 
the current measured average throughput of the system, but the system is 
being upgraded and the data flow is expected to increase substantially.)
> My own tests at 100 Gbps bandwidth found zero copy less important than
> other things and these other things bring their own problems.
In retrospect, our solution might be unnecessarily complicated. We 
didn't know in advance what level of performance we'd get when designing 
the system. We've put hundreds of hours of work into our simulations so 
we're not going to change the system design anymore at this point. Also, 
there's a deadline approaching. Hence, I'll just have to endure my 
zero-copy approach.