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 <[email protected]>: >> 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 > [email protected] > http://lists.zeromq.org/mailman/listinfo/zeromq-dev ------------------ Andrew Hume (best -> Telework) +1 623-551-2845 [email protected] (Work) +1 973-236-2014 AT&T Labs - Research; member of USENIX and LOPSA
_______________________________________________ zeromq-dev mailing list [email protected] http://lists.zeromq.org/mailman/listinfo/zeromq-dev
