4 ms·

This is actually really cool. They tried to verify Timsort as implemented in Python and Java using formal methods. When it didn't seem to work, they discovered

This is actually really cool. They tried to verify Timsort as implemented in Python and Java using formal methods. When it didn't seem to work, they discovered that there was actually a missing case in both implementations, which could lead to array out of bounds exceptions. Really shines as an example of how important proof is in computer science.

stingraycharles 12y ago
In the Haskell community there is a tool called QuickCheck [1]: it is able to generate inputs based on preconditions, and you provide a function to verify the postconditions. I am not sure why these kind of testing methods aren't used more often in other communities, since it makes it really easy to catch corner cases; in the Haskell world, at least, using QuickCheck is somewhat pervasive. [1] https://wiki.haskell.org/Introduction_to_QuickCheck2 https://wiki.haskell.org/Introduction_to_QuickCheck2 EDIT: I have never done this before, but could anyone explain why I am being downvoted? I wasn't making the claim that this is a substitute for a formal proof, I was merely adding this information to the discussion since it seemed relevant.
- im3w1l 12y ago
  It wouldn't catch this bug. The algorithm works for lists of size less than 2^49.
- jdimov 12y ago
  There is triq[1] for Erlang and excheck[2] for Elixir. [1] https://github.com/krestenkrab/triq https://github.com/krestenkrab/triq [2] https://github.com/parroty/excheck https://github.com/parroty/excheck
- Osmium 12y ago
  Just FYI for anyone who's interested, but there's a Swift implementation of QuickCheck described in this book: http://www.objc.io/books/ http://www.objc.io/books/ It's very minimal, but the chapter outlines what you'd need to do to make it more complete and get it on par with the Haskell version. There are also a few versions on GitHub too.
- ekimekim 12y ago
  At a guess: A lack of practical ways to perform such checks without extensive extra knowledge and annotation as seen in the article. A large factor is likely that Haskell is pure by default - something that is reasonably rare in many languages (where a method likely reads (or mutates) state from instance variables or even globals).
  - stingraycharles 12y ago
    I think it also has to do with Haskell's type system. Quickcheck is able to "discover" the bounds within any arbitrary type can operate, and thus makes generating random values within these bounds fairly easy.
    - lclarkmichalek 12y ago
      Eh, you still have to write instances of Arbitrary. And often those instances are not great; wayyy to many libraries are tested with Arbitrary String instances that only generate ascii, for example.
- grandpa 12y ago
  There's a difference, though: QuickCheck randomly tries a large-ish number of possible inputs to try and disprove a postcondition, whereas formal methods prove the postcondition for all inputs. Practically, if the number of possible inputs is huge compared to the number of failure cases, it's unlikely that QuickCheck will find it. I strongly suspect - and this would be an interesting experiment - that QuickCheck wouldn't have found this particular bug, since Timsort has been in use for years without anyone noticing it.
  - TheLoneWolfling 12y ago
    What about AFL?
    - jamesfisher 12y ago
      What's AFL?
      - fpgaminer 12y ago
        American Fuzzy Lop (http://lcamtuf.coredump.cx/afl/ http://lcamtuf.coredump.cx/afl/), a fuzzer which instruments programs at compile-time to help find interesting inputs faster than brute-force fuzzing. It may have indeed found a bug in TimSort, since it's more apt at exercising branches, but I think AFL is C/C++ only.
  - deleted 12y ago
    [deleted]
- vstolz 12y ago
  I'd say that QuickCheck would have a hard time coming up with a failing test case since the input needs to be rather large to trigger the bug.
- thu 12y ago
  It would be interesting to see if QC would find data easily that brake the implementations or require some tuning in the way it generates test data. And sorry, I have downvoted you by mistake when I wanted to reply.
- burntsushi 12y ago
  I am trying (with some success) to get QuickCheck used in the Rust community. Listing my projects that us QuickCheck would be cheating, so I'll link projects that aren't my own. The most impressive, by far, is this linear algebra library: https://github.com/japaric/linalg.rs/tree/master/tests https://github.com/japaric/linalg.rs/tree/master/tests --- Just pick a file at random and look for `#[quickcheck]`. :-) Here's some fancy testing for a "concurrent, lock-free, linearizable, insert-only, sorted map": https://github.com/danburkert/pawn/blob/1afe50c618a733de63b9fe62210e490c6701d1db/src/util/skip_list.rs https://github.com/danburkert/pawn/blob/1afe50c618a733de63b9... Another: https://github.com/apasel422/tree/blob/6656140c44687793e31aea473e30440b2c894140/tests/quickcheck.rs https://github.com/apasel422/tree/blob/6656140c44687793e31ae... And OK, I'll stop now, but you can see more here: https://github.com/search?q=extern+crate+quickcheck&type=Code&utf8=%E2%9C%93 https://github.com/search?q=extern+crate+quickcheck&type=Cod...
- andrewchambers 12y ago
  The use of these sorting functions is already orders of magnitude more than random testing would cover. This is a very rare failure, only affecting huge arrays, arrays so large that quickcheck would not even test it.
- Too 12y ago
  In C# there's a similar tool called Code Digger[1]. It analyzes all possible branches of a function and generates input to cover all of them, this includes not only your own "if's" but also branches inside library functions and stuff like divide by zero and dereferencing null pointers. It's really impressive and can even generate strings and arrays with data that causes a different branch to be taken. Sadly i found it to be no more than that, cool. On real life code it's not useful. Real code usually has a lot of mutable state, this tool works best with pure functions. Real code does pretty complex things like parsing xml, that takes too much time to analyze for these tools. Bugs in real code are not always exceptions or error codes returned, maybe you assigned foo.x to bar.y instead of bar.x, maybe the sort doesn't crash but your numbers came out unsorted, how would the tool know that's a fault? Real bugs happen across threads or even modules running on different machines. And the list goes on. Only if you have functions that are very pure and mostly work with simple data types, few strings and lists, it can be good to use as startng point for input to a test suite but doesn't replace it fully. [1] https://visualstudiogallery.msdn.microsoft.com/fb5badda-4ea3-4314-a723-a1975cbdabb4 https://visualstudiogallery.msdn.microsoft.com/fb5badda-4ea3...
- ngrilly 12y ago
  Here is an implementation of Timsort in Haskell that also exhibits the bug: https://github.com/timjb/haskell-timsort/commit/d9c3e1e454c7d338320f8c2aa12e882921d42828 https://github.com/timjb/haskell-timsort/commit/d9c3e1e454c7... I find interesting that this Haskell version of Timsort also exhibits the bug, despite Haskell having a type system more advanced than Python or Java. This is a reminder that type checking is not a magic bullet, and is hardly enough to prove a program correctness. Formal proofs and whole program static analysis are still necessary, with or without an advanced type system: http://www.cl.cam.ac.uk/~srk31/blog/2014/10/07/ http://www.cl.cam.ac.uk/~srk31/blog/2014/10/07/

stingraycharles 12y ago

In the Haskell community there is a tool called QuickCheck [1]: it is able to generate inputs based on preconditions, and you provide a function to verify the postconditions. I am not sure why these kind of testing methods aren't used more often in other communities, since it makes it really easy to catch corner cases; in the Haskell world, at least, using QuickCheck is somewhat pervasive. [1] https://wiki.haskell.org/Introduction_to_QuickCheck2 https://wiki.haskell.org/Introduction_to_QuickCheck2 EDIT: I have never done this before, but could anyone explain why I am being downvoted? I wasn't making the claim that this is a substitute for a formal proof, I was merely adding this information to the discussion since it seemed relevant.

im3w1l 12y ago
It wouldn't catch this bug. The algorithm works for lists of size less than 2^49.
jdimov 12y ago
There is triq[1] for Erlang and excheck[2] for Elixir. [1] https://github.com/krestenkrab/triq https://github.com/krestenkrab/triq [2] https://github.com/parroty/excheck https://github.com/parroty/excheck
Osmium 12y ago
Just FYI for anyone who's interested, but there's a Swift implementation of QuickCheck described in this book: http://www.objc.io/books/ http://www.objc.io/books/ It's very minimal, but the chapter outlines what you'd need to do to make it more complete and get it on par with the Haskell version. There are also a few versions on GitHub too.
ekimekim 12y ago
At a guess: A lack of practical ways to perform such checks without extensive extra knowledge and annotation as seen in the article. A large factor is likely that Haskell is pure by default - something that is reasonably rare in many languages (where a method likely reads (or mutates) state from instance variables or even globals).
- stingraycharles 12y ago
  I think it also has to do with Haskell's type system. Quickcheck is able to "discover" the bounds within any arbitrary type can operate, and thus makes generating random values within these bounds fairly easy.
  - lclarkmichalek 12y ago
    Eh, you still have to write instances of Arbitrary. And often those instances are not great; wayyy to many libraries are tested with Arbitrary String instances that only generate ascii, for example.
grandpa 12y ago
There's a difference, though: QuickCheck randomly tries a large-ish number of possible inputs to try and disprove a postcondition, whereas formal methods prove the postcondition for all inputs. Practically, if the number of possible inputs is huge compared to the number of failure cases, it's unlikely that QuickCheck will find it. I strongly suspect - and this would be an interesting experiment - that QuickCheck wouldn't have found this particular bug, since Timsort has been in use for years without anyone noticing it.
- TheLoneWolfling 12y ago
  What about AFL?
  - jamesfisher 12y ago
    What's AFL?
    - fpgaminer 12y ago
      American Fuzzy Lop (http://lcamtuf.coredump.cx/afl/ http://lcamtuf.coredump.cx/afl/), a fuzzer which instruments programs at compile-time to help find interesting inputs faster than brute-force fuzzing. It may have indeed found a bug in TimSort, since it's more apt at exercising branches, but I think AFL is C/C++ only.
- deleted 12y ago
  [deleted]
vstolz 12y ago
I'd say that QuickCheck would have a hard time coming up with a failing test case since the input needs to be rather large to trigger the bug.
thu 12y ago
It would be interesting to see if QC would find data easily that brake the implementations or require some tuning in the way it generates test data. And sorry, I have downvoted you by mistake when I wanted to reply.
burntsushi 12y ago
I am trying (with some success) to get QuickCheck used in the Rust community. Listing my projects that us QuickCheck would be cheating, so I'll link projects that aren't my own. The most impressive, by far, is this linear algebra library: https://github.com/japaric/linalg.rs/tree/master/tests https://github.com/japaric/linalg.rs/tree/master/tests --- Just pick a file at random and look for `#[quickcheck]`. :-) Here's some fancy testing for a "concurrent, lock-free, linearizable, insert-only, sorted map": https://github.com/danburkert/pawn/blob/1afe50c618a733de63b9fe62210e490c6701d1db/src/util/skip_list.rs https://github.com/danburkert/pawn/blob/1afe50c618a733de63b9... Another: https://github.com/apasel422/tree/blob/6656140c44687793e31aea473e30440b2c894140/tests/quickcheck.rs https://github.com/apasel422/tree/blob/6656140c44687793e31ae... And OK, I'll stop now, but you can see more here: https://github.com/search?q=extern+crate+quickcheck&type=Code&utf8=%E2%9C%93 https://github.com/search?q=extern+crate+quickcheck&type=Cod...
andrewchambers 12y ago
The use of these sorting functions is already orders of magnitude more than random testing would cover. This is a very rare failure, only affecting huge arrays, arrays so large that quickcheck would not even test it.
Too 12y ago
In C# there's a similar tool called Code Digger[1]. It analyzes all possible branches of a function and generates input to cover all of them, this includes not only your own "if's" but also branches inside library functions and stuff like divide by zero and dereferencing null pointers. It's really impressive and can even generate strings and arrays with data that causes a different branch to be taken. Sadly i found it to be no more than that, cool. On real life code it's not useful. Real code usually has a lot of mutable state, this tool works best with pure functions. Real code does pretty complex things like parsing xml, that takes too much time to analyze for these tools. Bugs in real code are not always exceptions or error codes returned, maybe you assigned foo.x to bar.y instead of bar.x, maybe the sort doesn't crash but your numbers came out unsorted, how would the tool know that's a fault? Real bugs happen across threads or even modules running on different machines. And the list goes on. Only if you have functions that are very pure and mostly work with simple data types, few strings and lists, it can be good to use as startng point for input to a test suite but doesn't replace it fully. [1] https://visualstudiogallery.msdn.microsoft.com/fb5badda-4ea3-4314-a723-a1975cbdabb4 https://visualstudiogallery.msdn.microsoft.com/fb5badda-4ea3...
ngrilly 12y ago
Here is an implementation of Timsort in Haskell that also exhibits the bug: https://github.com/timjb/haskell-timsort/commit/d9c3e1e454c7d338320f8c2aa12e882921d42828 https://github.com/timjb/haskell-timsort/commit/d9c3e1e454c7... I find interesting that this Haskell version of Timsort also exhibits the bug, despite Haskell having a type system more advanced than Python or Java. This is a reminder that type checking is not a magic bullet, and is hardly enough to prove a program correctness. Formal proofs and whole program static analysis are still necessary, with or without an advanced type system: http://www.cl.cam.ac.uk/~srk31/blog/2014/10/07/ http://www.cl.cam.ac.uk/~srk31/blog/2014/10/07/