5 ms·

Even longer. What's really wild is that they even got the rough proportion of security cost for losing it down to 5% of the numbers were seeing with today's se

Even longer. What's really wild is that they even got the rough proportion of security cost for losing it down to 5% of the numbers were seeing with today's security patches. I submitted this because I think their technique is preferred for lots of stuff distributed systems developers do with crypto primitives (as opposed to retpoline). There are lots of well-known things no one seems to know outside of Academia, like how generalized sorting is O(n) and compilers that can prove the correctness of real world code when it's written a specific way

dgoldstein0 9y ago
what's interesting to me about this paper is how many different things they had to worry about. Disable scheduling, pin to a single core, page coloring, no huge pages, disable hyperthreading, disabling frequency scaling, and lastly the lazy cleanup (I think that's all?). it's a pretty long list of kernel modifications and configuration, and I doubt these will ever be defaults.
wallacoloo 9y ago
Could you share some more information about generalized sorting in O(n)? Are you talking about algorithms like radix sort?
- KirinDave 9y ago
  I replied above: https://news.ycombinator.com/item?id=16084178 https://news.ycombinator.com/item?id=16084178
tyilo 9y ago
> generalized sorting is O(n) What do you mean by generalized sorting and how isn't this affected by the comparison sorting lower bound? Do you have a source?
- cryptonector 9y ago
  They probably mean the "postman sort", or whatever catchy name it goes by (radix sort, IIRC). That doesn't involve any comparisons between elements to be sorted. Think of how a postman sorts mail into P.O. boxes... you just algorithmically map a number to a row and column (bin), and deliver. This truly is O(N), but there's a catch: it doesn't work when you don't have bins to sort into, or when you don't know even how many bins you'll need. If you try to generalize this it becomes O(N log N).
  - KirinDave 9y ago
    Well... Actually. No. First of all, radix sort uses structural features to arrive at linear time, it doesn't incomplrtely sort the input. Secondly, I've tried to get the white paper exposed here and it generally goes over like a lead balloon but: http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein2011a.pdf http://www.diku.dk/hjemmesider/ansatte/henglein/papers/hengl... Is the technique. It's an imposing 80 page paper even dedicated educators like Edward Kmett has trouble explaining trivially, but there is a talk here by the author to help sum it up: https://www.youtube.com/watch?v=sz9ZlZIRDAg https://www.youtube.com/watch?v=sz9ZlZIRDAg We've had some of Henglein's associates here to talk about it, too. There is a Haskell implementation and it can really speed up certain types of operations. It's tricky to get the constants low in Haskell, but Kmett seems to have done a pretty good job.
    - deleted 9y ago
      [deleted]
- KirinDave 9y ago
  Please see my comment below.
naasking 9y ago
> compilers that can prove the correctness of real world code when it's written a specific way Do you have something I can read? I'm curious specifically what you mean by this.
- KirinDave 9y ago
  Agda and Idris are languages with more "real world" applications that can validate totality and offer proofs. It's pretty cool because you can essentially ad hoc extend the type system to understand all transitions valid for types, then prove then. Idris is different from Agda in that it has great introducory literature (the Idris book is just fantastic) and it also has F# style type providers that let you do things like query the AWS API with a given account's creds then extend the type system with a series of descriptive types for all valid operations for every asset. It means that you can (and I find this really surprising) assert code totality on very real world use cases like code that orchestrates containers, binary parsers, or network protocols. I spent my Christmas break studying Idris and what really delighted me most was that in many cases systems like that end up being simpler to use (even though their "Verified" constructions often involve simple inductive proofs to the compiler. You don't have to prove everything, but things that are proven are safe to use
  - naasking 9y ago
    I'm familiar with dependently typed languages, I thought you might mean something different than semi-manual theorem proving. For instance, writing your program in a particular style that could maximally take advantage of automated SMT solving in LiquidHaskell or something.

dgoldstein0 9y ago

what's interesting to me about this paper is how many different things they had to worry about. Disable scheduling, pin to a single core, page coloring, no huge pages, disable hyperthreading, disabling frequency scaling, and lastly the lazy cleanup (I think that's all?). it's a pretty long list of kernel modifications and configuration, and I doubt these will ever be defaults.

wallacoloo 9y ago

Could you share some more information about generalized sorting in O(n)? Are you talking about algorithms like radix sort?

KirinDave 9y ago
I replied above: https://news.ycombinator.com/item?id=16084178 https://news.ycombinator.com/item?id=16084178

tyilo 9y ago

> generalized sorting is O(n) What do you mean by generalized sorting and how isn't this affected by the comparison sorting lower bound? Do you have a source?

cryptonector 9y ago
They probably mean the "postman sort", or whatever catchy name it goes by (radix sort, IIRC). That doesn't involve any comparisons between elements to be sorted. Think of how a postman sorts mail into P.O. boxes... you just algorithmically map a number to a row and column (bin), and deliver. This truly is O(N), but there's a catch: it doesn't work when you don't have bins to sort into, or when you don't know even how many bins you'll need. If you try to generalize this it becomes O(N log N).
- KirinDave 9y ago
  Well... Actually. No. First of all, radix sort uses structural features to arrive at linear time, it doesn't incomplrtely sort the input. Secondly, I've tried to get the white paper exposed here and it generally goes over like a lead balloon but: http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein2011a.pdf http://www.diku.dk/hjemmesider/ansatte/henglein/papers/hengl... Is the technique. It's an imposing 80 page paper even dedicated educators like Edward Kmett has trouble explaining trivially, but there is a talk here by the author to help sum it up: https://www.youtube.com/watch?v=sz9ZlZIRDAg https://www.youtube.com/watch?v=sz9ZlZIRDAg We've had some of Henglein's associates here to talk about it, too. There is a Haskell implementation and it can really speed up certain types of operations. It's tricky to get the constants low in Haskell, but Kmett seems to have done a pretty good job.
  - deleted 9y ago
    [deleted]
KirinDave 9y ago
Please see my comment below.

naasking 9y ago

> compilers that can prove the correctness of real world code when it's written a specific way Do you have something I can read? I'm curious specifically what you mean by this.

KirinDave 9y ago
Agda and Idris are languages with more "real world" applications that can validate totality and offer proofs. It's pretty cool because you can essentially ad hoc extend the type system to understand all transitions valid for types, then prove then. Idris is different from Agda in that it has great introducory literature (the Idris book is just fantastic) and it also has F# style type providers that let you do things like query the AWS API with a given account's creds then extend the type system with a series of descriptive types for all valid operations for every asset. It means that you can (and I find this really surprising) assert code totality on very real world use cases like code that orchestrates containers, binary parsers, or network protocols. I spent my Christmas break studying Idris and what really delighted me most was that in many cases systems like that end up being simpler to use (even though their "Verified" constructions often involve simple inductive proofs to the compiler. You don't have to prove everything, but things that are proven are safe to use
- naasking 9y ago
  I'm familiar with dependently typed languages, I thought you might mean something different than semi-manual theorem proving. For instance, writing your program in a particular style that could maximally take advantage of automated SMT solving in LiquidHaskell or something.