[zeromq-dev] design communication protocols

andrea crotti andrea.crotti.0 at gmail.com
Fri Aug 17 13:29:41 CEST 2012


2012/8/17 Andrew Hume <andrew at research.att.com>:
> yes!
> you have discovered that devising a distributed computation is almost
> isomorphic
> to designing the protocol the distributed parts use to communicate.
>
> this is, in general, quite hard, and i know of no useful shortcuts other
> than
> to try and build on existing patterns (such as in teh Guide).
> i have used one method which, although somewhat tedious, did actually work.
>
> the protocol part of teh code was written in pseudocode with m4 macros.
> when you "compiled" the pseudocode, it produced two outputs:
> 1)  working C code
> 2) working Spin code (this language used to be called Promela).
>
> Spin is a protocol verifier which can handle fairly large protocols.
> the build process verified that the protocol was "correct" (taht is,
> it had no deadlocks etc) and then built the executable.
>
> there were occasional missteps in ensuring the two parts were equivalent,
> but i will say we never had a protocol botch. that is, we never deadlock'ed
> or wedged because of a protocol error. these had all been caught
> during compiling.
>
> obviously, none of this was specific to spin; any protocol verifier would
> work, i think.
>

Uhm that's really interesting, I used spin a long time ago in
university but I didn't even think it might be useful now, and it's
probably a very neat idea to formally verify the protocols..

Would you mind to share a simple example maybe?  I will use Python and
might generate the spin code from there too, but would still be nice
to see something running..



More information about the zeromq-dev mailing list