I wonder if we are reaching the point where we would need to write formal proofs for parts of the kernel code.
How to ruin Linus's vacation
Posted Jul 19, 2011 20:48 UTC (Tue) by smurf (subscriber, #17840) [Link]
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.
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]
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 (guest, #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.
How to ruin Linus's vacation
Posted Jul 19, 2011 20:54 UTC (Tue) by kleptog (subscriber, #1183) [Link]
It happens frequently that a cache introduced for performance actually contains some race condition. One way of checking this is to make the cache throw away entries almost immediately, this has a way of stress testing certain failure modes. I wonder if that would have helped here.
In any case, testing assertions in the face of race conditions is something we could all use. There is software proving software that tries but the false positive rate is still too high. I truly hope that in the future we will have good tools for this, because complexity is only getting worse.
How to ruin Linus's vacation
Posted Jul 19, 2011 23:03 UTC (Tue) by Ben_P (guest, #74247) [Link]
How to ruin Linus's vacation
Posted Jul 19, 2011 21:57 UTC (Tue) by tshow (subscriber, #6411) [Link]
At least as I understand the state of the art in formal code proofs, the only place they work is places where they aren't particularly useful; places where things like timing, instruction reordering, hardware errors and concurrency are not considerations.
Copyright © 2017, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds