Hacker News Reader

Comment by Animats | Hacker News Reader

Excellent! I've wanted compilers to optimize overflow checks and subscript checks since my proof of correctness work decades ago. This was done in the 1980s for Pascal, but the technology was forgotten. It's finally going mainstream.

The next optimization, which the parent article doesn't cover, is hoisting checks out of loops. This is a huge win for subscript checks. Most newer compilers optimize FOR loops, at least.

Having detected an error, what do you do? An exception would be nice, but few languages other than Ada handle machine level exceptions well. Aborting the whole program is drastic.

View on HN

Isn't value range inference for eliminating overflow / out-of-bounds checks, and LCM (/PRE) for hoisting checks out of loops pretty standard in any optimizing compiler nowadays?

Do you have a reference for the proof you did? I'm interested in optimising overflow checks in Ruby.

The system: [1] The Nelson-Oppen decision procedure: [2]

There's a subset of of arithmetic and logic that's completely decidable. It includes addition, subtraction, multiplication by constants, "if", the theory of arrays, a similar theory of structures, and the Boolean operators (on bools, not integers.) This is enough for most subscript and overflow checks. Complete solvers exist for this subset. If you try to prove all constraints that need run-time checks with this approach, you can eliminate maybe 80-90% of run time checks as unnecessary.

Some checks cannot be eliminated, but can be hoisted out of loops. This means making one check before entering the loop, rather than one on each iteration. FOR statements usually can be optimized in this way. That's almost a no-brainer in modern compilers. The "Go" compiler does this. Heavier machinery is needed for more complex loops.

[1] http://www.animats.com/papers/verifier/verifiermanual.pdf

[2] http://www.cs.cmu.edu/~joshuad/NelsonOppen.pdf

> The "Go" compiler does this

Really? I was under the impression the Go compiler did only simplistic optimisations, to get their wonderfully fast compile times. Do you have a source (e.g. the source)?

That was from the developers mailing list. I think the only optimization they're doing is for FOR statements, where you know the bounds on a loop variable at loop start. This is a big win for loops that iterate over an array and do something trivial, like setting the array elements to 0. Subscript check performance is mostly an inner-loop problem.

I didn't see general LICM, but I suspect they'll add it eventually on the SSA backend.

Oh, I'm curious why you pointed out Go specifically, since that sounds like fairly standard bounds check eliminations that pretty much all optimising compilers can do (compilers built on both LLVM and GCC's infrastructure), and most compilers aren't tied to specific looping constructs for it: it can work with while loops, or for loops, or whatever.

And, my impression is that bounds checks are only avoided in Go with range-based for loops (which are very similar to C++ or Rust iterators, which avoid bounds checks in probably exactly the same way), not a loop over integers with indexing.

Reply on news.ycombinator.com