Hi Bill,
Sounds like an interesting project! Sounds like you have already done
interesting work on on it. I'll have a look at it on weekend.
Cheers,
John
Bill Torpey kirjoitti 7.3.2022 klo 21.34:
Hi John:
Our ZeroMQ project (https://github.com/nyfix/OZ) uses PUB/SUB to provide
discovery for network peers, as documented here:
https://github.com/nyfix/OZ/blob/master/doc/Naming-Service.md
We added “heartbeating” to the protocol because we weren’t able to prove
conclusively that the startup sequence was sufficient to guarantee that we
could never miss a connection message, but intuitively it seems that the
heartbeats are probably unnecessary.
I’d certainly be interested in working with you to try to come up with a formal
proof, either way.
Best Regards,
Bill Torpey
On Mar 7, 2022, at 1:10 PM, John Lång <[email protected]> wrote:
Hello,
I've been developing tooling for the Spin model checker (see
https://spinroot.com). I'd like to try out my tools in a real life case study.
Do you think it would be feasible to build an abstract model for some aspect of
the specification of ZeroMQ, e.g. the PUB-SUB mechanism? Is there anyone who
would be interested in becoming a co-author for a study?
Best regards,
John Lång
_______________________________________________
zeromq-dev mailing list
[email protected]
https://lists.zeromq.org/mailman/listinfo/zeromq-dev
_______________________________________________
zeromq-dev mailing list
[email protected]
https://lists.zeromq.org/mailman/listinfo/zeromq-dev
_______________________________________________
zeromq-dev mailing list
[email protected]
https://lists.zeromq.org/mailman/listinfo/zeromq-dev
