7 ms·

Liquid Types enabled a 6x speed up in high-performance parsing of UDP packets, according to "Scrap your Bounds Checks with Liquid Haskell" of Gabriella Gonzalez

Liquid Types enabled a 6x speed up in high-performance parsing of UDP packets, according to "Scrap your Bounds Checks with Liquid Haskell" of Gabriella Gonzalez [1]. With Liquid Haskell, the bound checks are moved from runtime to compile time, semi-automatically handled by SMT-solvers. Static types help programmers to write correct programs faster, and the programs also run faster. As an aside, speeding up programs with static analysis (constrained dynamism) are also present in Mojo (a variant of Python) or Swift [2]. [1]: https://github.com/Gabriella439/slides/blob/main/liquidhaskell/slides.md https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell" [2]: https://github.com/modularml/mojo/discussions/466 https://github.com/modularml/mojo/discussions/466 "Mojo and Dynamism"

CyberDildonics 3y ago
This seems to be a complication to haskell to fix a performance problem that is only in haskell.
- andyferris 3y ago
  I don't think that's fair. Automated bounds checking exists in many languages (and most modern high-level languages). In Rust you might be incentivised to use unsafe blocks for array access in performance sensitive code. Julia has its `@inbounds` annotation. Some languages might not have an escape hatch at all. Automatically removing bounds checking where safe seems like a good goal, but in all but the most trivial cases its quite complex for the compiler to decide what's safe.
  - capitalsigma 3y ago
    It seems a little disingenuous to call something written in an obscure Haskell dialect a "high performance UDP packet parser"
    - maxbond 3y ago
      Why? Looks like they're doing realtime network monitoring for security purposes. Sounds like a high performance application to me. Haskell has a reputation for being slow, but the proof is in the pudding - and what's being asserted is that a stronger type system enables better optimization.
    - epgui 3y ago
      [flagged]
    - cdogl 3y ago
      Interesting - I didn't realise the performance of a system was measured in how "obscure" the source language is. (edit: I am Australian - this is sarcasm.)
      - team_dale 3y ago
        I’m also Australian and can confirm this was sarcasm
  - CyberDildonics 3y ago
    I think it's more than fair. C++ doesn't have this problem at all, bounds checks are in the std library in debug mode only. Rust and Julia make it very easy to take the bounds checks out. They don't need 'liquid types' or any extra complexity then a single keyword and even that is a little quirky. Also if you are accessing a data structure out of bounds, that's a show stopping bug that shouldn't ever happen. That should be something that is prevented ahead of time, not recovered from. Tanking a program's performance to catch bugs in released programs is a bold strategy to begin with.
    - one-punch 3y ago
      > C++ doesn't have this problem at all, bounds checks are in the std library in debug mode only. Rust and Julia make it very easy to take the bounds checks out. Haskell can do that too, with unsafeTake and unsafeDrop [1], you can opt-out of runtime bounds checks as easily as C++, Rust, and Julia. But opting-out of machine-checked guarantees is unsafe, and Haskell can do better. What's more is that Liquid Haskell can move such runtime bounds checks to compile time, made ergonomic with SMT solvers. This way, you get machine-checked guarantees (so programmers can write correct programs faster) with no runtime overhead (the programs also run faster). > Also if you are accessing a data structure out of bounds, that's a show stopping bug that shouldn't ever happen. That should be something that is prevented ahead of time, not recovered from. Yes, that's the whole point of static analysis, to move runtime checks to compile time, made ergonomic with Liquid Types. Note that this compile time verification is much stronger than testing at development time, which is what C++, Rust, and Julia offer without Liquid Types. > That should be something that is prevented ahead of time, not recovered from. Gabriella Gonzalez agrees with you, and calls this idea of "Prefer pushing fixes upstream over pushing problems downstream" as "The golden rule of programming", at the 1st slide in her talk [2]. Her talk shows you how such machine-checked verification is possible with Liquid Haskell, which is not possible in C++, Rust, and Julia without Liquid Types. [1]: https://github.com/Gabriella439/slides/blob/main/liquidhaskell/slides.md#documented-preconditions https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Documented preconditions - Scrap your Bounds Checks with Liquid Haskell" [2]: https://github.com/Gabriella439/slides/blob/main/liquidhaskell/slides.md https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"
hyperhello 3y ago
Maybe naive question, but what if a UCP packet comes in that doesn’t meet the requirements of the parser? Undefined behavior?
- marcosdumay 3y ago
  The type system removes checks that are redundant or unnecessary given the rest of the code. It doesn't assume things about external data.
  - moomin 3y ago
    Yeah, anything you assert has to be proved at runtime. Liquid Haskell just a) checks your assertions are consistent with the type returned and b) avoids you having to check again. You could theoretically remove all the unnecessary checks by hand, but it’s tricky.
anon-3988 3y ago
I assume Liquid Types can greatly increased performance in C programs where pointer checks are littered everywhere.

CyberDildonics 3y ago

This seems to be a complication to haskell to fix a performance problem that is only in haskell.

andyferris 3y ago
I don't think that's fair. Automated bounds checking exists in many languages (and most modern high-level languages). In Rust you might be incentivised to use unsafe blocks for array access in performance sensitive code. Julia has its `@inbounds` annotation. Some languages might not have an escape hatch at all. Automatically removing bounds checking where safe seems like a good goal, but in all but the most trivial cases its quite complex for the compiler to decide what's safe.
- capitalsigma 3y ago
  It seems a little disingenuous to call something written in an obscure Haskell dialect a "high performance UDP packet parser"
  - maxbond 3y ago
    Why? Looks like they're doing realtime network monitoring for security purposes. Sounds like a high performance application to me. Haskell has a reputation for being slow, but the proof is in the pudding - and what's being asserted is that a stronger type system enables better optimization.
  - epgui 3y ago
    [flagged]
  - cdogl 3y ago
    Interesting - I didn't realise the performance of a system was measured in how "obscure" the source language is. (edit: I am Australian - this is sarcasm.)
    - team_dale 3y ago
      I’m also Australian and can confirm this was sarcasm
- CyberDildonics 3y ago
  I think it's more than fair. C++ doesn't have this problem at all, bounds checks are in the std library in debug mode only. Rust and Julia make it very easy to take the bounds checks out. They don't need 'liquid types' or any extra complexity then a single keyword and even that is a little quirky. Also if you are accessing a data structure out of bounds, that's a show stopping bug that shouldn't ever happen. That should be something that is prevented ahead of time, not recovered from. Tanking a program's performance to catch bugs in released programs is a bold strategy to begin with.
  - one-punch 3y ago
    > C++ doesn't have this problem at all, bounds checks are in the std library in debug mode only. Rust and Julia make it very easy to take the bounds checks out. Haskell can do that too, with unsafeTake and unsafeDrop [1], you can opt-out of runtime bounds checks as easily as C++, Rust, and Julia. But opting-out of machine-checked guarantees is unsafe, and Haskell can do better. What's more is that Liquid Haskell can move such runtime bounds checks to compile time, made ergonomic with SMT solvers. This way, you get machine-checked guarantees (so programmers can write correct programs faster) with no runtime overhead (the programs also run faster). > Also if you are accessing a data structure out of bounds, that's a show stopping bug that shouldn't ever happen. That should be something that is prevented ahead of time, not recovered from. Yes, that's the whole point of static analysis, to move runtime checks to compile time, made ergonomic with Liquid Types. Note that this compile time verification is much stronger than testing at development time, which is what C++, Rust, and Julia offer without Liquid Types. > That should be something that is prevented ahead of time, not recovered from. Gabriella Gonzalez agrees with you, and calls this idea of "Prefer pushing fixes upstream over pushing problems downstream" as "The golden rule of programming", at the 1st slide in her talk [2]. Her talk shows you how such machine-checked verification is possible with Liquid Haskell, which is not possible in C++, Rust, and Julia without Liquid Types. [1]: https://github.com/Gabriella439/slides/blob/main/liquidhaskell/slides.md#documented-preconditions https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Documented preconditions - Scrap your Bounds Checks with Liquid Haskell" [2]: https://github.com/Gabriella439/slides/blob/main/liquidhaskell/slides.md https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"

hyperhello 3y ago

Maybe naive question, but what if a UCP packet comes in that doesn’t meet the requirements of the parser? Undefined behavior?

marcosdumay 3y ago
The type system removes checks that are redundant or unnecessary given the rest of the code. It doesn't assume things about external data.
- moomin 3y ago
  Yeah, anything you assert has to be proved at runtime. Liquid Haskell just a) checks your assertions are consistent with the type returned and b) avoids you having to check again. You could theoretically remove all the unnecessary checks by hand, but it’s tricky.

anon-3988 3y ago

I assume Liquid Types can greatly increased performance in C programs where pointer checks are littered everywhere.