lkml.org 
[lkml]   [2010]   [Aug]   [11]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    SubjectRe: [patch 1/2] x86_64 page fault NMI-safe
    From
    Date
    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




    \
     
     \ /
      Last update: 2010-08-11 16:47    [W:4.214 / U:0.088 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site