User: Password:
|
|
Subscribe / Log in / New account

How to ruin Linus's vacation

How to ruin Linus's vacation

Posted Jul 19, 2011 20:00 UTC (Tue) by cesarb (subscriber, #6266)
Parent article: How to ruin Linus's vacation

> The behavior of the dentry cache is, at this point, so subtle that even the combined brainpower of developers like Linus, Al, and Hugh has a hard time figuring out what is going on. [...] But if we reach a point where almost nobody can understand, review, or fix some of our core code, we may be headed for long-term trouble.

I wonder if we are reaching the point where we would need to write formal proofs for parts of the kernel code.


(Log in to post comments)

How to ruin Linus's vacation

Posted Jul 19, 2011 20:48 UTC (Tue) by smurf (subscriber, #17840) [Link]

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.

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 (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]

I'm not sure about complete proofs, but we do need better tools for testing certain assertions with respect to race conditions.

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]

It's also important to note than when working in languages with the freedom that C gives you, determining accurate life times and reference counts can be hellish if very strict coding conventions are not adhered to.

How to ruin Linus's vacation

Posted Jul 19, 2011 21:57 UTC (Tue) by tshow (subscriber, #6411) [Link]

The trouble with formal proofs is that the logical errors and bad assumptions made when writing the code tend to be propagated into the formal proofs, where they typically remain equally unnoticed. Or worse, the proof is fine, but the code deviates in subtle ways due to abstraction mismatches and model simplification.

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