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
