| |||||||||||||
How to ruin Linus's vacationHow to ruin Linus's vacationPosted Jul 19, 2011 20:48 UTC (Tue) by smurf (subscriber, #17840)In reply to: How to ruin Linus's vacation by cesarb Parent article: How to ruin Linus's vacation
Unfortunately, any VFS operation needs to be formally described not as in "X happens", but as in "there is an arbitrarily complex state Y which is transformed into the almost-identical state Y', and the only relevant difference between Y and Y' is X". (There may be non-relevant differences, e.g. cache state.)
Add in the fact that the kernel is reentrant (formal descriptions for concurrent processes? Dream on) and has the aforementioned caching and RCU and whatnot (so for each file there are multiple valid pre- and postconditions), and you're in for a _real_ treat.
I very much doubt that anybody can manage this for any specific non-trivial testcase, much less in general.
(Log in to post comments)
How to ruin Linus's vacation Posted Jul 20, 2011 3:24 UTC (Wed) by bfields (subscriber, #19510) [Link] Well, it's also true that you can't write purely "formal" proofs for most mathematical theorems. And yet, mathematics gets done, because people can write perfectly good proofs in ordinary language. And in fact anyone that writes non-trivial code probably does form in their head at least a hand-wavy proof of its correctness. If those actually got written down, it would probably help clarify thinking and avoid some bugs. But that doesn't happen for the same reason that nobody writes documentation. An example of an exception: Documentation/filesystems/directory-locking.
How to ruin Linus's vacation Posted Jul 20, 2011 4:05 UTC (Wed) by viro (subscriber, #7872) [Link]
Yeah, well... you forgot to add "and actually read" to conditions... Exhibit A: people adding hardlinks to directories or equivalents thereof, despite the aforementioned example of documentation ;-/
We do need such writeups, of course. If nothing else, writing them tends to find holes - see e.g. ->d_lock mess discussion on fsdevel lately. There the locking order had been fscked in head (not transitive, for one thing), but locks outside of that set had mostly avoided bad trouble. Trying to write the proof of correctness hadn't been fun (and what I've got still relies on unverified assumptions about the things filesystem code does not do; verifying those has already caught a bunch of really broken things), but it helped to catch rather nasty stuff. Simply by reasoning about the properties of counterexample - i.e. "what would a deadlock have to look like". It's math, like any other...
FWIW, I wonder what backgrounds people have - in my case, it's geometry and topology and _that_ has certainly helped to acquire many mental habits useful for that kind of work...
How to ruin Linus's vacation Posted Jul 20, 2011 23:02 UTC (Wed) by bfields (subscriber, #19510) [Link] Yeah. Especially for CS students, something like the classic first point-set topology course might give good experience with that kind of proof-or-counterexample mode of problem solving. I think that's rare, unfortunately, at least outside a few countries with very rigorous math programs?(Like some others, I'm a refugee from mathematics, coming late to this after getting a PhD (commutative algebra and some algebraic topology). Not a particularly smart career path, but fun in its own way.)
How to ruin Linus's vacation Posted Jul 21, 2011 23:34 UTC (Thu) by fuhchee (subscriber, #40059) [Link] "there is an arbitrarily complex state Y which is transformed into the almost-identical state Y', and the only relevant difference between Y and Y' is X"That sounds like the AI Frame Problem.
|
|||||||||||||