5 ms·

On the other hand this is the kind of bugs you'd expect to see when programmers rely too heavily on the tests to catch bugs.

shakna 8y ago
It takes 20 lines to reproduce the bug minimally, and relies on a confluence of code-generator bugs. I believe most fuzzers would take a considerable amount of time to find a bug like this... How are you suggesting a team on a very large project find this elsewise?
- jessaustin 8y ago
  rely too heavily on the tests Presumably they are to find it using something besides tests? Intuition? Casting lots? Code review?
  - lifthrasiir 8y ago
    I think the intention was to embrace formal methods, which "proves" the absence of bugs (to the limited extents though). For a heavily-used critical piece of code like SQLite the lack or weak use of formal methods might actually be a reasonable criticism. EDIT: Not meant to say that the original comment was reasonable.
    - shakna 8y ago
      Surprisingly SQLite does actually embrace formal methods in various places. Such as, in their draft goals [0], under S30200, they outline a memory allocator goal by referring to a proof. Though, if the parents goal was to imply that the whole of SQLite should be verified... I'm not convinced its entirely possible. Quite a lot of SQLite revolves around things around where the halting problem may come into play. [0] http://www.sqlite.org/draft/sysreq.html http://www.sqlite.org/draft/sysreq.html
      - adrianN 8y ago
        Almost all things you'd want to prove about a program are undecidable in the general case. That doesn't mean much about the particular case of your program.
      - im3w1l 8y ago
        A computer program should be written to never* deadlock, and that implies that the programmers have a vague proof sketch in their head of why it doesn't deadlock that could if needed be formalized as a proof. *I'm sure there is some exception out there but it doesn't matter for this argument.
      - Jweb_Guru 8y ago
        What things that SQLite does revolves around anything halting-problem related? Almost all SQLite queries are over a finite amount of data and have a well-specified legal solution set that barely requires recursion; WITH RECURSIVE doesn't have to halt but still has a well-defined semantics where it does. I think even most optimization problems on SQL queries are decidable; you have to want to do quite interesting things (like prove query subsumption) before you get into undecidability territory.
        shakna 8y ago
        I see two main areas where the halting problem comes into play: SQLite involves extensive amounts of IO, it's a flat-file database most of the time, afterall. That is inherently unsafe, and can't be proven to terminate. SQLite also has an internal VM, for which it generates code (the source of the bug in this article). The VM is Turing-Complete, hence you can't always prove that it will terminate.
        Jweb_Guru 8y ago
        > SQLite involves extensive amounts of IO, it's a flat-file database most of the time, afterall. That is inherently unsafe, and can't be proven to terminate. Under reasonable assumptions about I/O (POSIX APIs and stuff), you can certainly prove termination of such operations. > SQLite also has an internal VM, for which it generates code (the source of the bug in this article). The VM is Turing-Complete, hence you can't always prove that it will terminate. You don't have to always prove any VM program will terminate. You just have to show termination-preserving refinement of the SQLite code generator (as I alluded to in my other post). You don't even need types for this.
- contravariant 8y ago
  Looks like somewhere along the lines my comment got interpreted as criticism rather than merely an observation, that wasn't my intent. Anyway I'm not suggesting they find it elsewise. In fact as you rightfully pointed out finding bugs like this is incredibly hard. However surely those code-generator bugs could have been spotted earlier? The reason they weren't was because they didn't cause any obviously wrong behaviour, which made it hard to find them using test, but as long as you pay attention you can still spot them (as evidenced by the fact that they were eventually fixed). So if you're wondering how a bug like this might have slipped past their 'extensive test coverage', I felt it was important to point out that putting too much trust in those test is also a viable explanation. Not necessarily the right explanation, as I have no way of knowing the situation at SQLite, but a possible explanation.

shakna 8y ago

It takes 20 lines to reproduce the bug minimally, and relies on a confluence of code-generator bugs. I believe most fuzzers would take a considerable amount of time to find a bug like this... How are you suggesting a team on a very large project find this elsewise?

jessaustin 8y ago
rely too heavily on the tests Presumably they are to find it using something besides tests? Intuition? Casting lots? Code review?
- lifthrasiir 8y ago
  I think the intention was to embrace formal methods, which "proves" the absence of bugs (to the limited extents though). For a heavily-used critical piece of code like SQLite the lack or weak use of formal methods might actually be a reasonable criticism. EDIT: Not meant to say that the original comment was reasonable.
  - shakna 8y ago
    Surprisingly SQLite does actually embrace formal methods in various places. Such as, in their draft goals [0], under S30200, they outline a memory allocator goal by referring to a proof. Though, if the parents goal was to imply that the whole of SQLite should be verified... I'm not convinced its entirely possible. Quite a lot of SQLite revolves around things around where the halting problem may come into play. [0] http://www.sqlite.org/draft/sysreq.html http://www.sqlite.org/draft/sysreq.html
    - adrianN 8y ago
      Almost all things you'd want to prove about a program are undecidable in the general case. That doesn't mean much about the particular case of your program.
    - im3w1l 8y ago
      A computer program should be written to never* deadlock, and that implies that the programmers have a vague proof sketch in their head of why it doesn't deadlock that could if needed be formalized as a proof. *I'm sure there is some exception out there but it doesn't matter for this argument.
    - Jweb_Guru 8y ago
      What things that SQLite does revolves around anything halting-problem related? Almost all SQLite queries are over a finite amount of data and have a well-specified legal solution set that barely requires recursion; WITH RECURSIVE doesn't have to halt but still has a well-defined semantics where it does. I think even most optimization problems on SQL queries are decidable; you have to want to do quite interesting things (like prove query subsumption) before you get into undecidability territory.
      - shakna 8y ago
        I see two main areas where the halting problem comes into play: SQLite involves extensive amounts of IO, it's a flat-file database most of the time, afterall. That is inherently unsafe, and can't be proven to terminate. SQLite also has an internal VM, for which it generates code (the source of the bug in this article). The VM is Turing-Complete, hence you can't always prove that it will terminate.
        Jweb_Guru 8y ago
        > SQLite involves extensive amounts of IO, it's a flat-file database most of the time, afterall. That is inherently unsafe, and can't be proven to terminate. Under reasonable assumptions about I/O (POSIX APIs and stuff), you can certainly prove termination of such operations. > SQLite also has an internal VM, for which it generates code (the source of the bug in this article). The VM is Turing-Complete, hence you can't always prove that it will terminate. You don't have to always prove any VM program will terminate. You just have to show termination-preserving refinement of the SQLite code generator (as I alluded to in my other post). You don't even need types for this.
contravariant 8y ago
Looks like somewhere along the lines my comment got interpreted as criticism rather than merely an observation, that wasn't my intent. Anyway I'm not suggesting they find it elsewise. In fact as you rightfully pointed out finding bugs like this is incredibly hard. However surely those code-generator bugs could have been spotted earlier? The reason they weren't was because they didn't cause any obviously wrong behaviour, which made it hard to find them using test, but as long as you pay attention you can still spot them (as evidenced by the fact that they were eventually fixed). So if you're wondering how a bug like this might have slipped past their 'extensive test coverage', I felt it was important to point out that putting too much trust in those test is also a viable explanation. Not necessarily the right explanation, as I have no way of knowing the situation at SQLite, but a possible explanation.