3 ms·

I guess it depends on the perspective and interpretation of soundness. If a JIT-compiler AoT compiles your entire program but infers that your function that imp

I guess it depends on the perspective and interpretation of soundness. If a JIT-compiler AoT compiles your entire program but infers that your function that implements logic that works for every number (as you defined it using the Number interface within the rules of it's type system) will only use 32 bits integers, then it will compile code that effectively does not hold up to the property that was established. The fact that it will stop execution the moment it reaches an invalid path and correct it doesn't change that.

pvg 7y ago
It could be and that would be uninteresting. But it's not hard to come up with a (contrived, limit-casey) optimization approach that does actually make guesses about soundness. Let's say you wanted to optimize a short instruction sequence with a small domain of inputs. You could try to generate all (or at least, zillions) of similarly-sized possible instruction sequences and check them for soundness and performance. Now you're really making soundness guesses. Do real JITs actually make that sort of soundness guess (not that kind of attempt at optimization, obviously)?
- ddragon 7y ago
  A JIT compiler could detect that an instruction sequence (or function) is pure (for some range of valid inputs) and auto-memoize them for performance gains. But if you want the JIT to evolve compiled representation by profiling some fitness measurement (performance) and condition (soundness), that will most likely not happen any time soon. The JIT compiler has to balance compile time execution with runtime execution, if it wastes 5s to generate a program that runs in 2s when it could waste 1s to generate a program that would run in 4s then it would not be a good compiler at all. And above all else, JIT compilers, even the notoriously aggressive ones, still need to have some degree of predictability. If the user of the language can't predict the performance of the language, then they can't reliably improve their code performance. I'm mostly talking about production-ready stuff, such work is certainly some fun playground. The Julia JIT (one of the notoriously aggressive JITs, for good and bad), allows users to, at runtime, add new context-aware behaviors to the compiler [1], and people used it for example to experiment with auto-parallelization of code and overall manipulating the code generated by the compiler. That was basically what got me into the language. So you could probably make a library that would inject some weird risky optimization that abuses the type system. [1] https://docs.google.com/presentation/d/1IiBLVU5Pj-48vzEMnuYEr9WQy9u2oi6Yk_8F3sgGkvQ/preview#slide=id.p https://docs.google.com/presentation/d/1IiBLVU5Pj-48vzEMnuYE...
- pron 7y ago
  All the time, and BTW, I didn't say JITs sacrifice soundness but that they don't require proof of soundness. That's different as I'll show. Let me give you two common examples: virtual calls and branches. A JIT will speculatively devirtualize and inline a virtual call at a particular callsite if it has only encountered one or a small number of concrete instances, even if it can't prove that those are the only instances that can be encountered at that callsite. This is still sound because the JIT will emit a trap that will trigger if an unknown target is ever encountered, in which case it will deoptimize the compilation, go back to the interpreter and then compile again under new assumptions. Another example is branch elimination. If a JIT only ever encounters the program taking one side of a branch, it will only compile that branch (and introduce a trap), even if it can't prove that only that side will ever be taken.
  - pvg 7y ago
    Thanks! I did (eventually) figure it out, I initially misread it as something like: 1. Jettison soundness 2. ??? 3. Performance profit. Which seems like witchcraft, then again JITs are full of witchcraft. But it's also not what you wrote. I've now come to understand the two chief weapons of the JIT remain surprise, fear, ruthless efficiency and an almost fanatical devotion to the Pope.

pvg 7y ago

It could be and that would be uninteresting. But it's not hard to come up with a (contrived, limit-casey) optimization approach that does actually make guesses about soundness. Let's say you wanted to optimize a short instruction sequence with a small domain of inputs. You could try to generate all (or at least, zillions) of similarly-sized possible instruction sequences and check them for soundness and performance. Now you're really making soundness guesses. Do real JITs actually make that sort of soundness guess (not that kind of attempt at optimization, obviously)?

ddragon 7y ago
A JIT compiler could detect that an instruction sequence (or function) is pure (for some range of valid inputs) and auto-memoize them for performance gains. But if you want the JIT to evolve compiled representation by profiling some fitness measurement (performance) and condition (soundness), that will most likely not happen any time soon. The JIT compiler has to balance compile time execution with runtime execution, if it wastes 5s to generate a program that runs in 2s when it could waste 1s to generate a program that would run in 4s then it would not be a good compiler at all. And above all else, JIT compilers, even the notoriously aggressive ones, still need to have some degree of predictability. If the user of the language can't predict the performance of the language, then they can't reliably improve their code performance. I'm mostly talking about production-ready stuff, such work is certainly some fun playground. The Julia JIT (one of the notoriously aggressive JITs, for good and bad), allows users to, at runtime, add new context-aware behaviors to the compiler [1], and people used it for example to experiment with auto-parallelization of code and overall manipulating the code generated by the compiler. That was basically what got me into the language. So you could probably make a library that would inject some weird risky optimization that abuses the type system. [1] https://docs.google.com/presentation/d/1IiBLVU5Pj-48vzEMnuYEr9WQy9u2oi6Yk_8F3sgGkvQ/preview#slide=id.p https://docs.google.com/presentation/d/1IiBLVU5Pj-48vzEMnuYE...
pron 7y ago
All the time, and BTW, I didn't say JITs sacrifice soundness but that they don't require proof of soundness. That's different as I'll show. Let me give you two common examples: virtual calls and branches. A JIT will speculatively devirtualize and inline a virtual call at a particular callsite if it has only encountered one or a small number of concrete instances, even if it can't prove that those are the only instances that can be encountered at that callsite. This is still sound because the JIT will emit a trap that will trigger if an unknown target is ever encountered, in which case it will deoptimize the compilation, go back to the interpreter and then compile again under new assumptions. Another example is branch elimination. If a JIT only ever encounters the program taking one side of a branch, it will only compile that branch (and introduce a trap), even if it can't prove that only that side will ever be taken.
- pvg 7y ago
  Thanks! I did (eventually) figure it out, I initially misread it as something like: 1. Jettison soundness 2. ??? 3. Performance profit. Which seems like witchcraft, then again JITs are full of witchcraft. But it's also not what you wrote. I've now come to understand the two chief weapons of the JIT remain surprise, fear, ruthless efficiency and an almost fanatical devotion to the Pope.