[HN Gopher] Optimizers need a rethink
___________________________________________________________________
Optimizers need a rethink
Author : ingve
Score : 57 points
Date : 2024-10-23 06:10 UTC (4 days ago)
(HTM) web link (typesanitizer.com)
(TXT) w3m dump (typesanitizer.com)
| leni536 wrote:
| I think this is mostly a philosphical question, rather than
| optimizer quality.
|
| Once an optimization becomes part of the interface and it is
| guaranteed, is it really an optimization? Or did it just became
| part of the language/library/database/whatever?
|
| One example is return value optimization in C++. In C++17 the
| "optimization" became mandatory in some contexts. What really
| happened though is that the rules of temporary materialization
| changed, and in those contexts it just never happens prematurely
| by the language rules. This ceased to be an optimization and
| became a mechanism in the language.
|
| What I'm getting at is that unreliability is a defining quality
| of optimizations.
|
| Sure, there are certain optimizations that become load-bearing,
| in which case it would be better if they became part of the
| language's semantics and guarantees, therefore they ceased to be
| optimizations.
| gizmo686 wrote:
| It is still a useful distinction. Programming languages are
| complex enough to understand. It is useful to have a base of
| 'this is the simplest description of how programs will work'
| that is as simple as possible. Then, a separate set of 'and
| here is a separate description of its performance
| characteristics; nothing in this portion should be understood
| to change the defined behavior of any program".
|
| Even if that second description is stable and part of the
| guarantees you make, keeping it seperate is still incredibly
| useful from a user perspective.
|
| From an implementation perspective, there is also a useful
| distinction. Optimizations take a valid representation, and
| turn it into a different valid representation of the same type
| that shares all defined behavior. This is a fairly different
| operation than compilation, which converts between
| representations. In particular, for the compilation step, you
| typically have only one compilation function for a given pair
| of representations; and if you have multiple, you select one
| ahead of time. For optimizations, each representation has a set
| of optimization functions, and you need to decided what order
| to apply them and how many times to do so. Compilation
| functions, for their part, need to deal with every difference
| between the two representations, whereas optimization functions
| get to ignore everything except the part they care about.
| nanolith wrote:
| One area that I have been exploring is building equivalence
| proofs between high-level specifications, an implementation in C,
| and the machine code output from the compiler. I'm still very
| early in that work, but one of my hopes is to at least
| demonstrate that the output still meets the specifications, and
| that we can control things like timing (e.g. no branching on
| secret data) and cache in this output.
|
| I think that the compilation and optimization step, as a black
| box, is a disservice for highly reliable software development.
| Compiler and optimizer bugs are definitely a thing. I was bitten
| by one that injected timing attacks into certain integer
| operations by branching on the integer data in order to optimize
| 32-bit multiplications on 8-bit microcontrollers. Yeah, this
| makes perfect sense when trying to optimize fixed point
| multiplication, but it completely destroys the security of DLP or
| ecDLP based cryptography by introducing timing attacks that can
| recover the private key. Thankfully, I was fastidious about
| examining the optimized machine code output of this compiler, and
| was able to substitute hand coded assembler in its place.
| cesarb wrote:
| > One area that I have been exploring is building equivalence
| proofs between high-level specifications, an implementation in
| C, and the machine code output from the compiler.
|
| AFAIK, that's how seL4 is verified. Quoting from
| https://docs.sel4.systems/projects/sel4/frequently-asked-que...
|
| "[...] Specifically, the ARM, ARM_HYP (ARM with virtualisation
| extensions), X64, and RISCV64 versions of seL4 comprise the
| first (and still only) general-purpose OS kernel with a full
| code-level functional correctness proof, meaning a mathematical
| proof that the implementation (written in C) adheres to its
| specification. [...] On the ARM and RISCV64 platforms, there is
| a further proof that the binary code which executes on the
| hardware is a correct translation of the C code. This means
| that the compiler does not have to be trusted, and extends the
| functional correctness property to the binary. [...] Combined
| with the proofs mentioned above, these properties are
| guaranteed to be enforced not only by a model of the kernel
| (the specification) but the actual binary that executes on the
| hardware."
| nanolith wrote:
| Indeed it is. What I'm working toward is a more efficient way
| to do the same, that doesn't take the touted 30 man years of
| effort to accomplish.
|
| I'm working on a hybrid approach between SMT solving and
| constructive proofs. Model checking done with an SMT solver
| is pretty sound. I'm actually planning a book on a scalable
| technique to do this with CBMC. But, the last leg of this
| really is understanding the compiler output.
| gizmo686 wrote:
| If you haven't done so, you might want to look at some of the
| work done by the seL4 microkernel project.
|
| They start with a Haskell prototype that is translated
| programatically into a formal specification for the theorem
| prover.
|
| They then implement the same thing in C, and use a refinement
| prove to demonstrate that it matches their Haskell
| implementation.
|
| They then compile the program, and create another refinement
| proof to demonstrate that the binary code matches the C
| semantics.
| nanolith wrote:
| I'll refer you to my reply to a sibling comment. I'm hoping
| that I can build a more efficient means of doing similar work
| as with seL4, but without the 30 man year effort.
|
| They are on the right track. But, I think there have been
| some improvements since their effort that can lead to more
| streamlined equivalence proofs.
| nlewycky wrote:
| > I was bitten by one that injected timing attacks into certain
| integer operations by branching on the integer data in order to
| optimize 32-bit multiplications on 8-bit microcontrollers.
|
| FWIW, I think this should be considered a language design
| problem rather than an optimizer design problem. Black box
| optimizer behaviour is good for enabling language designs that
| have little connection to hardware behaviour, and good for
| portability including to different extensions within an ISA.
|
| C doesn't offer a way to express any timing guarantees. The
| compiler, OS, CPU designer, etc. can't even do the right thing
| if they wanted to because the necessary information isn't being
| received from the programmer.
| jcranmer wrote:
| To a large degree, constant-time programming is hampered by
| the fact that even _hardware_ is often unwilling to provide
| constant-time guarantees, let alone any guarantees that the
| compiler would care to preserve. (Although, to be honest,
| constant-time guarantees are the sort of things that most
| compiler writers prefer to explicitly not guarantee in any
| circumstances whatsoever).
| bluGill wrote:
| 8 bit cpus offer constant time. 16 bit was starting to get
| into the issues where you cannot off it.
| nanolith wrote:
| Few languages provide such guarantees. But, there really was
| no way with this particular compiler to pass a hint to
| generate constant time code.
|
| Black box designs work until the knob or dial you need to
| control it isn't there. I would have taken a pragma, a
| command-line option to the compiler, or even a language
| extension.
|
| This is one example of many as to why I think that user-
| guided code generation should be an option of a modern tool
| suite. If I build formal specifications indicating the sort
| of behavior I expect, I should be able to link these
| specifications to the output. Ultimately, this will come down
| to engineering, and possibly, overriding or modifying the
| optimizer itself. An extensible design that makes it possible
| to do this would significantly improve my work. Barring that,
| I have to write assembler by hand to work around bad
| assumptions made by the optimizer.
| sebmellen wrote:
| I like that the author included their intended audience up front.
| Definitely not me, but it helped me read the article with a
| different perspective.
| keybored wrote:
| The standard optimization user case story is absurd.
|
| 1. You're not gonna get any guarantees that the optimization will
| happen. That makes it High Level. Just write code. We won't force
| you to pollute your code with ugly annotations or pragmas.
|
| 2. In turn: check the assembly or whatever the concrete thing
| that reveals that the optimization you wished for in your head
| actually went through
|
| There's some kind of abstraction violation in the above
| somewhere.
| jiggawatts wrote:
| I have the same experience with database query planners. The
| promise is that you just write your business logic in SQL and
| the planner takes care of the rest. In practice you spend weeks
| staring at execution plans.
| dspillett wrote:
| A key difference between many compilers and DB query
| planners, is that a compiler can spend more time over its
| optimisations because it is run dev-side and the benefits
| (and none of the time taken) are felt by the users. A query
| planner needs to be more conservative with its resource use.
|
| This is not true of JIT compilers, of course, which have
| similar constraints to DB query planners. In these cases the
| goal is to do a good job pretty quickly, rather than an
| excellent job in a reasonable time.
| glitchc wrote:
| Agreed. You put your finger directly on something that's always
| bugged me about optimistic code optimization strategies. The
| code I write is supposed to have deterministic behaviour. If
| the determinism changes, it should be because of a change I
| made, not a flag in the compiler. The behaviour is completely
| opaque and uncorrelatable, makes it very hard to figure out if
| a given change will lead to better or worse performance.
|
| "Abstraction violation" is a good way to put it.
| rocqua wrote:
| The excuse for this is that performance is not considered
| part of the behavior of the program. So it doesn't matter to
| the question of whether your program is deterministic.
| bluGill wrote:
| These days you don't know what cpu you run on so you can't
| make performance guarentees anyway. Even in embedded we
| have been burn with the only cpu going out of production
| enough to not depend on it anymore in most cases.
| pizlonator wrote:
| Compiler optimizers are designed from a "win in the average"
| mindset - so whether a particular optimization succeeds or not is
| really not something the user ought to rely on. If you're relying
| on it then you're playing with fire. (I say that as someone who
| has played with this particular kind of fire. Sometimes I'm ok,
| other times I get burned.)
|
| A great example of when winning in the average works is register
| allocation. It's fine there because the cost of any particular
| variable getting spilled is so low. So, all that matters is that
| most variables are in registers most of the time. If spill
| heuristics change for the better, it usually means some of your
| variables that previously got spilled now are in registers while
| others that were in registers are now spilled - and the compiler
| writer declares victory if this is a speedup in some overall
| average of large benchmarks. Similar thinking plays out in stuff
| like common subexpression elimination or basically any strength
| reduction. (In fact, most of those optimizations have the
| peculiar property that you'll always be able to craft a program
| that shows the optimization to be a bad idea; we do them anyway
| because on average they are a speedup.)
|
| In my view, if a compiler optimization is so critical that users
| rely on it reliably "hitting" then what you really want is for
| that optimization to be something guaranteed by the language
| using syntax or types. The way tail calls work in functional
| languages comes to mind. Also, the way value types work in C#,
| Rust, C++, etc - you're guaranteed that passing them around won't
| call into the allocator. Basically, relying on the compiler to
| deliver an optimization whose speedup from hitting is enormous
| (like order of magnitude, as in the escape analysis to remove GC
| allocations case) and whose probability of hitting is not 100% is
| sort of a language design bug.
|
| This is sort of what the article is saying, I guess. But for
| example on the issue of the optimizer definitely removing a GC
| allocation: the best design there is for the GC'd language to
| have a notion of value types that don't involve allocation at
| all. C# has that, Java doesn't.
| pjmlp wrote:
| Java doesn't have it yet, but they are making progress,
|
| https://jdk.java.net/valhalla/
|
| Yes, it was a bummer that Java didn't take up on the ideas of
| Cedar, Oberon linage, Modula-3, Eiffel,... even though some are
| quoted as its influences.
|
| Still I am confident that it might be getting value types,
| before C++ reflection, networking, senders/receivers, or safety
| gets sorted out. Or even that we can finally write portable C++
| code using C++20 modules.
| pizlonator wrote:
| That is really cool!
|
| It's a dang hard feature to retrofit into the way the JVM
| works. I wish those folks the best of luck.
| pjmlp wrote:
| Yes, that is the biggest engineering effort of the whole
| thing, how to add the value types concept into the JVM,
| without breaking the ecosystem.
|
| JARs and modules that work on the JVM before value types
| introduction should keep running, and how can new code
| interoperate with such jars.
| dzaima wrote:
| Unfortunately, it doesn't look like there's much of a
| guarantee that value objects wouldn't result in heap
| allocations. https://openjdk.org/jeps/401 even contains:
|
| > So while many small value classes can be flattened, classes
| that declare, say, 2 int fields or a double field, might have
| to be encoded as ordinary heap objects.
|
| There's a further comment about potential of opting out of
| atomicity guarantees to not have that problem, but then there
| are more problems - looks like pre-JIT would still allocate,
| and who knows how consistent would JIT be about
| scalarization. IIRC there was also some mention somewhere
| about just forcing large enough value objects to always be
| heap allocations.
| crabmusket wrote:
| > In my view, if a compiler optimization is so critical that
| users rely on it reliably "hitting" then what you really want
| is for that optimization to be something guaranteed by the
| language using syntax or types. The way tail calls work in
| functional languages comes to mind.
|
| Automatic vectorisation is another big one. It feels to me like
| vectorisation is less reliable / more complex than TCO? But on
| the other hand the downside is a linear slowdown, not "your
| program blows the stack and crashes".
| pizlonator wrote:
| If you're talking about autovectorization in C++ then you
| have the option of using intrinsics to get real vector code.
| So I think that's fine because you have a way to tell the
| compiler, "I really want simd".
| dzaima wrote:
| With clang you can add "#pragma clang loop
| vectorize(assume_safety)" to a loop to reduce the burden of
| proof of vectorizability and to do it if at all possible,
| giving a warning when it fails to. gcc has "#pragma GCC
| ivdep" to reduce dependency analysis, but it's not as
| powerful as clang's pragma.
| jonstewart wrote:
| At least databases have Explain. I'd love to get feedback from
| clang or gcc about why particular optimizations were not applied.
| einpoklum wrote:
| Explain doesn't give you that information in many (most?)
| DBMSes. It's a bit like seeing the compiler IR code of your
| program. It lets you understand some things, while others
| remain a mystery.
| gpm wrote:
| Arguing against query planning by pointing at a quote about
| databases is wild. Automatic query planning is ubiquitous and
| hugely succesfull in databases.
| skybrian wrote:
| > The optimizer's behavior is in some contexts load-bearing and
| has little margin for error (e.g. missing an optimization).
|
| Well, sure, sometimes, to an extent. But if it's load-bearing,
| maybe that's a bug? You might have written non-portable code that
| won't last, because it depends on an implementation detail that
| isn't standardized.
|
| There are widespread applications where performance isn't
| critical. For example, any time you do a network request. Web
| pages shouldn't break because the network is slow today, if you
| can possibly avoid it.
|
| The web provides no performance guarantees, but it tries pretty
| hard to provide _compatibility_ guarantees. Your code should,
| usually, work on new browser versions and on devices that haven
| 't been released yet. New browsers will have different JIT
| compilers with different performance cliffs. And yet, there are
| websites written many years ago that still work.
|
| When standardizing things, we need to be precise about what's
| standardized and what isn't, or protocols "rust shut" and can't
| be changed without breaking lots of stuff. _Not_ standardizing
| performance is often a win. (With some exceptions like video game
| consoles where the hardware is standardized.)
|
| Hyrum's law suggests that all compiler optimizations will
| eventually be load-bearing for someone, but we should usually try
| to avoid it. To make sure that the code is robust, perhaps
| performance should vary. Maybe it would be useful to have
| something like a chaos monkey for programs, where optimizations
| vary based on a random seed?
| f33d5173 wrote:
| the optimizer should be a magic black box. As soon as you start
| demanding a particular optimization, it shouldn't be an
| optimization anymore. In C you have inline assembly and
| intrinsics and pragmas and macros and so on. If you want the
| compiler to compile your code a particular way you should be
| using these, not trying to wrangle the optimizer to invoke a
| particular optimization.
| dzaima wrote:
| [delayed]
| QuadmasterXLII wrote:
| Frankly, the problem is that (generally, across languages various
| compiler hints) @inline sometimes fails to inline. At this point
| I've given up on ever having an @inline that reliably inlines,
| and I would very happily settle for an @assert_inline that
| doesn't change the generated assembly at all but reliably crashes
| out if the function isn't inline.
|
| Julia is by far the worst language about this. It would be vastly
| more usable with the addition of @assert_type_stable,
| @assert_doesn't_allocate, and @assert_doesn't_error macros.
___________________________________________________________________
(page generated 2024-10-27 23:00 UTC)