Re: [patch 1/2] x86_64 page fault NMI-safe

[Steven Rostedt <rostedt@goodmis.org>]

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