Darren New wrote: > Andrew Lentvorski wrote: >> All you are verifying is that for any state S, there exists a way to >> leave that state. That's not that hard a problem. Tedious, yes, but >> not hard. > > No. Actually, it's so tedious, it's extremely difficult, even for > computers. It's an exponential problem, which works well only for very > small problems. His sample has two processes, each of which executes two > instructions, and he winds up with 45 states. 7 incrementers, each > running one instruction, takes 675 megabytes of memory to track.
W ... T ... F ?!?!? > Look at peculiarity number five: "Don't make loops. Especially infinite > loops." Not very useful for describing servers. Or, well, anything useful really. Practically every state machine which has deadlock problems has loops. > I worked with a guy in grad school who did *exactly* this work as a > graduate thesis on an actual formal language (called Estelle, if you > care) with actual definitions for what the language meant, what "atomic" > vs "interleaved" was, and so on. Doing brute-force checking of > algorithms is easy, but ineffective for anything but the smallest > algorithms. > > There are also languages (like LOTOS) which people have been able to > translate into executables (with great effort) but which you can prove > various things about (like compatibility between versions, progress over > certain timeframes, and so on). Most of my experience with this kind of stuff comes from VLSI with verifying interprocessor communication and/or cache coherency protocols. Generally, we were translating from a hardware description language into a formal verification language and then trying to prove the equivalence. It was tedious, but it could be done. Yes, the computers crunched a long time and there were a *lot* of pruning tricks to avoid the combinatorial explosion of states. -a -- [email protected] http://www.kernel-panic.org/cgi-bin/mailman/listinfo/kplug-lpsg
