[lkml]   [1998]   [Jul]   [30]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
Messages in this thread
    SubjectRe: [patch] IDE problems on SMP, fixed? (fwd)
    Linus Torvalds writes:
    > Well, if we had a static analysis tool we'd obviously be able to track a
    > lot of things that we can't currently track. You could build a tree of all
    > calling sequences, and statically verify quite a few rules. You might not
    > prove correctness, but you could find a lot of things like this.
    > Dreaming? Yes.


    Nah, it's not hard.

    First, you rewrite the kernel in ML... ;)


    But this has set me wondering. Is it remotely possible to do something
    like this? An assertion-checking tool like GNU nana could help, but
    that particular tool - and, probably, all similar tools - have the
    disadvantage that they render your source almost illegible :(

    Strictly speaking if we wanted a generic tool we'd need to verify a
    lot more than calling sequences. There's calling thru function
    pointers, for a start (does that go on to any significant degree
    within the kernel, though? For context switches it obviously has to
    but that's accompanied by ring transitions &c so it hardly counts;
    we're not trying to validate user-level too)...

    I shall have to think about this.

    `It is inelegant and it was hacked on. But it was hacked on with
    careful consideration.' - PLA on perl and OO

    To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
    the body of a message to
    Please read the FAQ at

     \ /
      Last update: 2005-03-22 13:43    [W:0.021 / U:12.880 seconds]
    ©2003-2017 Jasper Spaans. hosted at Digital OceanAdvertise on this site