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.
Now go verify a multi-user FTP server, including modeling the file system.
Look at peculiarity number five: "Don't make loops. Especially infinite
loops." Not very useful for describing servers.
Look at "Promela coding tricks": All of them are descriptions of
(essentially) unrealistic ways to reduce state space explosion.
Go down to "Running the QRCU example." His QRCU looks like about 100
lines of C-level code. He guesses that having three readers and three
writers takes about a terabyte of memory. Tedious, but not difficult.
While it's difficult to be sure, I don't see any actual counters in the
body of algorithms. Nothing like "serve this if there are five or fewer
users connected, or that if there are more than five." This too leads to
tremendous state-space explosion.
Plus, once it's written, there doesn't seem to be much you can do with
it. It might be interesting to verify things like your mutex lock
subroutine is valid, but it certainly isn't going to work well for (say)
a network protocol.
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).
--
Darren New / San Diego, CA, USA (PST)
The primary use of XML is as a technique
to avoid documenting your interchange formats.
--
[email protected]
http://www.kernel-panic.org/cgi-bin/mailman/listinfo/kplug-lpsg
