5 ms·

The hardest part of optimizations like this is verifying that they are correct. We don’t have a reliable general purpose was of verifying if any code transform

The hardest part of optimizations like this is verifying that they are correct. We don’t have a reliable general purpose was of verifying if any code transformation is correct. LLMs definitely can’t do this (they will lie and say that something is correct even if it isn’t).

viraptor 1y ago
But we do! For llvm there's https://github.com/AliveToolkit/alive2 https://github.com/AliveToolkit/alive2 There are papers like https://people.cs.rutgers.edu/~sn349/papers/cgo19-casmverify-preprint.pdf https://people.cs.rutgers.edu/~sn349/papers/cgo19-casmverify... There's https://github.com/google/souper https://github.com/google/souper There's https://cr.yp.to/papers/symexemu-20250505.pdf https://cr.yp.to/papers/symexemu-20250505.pdf And probably other things I'm not aware of. If you're limiting the scope to a few blocks at a time, symbolic execution will do fine.
- pizlonator 1y ago
  > limiting the scope to a few blocks Yeah so like that doesn’t scale. The interesting optimizations involve reasoning across thousands of blocks And my point is there is no reliable general purpose solution here. „Only works for a few blocks at a time” is not reliable. It’s not general purpose
  - viraptor 1y ago
    No optimisation currently done in production compilers (that I know of) work on more than a few blocks. I haven't seen anyone claim they're not general purpose or don't scale yet, or are not reliable. Meanwhile the patch we're discussing is 2 functions, 3 blocks each. So in this context we're not talking about anything crazy.
    - pizlonator 1y ago
      Examples of optimization passes in llvm that reason across arbitrary numbers of blocks: - SROA - GVN - regalloc And those are just the heaviest hitters. In fact most optimization passes are capable of performing changes that impact many blocks at once.
      - viraptor 1y ago
        Eh, kinda? I mean regalloc is not an optimisation pass. And SROA/GVM go through whole functions, but they don't really optimise across blocks. They do local changes only with information from previous blocks available. I meant that I don't know of anything that makes modifications across multiple blocks as one complex change. Even licm pokes one thing at a time from one block to a different one. There's no complex "let's replace this kind of cross-block pattern with a different equivalent code that changes multiple blocks at the same time".
        pizlonator 1y ago
        SROA absolutely does a coordinated modification across an arbitrary number of blocks whenever it kills an alloca. GVN has cases where it’ll also make a coordinated change across multiple blocks And those are just two passes. I’m not mentioning the many other passes that have this property just for the sake of brevity.

viraptor 1y ago

But we do! For llvm there's https://github.com/AliveToolkit/alive2 https://github.com/AliveToolkit/alive2 There are papers like https://people.cs.rutgers.edu/~sn349/papers/cgo19-casmverify-preprint.pdf https://people.cs.rutgers.edu/~sn349/papers/cgo19-casmverify... There's https://github.com/google/souper https://github.com/google/souper There's https://cr.yp.to/papers/symexemu-20250505.pdf https://cr.yp.to/papers/symexemu-20250505.pdf And probably other things I'm not aware of. If you're limiting the scope to a few blocks at a time, symbolic execution will do fine.

pizlonator 1y ago
> limiting the scope to a few blocks Yeah so like that doesn’t scale. The interesting optimizations involve reasoning across thousands of blocks And my point is there is no reliable general purpose solution here. „Only works for a few blocks at a time” is not reliable. It’s not general purpose
- viraptor 1y ago
  No optimisation currently done in production compilers (that I know of) work on more than a few blocks. I haven't seen anyone claim they're not general purpose or don't scale yet, or are not reliable. Meanwhile the patch we're discussing is 2 functions, 3 blocks each. So in this context we're not talking about anything crazy.
  - pizlonator 1y ago
    Examples of optimization passes in llvm that reason across arbitrary numbers of blocks: - SROA - GVN - regalloc And those are just the heaviest hitters. In fact most optimization passes are capable of performing changes that impact many blocks at once.
    - viraptor 1y ago
      Eh, kinda? I mean regalloc is not an optimisation pass. And SROA/GVM go through whole functions, but they don't really optimise across blocks. They do local changes only with information from previous blocks available. I meant that I don't know of anything that makes modifications across multiple blocks as one complex change. Even licm pokes one thing at a time from one block to a different one. There's no complex "let's replace this kind of cross-block pattern with a different equivalent code that changes multiple blocks at the same time".
      - pizlonator 1y ago
        SROA absolutely does a coordinated modification across an arbitrary number of blocks whenever it kills an alloca. GVN has cases where it’ll also make a coordinated change across multiple blocks And those are just two passes. I’m not mentioning the many other passes that have this property just for the sake of brevity.