[zeromq-dev] design communication protocols

Andrew Hume andrew at research.att.com
Fri Aug 17 13:56:18 CEST 2012


regrettably, that code is unavailable to me, but i will see if i can resurrect some of it.

On Aug 17, 2012, at 4:29 AM, andrea crotti wrote:

> 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..
> _______________________________________________
> zeromq-dev mailing list
> zeromq-dev at lists.zeromq.org
> http://lists.zeromq.org/mailman/listinfo/zeromq-dev


------------------
Andrew Hume  (best -> Telework) +1 623-551-2845
andrew at research.att.com  (Work) +1 973-236-2014
AT&T Labs - Research; member of USENIX and LOPSA




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.zeromq.org/pipermail/zeromq-dev/attachments/20120817/bc844363/attachment.htm>


More information about the zeromq-dev mailing list