Messages in this thread | | | Subject | Re: [patch 1/2] x86_64 page fault NMI-safe | From | Steven Rostedt <> | Date | Wed, 11 Aug 2010 10:44:09 -0400 |
| |
On Fri, 2010-08-06 at 10:13 -0400, Mathieu Desnoyers wrote: > * Peter Zijlstra (peterz@infradead.org) wrote:
> Less code = less instruction cache overhead. I've also shown that the LTTng code > is at least twice faster. In terms of complexity, it is not much more complex; I > also took the extra care of doing the formal proofs to make sure the > corner-cases were dealt with, which I don't reckon neither Steven nor yourself > have done.
Yes Mathieu, you did a formal proof. Good for you. But honestly, it is starting to get very annoying to hear you constantly stating that, because, to most kernel developers, it is meaningless. Any slight modification of your algorithm, renders the proof invalid.
You are not the only one that has done a proof to an algorithm in the kernel, but you are definitely the only one that constantly reminds people that you have done so. Congrats on your PhD, and in academia, proofs are important.
But this is a ring buffer, not a critical part of the workings of the kernel. There are much more critical and fragile parts of the kernel that work fine without a formal proof.
Paul McKenney did a proof for RCU not for us, but just to help give him a warm fuzzy about it. RCU is much more complex than the ftrace ring buffer, and it also is much more critical. If Paul gets it wrong, a machine will crash. He's right to worry. And even Paul told me that no formal proof makes up for large scale testing. Which BTW, the ftrace ring buffer has gone through.
Someday I may go ahead and do that proof, but I did do a very intensive state diagram, and I'm quite confident that it works. It's been deployed for quite a bit, and the design has yet to be a factor in any bug report of the ring buffer.
-- Steve
| |