Reading 9/28: Automatic Verification

[bcarlet]

Hi all, this is the discussion thread for next Thursday (September 28). The selected paper is Provably Correct Peephole Optimizations with Alive. Please post your comments/questions here!

[keikun555]

I wonder if there has been efforts to verify the Alive to C++ transpiler in addition to the empirical testing presented in page 9.

The code compiled by LLVM+Alive did not have any unexpected test case failures: as far as we can tell, it is free of miscompilation bugs.

[sampsyo]

I don't think so! FWIW, there may be a larger lesson here about what counts as "verified." Colloquially, people are very comfortable saying that their system is "verified" if only a part of it is actually verified, merely because it's impossible to verify the whole world.

In other words, every verified system has a TCB. It is a squishy, human task to decide how risky that TCB is. This kind of assertions from the Alive paper amount to saying "hey, maybe this TCB is not so bad and seems kinda trustworthy?" And honestly, I believe them: at least in contrast to human-written C++ for peephole optimizations, it seems much more likely that this code generator is correct.

[bcarlet]

One of the difficulties in verifying something like the Alive to C++ translation is that suddenly you need a formal specification of a nontrivial subset of C++ and the LLVM APIs. In my experience with papers on large-scale formal verification, such specifications are often large contributions in their own right. See, for instance, the formal semantics produced for "CompCert C" in the case of CompCert, or for a subset of Verilog in the case of CakeML.

[matth2k]

So would you agree that the bottleneck to large-scale formal verification is basically a semantics problem? These narrow-focused verification papers leave me wanting to better understand the gap between formal methods and the high-level applications that are in most demand.

[keikun555]

Doing the tasks in this class gave me the impression that writing compiler optimizations for a feature-rich programming language are really tedious with a plethora of edge cases. I think this paper is a right step towards towards optimization development using machines to find these edge cases for us, and even better, prove that our optimizations are correct. This makes me wonder if there are more classes of optimizations we can write general formal verifiers for.

[sampsyo]

With apologies for self-promotion, our lab has been connected lately to a similar kind of "verifiable DSL to replace plain ol programming" effort, this time for instruction selection:
https://www.cs.cornell.edu/~avh/veri-isle-preprint.pdf

[bennyrubin]

I agree. I think that may be one of the biggest lessons I've learned from this class -- trying to write and verify optimizations in assembly is incredibly tedious and error prone. As someone with one foot in verification, I see this as an extremely rich use case.

[keikun555]

I was looking up what peephole optimizations were and this wikipedia article provides many examples. They seem like a small subset of local optimization where we replace a contiguous set of instructions in a block with something computationally less expensive.

[willwng]

Rather than verifying existing transformations, how feasible would it be to brute-force new peephole optimizations? I saw that the paper referenced the program Optgen, which generates all possible optimizations but doesn't support poison values and undefined behavior. Alive also claims to take several hours to test multiplication/division heavy transformations. If we restrict our transformations to a subset of the language (no instructions that multiply/divide or can cause undefined behavior) can we still find optimizations that aren't immediately obvious to us?

[vivianyyd]

My intuition is that extending Optgen is possible, but probably not to arbitrary optimizations.
From a quick skim, it looks like Optgen uses bottom-up enumeration/observational equivalence, then checks correctness using an SMT solver.
Since Alive is able to verify optimizations that involve richer language features, it seems like one could similarly extend the correctness checking step in Optgen.
In the first enumeration step in Optgen, they synthesize interesting rules for constant folding using symbolic constants. It's not obvious to me whether we could do the same for values that are not integers.
However, synthesizing optimizations involving some limited memory operations might be possible^{[citation needed]}?
During the enumeration step, I think we could ignore undef and poison values and defer checking for them to the verification stage. So it doesn't seem unreasonable to me that Optgen could support poison values and undefined behavior.
(Sorry this is kind of off topic! Got carried away)

[sampsyo]

Totally a good question in general! Aside from peephole optimizations in particular, there is other work on synthesizing optimizations. One good recent example is Vegen, which generates vectorization pattern-based rewrites:
https://groups.csail.mit.edu/commit/papers/2021/vegen.pdf

[stephenverderame]

I think even with those restrictions, we can still find a large amount of optimizations. Optgen itself seems to restrict itself only to bitwise operators, addition, and subtraction. One interesting thing they do in the paper is to use preconditions, like Alive, before applying transformations which I think can definitely introduce a lot of non-obvious simplifications. A simple, yet, easily overlookable, (at least to me) example they gave in the paper was

(c1 & c2) == 0 => 
        (x | c1) & c2 -> x & c2

where c1 and c2 are constants

[bcarlet]

On the subject of preconditions that @stephenverderame mentioned, the Alive-Infer follow-on paper looked at the issue of automatically obtaining these preconditions. In particular, in some cases their prototype was able to find a weaker precondition than the human-generated one, which adds credibility to the argument that these tools can find optimizations that aren't obvious to humans.

[jdroob]

Couple questions:

1. Since Alive is specific to LLVM, are there similar projects that are built around intermediate representations other than LLVM's? Or is LLVM's IR so common that there isn't really much motivation for such projects?

2. Have there been any extensions to Alive that allow it to handle optimizations other than peephole optimizations (e.g. optimizations involving branches)?

[sampsyo]

FWIW, Peepmatic was an Alive-inspired peephole optimization DSL/verifier/generator for Cranelift's IR:
https://github.com/fitzgen/peepmatic

It's very fun to read about!

You might also be interested in Alive2, which has a very different flavor, but it does translation validation in general for LLVM code, including with control flow:
https://users.cs.utah.edu/~regehr/alive2-pldi21.pdf

[vivianyyd]

I'm pretty excited by the impact of this paper (and Alive2) on real production code. It's neat that this was done on such a widely used tool, yet still on a problem small enough to apply formal verification.

I like that they tried both using SMT array theory to encode memory operations, as well as replacing stores with if-then-else expressions to be more efficient. I don't think I quite understood the latter approach fully though, and what exactly an "eager Ackermannization encoding" is.

[sampsyo]

Hilariously, some research collaborators and I were just discussing this specific part of this paper (and the funky "eager Ackermannization" name) earlier today!! I also can't pretend to understand it in detail, but I think it's basically just modeling "load from address A" as "if A == B, return value previously stored to B. if A == C, return value previously stored to C." and so on.

[stephenverderame]

I think it's kind of interesting how the paper notes that many LLVM developers working on peephole optimizations frequently just leave out nsw, nuw, and exact from the target side just because of the difficulty of getting it right. The paper kind of gets the inference "for free" just by brute-forcing all attributes and seeing which ones produce valid transformations. It feels like there should be a way to do this more efficiently, although I don't currently have any particularly insightful ideas.

[sampsyo]

While you may be right that there's an easier way, I think one of the great things about solver-aided automatic verification tools is that they enable "dumb" tools to work that otherwise would be really hard to build. That "dumb" thing can use arbitrary, unsound heuristics to search for good solutions, relying on the backstop of formal verification to make sure it doesn't produce wrong answers.

[ryanwmao]

I thought this paper was a pretty interesting read, although it was a lot to digest. Compiler testing is definitely a very important part of implementing compilers, so I'm curious as to the impact that this paper has had? It seems to me that the integration of tools like Alive into compiler work could have led to more efficient development in the field.

[obhalerao]

Echoing the sentiments of some of the previous comments, I think this is a really cool paper that has the potential to improve a lot of compiler engineers' lives; writing all these compiler optimizations so far this semester has made me realize just how many edge cases have the potential to exist, and I'm sure that being able to formally verify any optimization, even if it only affects a small subset of instructions, has the potential to improve the correctness of many existing compilers out there. I also find it interesting how the authors encoded undefined behavior and logic on arrays to work well with the SMT solvers they use; these encodings certainly do not seem trivial and I'd like to learn more about how exactly they're done.

Also, since this paper came out nearly a decade ago, I'm curious as to how the use of this tool has spread over that time in compiler development. It certainly seems well-suited for its use case, so I'd appreciate learning about how this tool or others like it are used in the real world currently.

[bcarlet]

To address one part of the question, it certainly seems like this tool (or rather its successor, Alive2, which is hosted on Compiler Explorer) is still in active use by LLVM developers. Looking through the LLVM issue history for InstCombine, many of the recent issues (e.g., here or here) provide a link to an Alive2 proof. There's also this impressive list of bugs found by the tool, some of which are fairly recent.

[AliceSzzze]

Oh wow, it even found bugs in Z3...

[SanjitBasker]

I agree with others that one of the most attractive points of this system is that it can be used to prevent new bugs before they arise, in tandem with regular compiler development (section 6.2). This reminds me of the counterexample generation in the parser generator I used in CS 4120 (the parser generator outputs a sequence of tokens and a description of how the parser gets "confused," i.e. a shift-reduce or reduce-reduce conflict).

If we regard the process of formally proving something and the process of finding a counterexample as duals, then both these tools perform a process that can be boring or unintuitive for humans and replace it with a checker that is conservative (i.e. it may not finish its task in time, but it never outputs a wrong answer). It seems to me that in the long run, such a tool would be well worth the initial investment to get developers familiarized with it.

[evanmwilliams]

I'm curious about some of the problems that arise when making a tool like this. As others have mentioned, Alive is very useful. Being able to prove your peephole optimizations saves the fear of deploying an optimization that inevitably wrecks someone's program out in the world. But many of the ways the problems were framed suggested that proving optimizations created the need to solve SAT-instances, some of which are even quantified placing the problem in NP-Hard or PSPACE-Hard. The SMT solvers we have are great, but I'm curious about the applicability at scale.

Another thing that I was curious about was the notion of translating Alive back into C++. It seems like Alive syntax is meant to be reminiscent of LLVM syntax, but if it gets transpiled to C++ it seems like it'd be better making the syntax a bit more lightweight to begin with?

Anyways, definitely an interesting read. I also found it pretty funny that LLVM passes were proved incorrect with this tool - definitely tough to get compiler optimizations right, and it's especially important for what they're used for.

[sampsyo]

Scalability is indeed the core issue in automatic verification. The work usually involves either (a) finding a use case where small-scale problems/proofs suffice to accomplish something useful, and (b) playing a lot of tricks to make the encoding for the solver as efficient as possible to push out the scalability limits. This paper does quite a bit of both. The whole idea of focusing on peephole optimizations in particular is a brilliant example, IMO, of part (a): it's a case where a fairly small number of instructions are involved, but human reasoning is nonetheless very fallible.

[sampsyo]

I think the reason the syntax looks like LLVM is so that it looks like the examples it's transforming. That is, so the LHS and RHS look very similar to the LLVM IR snippets an optimization will produce/consume.

[NgaiJustin]

The formal methods tools introduced in the paper are really exciting and seem to bring a lot of promise and reassurance to compiler developers—a structured and mathematically sound approach to verifying the correctness of compiler transformations.

Also, apologies if this seems like a silly question as I have 0 background with formal verification, but I was wondering how we can be certain that the verifier itself is correct. I understand that in the context of this paper, when Alive fails to prove the correctness of a transformation, it prints a counterexample showing values for inputs and constants, as well as for each of the preceding intermediate operations. However, if these counterexamples become too complex or exceed the scale at which we can manually inspect them, it may raise concerns about the reliability of the verifier. In such cases, it might seem impractical to manually validate the correctness of the verifier, potentially leading to a paradoxical situation where we rely on an automated tool whose accuracy we cannot independently verify.

[xalbt]

I was curious about this issue as well, and it turns out there is a formally verified version of Alive called "AliveInLean". The same authors essentially rewrote a subset of Alive in the Lean theorem solver. Although it isn't as feature rich as the original Alive, it supports most of the original tool, and I inferred from the paper that remaining support could be added.

I can attest your point about the complexity of counterexamples with a personal experience. As @SanjitBasker mentioned, we used a parser generator that generates counter examples in CS 4120. During the construction of our grammar, we went through many iterations that were not LR(1). The counterexample generator was helpful in some of these iterations, but in some, the counterexamples were dozens of tokens long and entirely unhelpful. I can imagine the counterexamples generated by Alive will be even more difficult to understand, especially with undefined behavior.

[zachary-kent]

Even if the counterexample output of Alive was quite complex, I would not be particularly worried about its correctness. Specifically, these counterexamples are generated using Z3, which is quite well trusted -- Alive is not doing the heavy lifting here. IMO, bugs are most likely to appear while encoding LLVM semantics, which (beyond projects like Vellvm), are not well-formalized.

[sampsyo]

I don't know if this is what you're looking for, but there's another discussion thread at #387 (reply in thread) all about TCBs. Every verified system has a TCB; it's usually difficult to decide how trustworthy it is.

[MelindaFang-code]

The authors seems to be hiding a lot of implementation detail and they seem to be non trivial to implement. For instance, Alive would rely on using a collection of built-in predicates such as isPowerOf2(), MaskedValue, IsZero(), for dataflow analysis. I wonder if there exist a tradeoff here between simplicity vs program runtime, like RISC vs MISC.

[Enochen]

One interesting side detail brought up by the paper was compilation time. At the time of the paper, the LLVM+Alive configuration was slightly faster (7%) than LLVM 3.6 at -O3. The paper noted that this was because Alive only had implemented a fraction of the InstCombine optimizations. This, coupled with the imbalanced applicability of different optimizations makes me wonder about ways to navigate the balance between trying out all the optimizations in the world and compilation speed.

I'm not the most familiar in this area but I assume there's some level of overhead on compilation speed that grows linearishly based on number of optimizations. The way I know is provided to navigate this is simply having compiler options like -O2 and -O3 that allow you to (coarsely) turn the knobs on how optimized you want to go. However, I feel like it'd be interesting to look at more intelligent/efficient methods for applying optimizations that reduce the penalty of having a larger suite of optimizations, especially with a majority having a good chance of not being applied to any particular program.

When I worked with Haskell at an internship years ago, I remember the production build times were excruciatingly long due to GHC being absolutely massive. I'm not sure if it's the same situation mentioned in the paper where there are many optimizations that don't get applied (I'm sure many were). Nevertheless, I think it'd be super cool to look into. Does anyone know if this is an active area of research?

[sampsyo]

Certainly there is something about more optimizations being more expensive (after all, each optimization comes with a nonnegative performance cost!!). But I'm not sure LLVM vs. GHC is an example of that trend—they represent very different approaches to building compilers for very different kinds of languages.

[sampsyo]

(I don't know of any papers that examine how many optimizations were "useless." Seems like an interesting project.)

[AliceSzzze]

It goes without saying that the correctness of compilers is critical and almost always expected. As the authors remark in the paper,

the incorrectness is introduced at a level of abstraction lower than the one where software developers typically work.

Most people wouldn't even think about the possibility of a compiler bug when debugging, so this paper undoubtedly addresses some important problems. I was shocked and impressed to find that Alive managed to catch eight bugs in such a widely used compiler infrastructure. Some of them were subtle (e.g. different ranges of inputs), and others produced incorrect expressions.

While this work is promising and already impactful, its scope is somewhat limited. As others have noted,

for some transformations involving multiplication and division instructions, Alive can take several hours or longer to verify the larger bitwidths.

Moreover, (the non-experimental version of) Alive does not support branches, which are integral to many programs. I wonder if they have included control flow in Alive2.

I don't know much about SMT solvers so I didn't fully understand some parts of the paper, but hopefully I will! It was also interesting to see how the authors handled different features of the language (e.g. keeping track of allocated memory with alloca).

[sampsyo]

Alive2 is a translation validation tool, not a peephole-optimization-generating tool—but yes, it supports control flow. You can try it out yourself if you like: https://alive2.llvm.org/

[alifarahbakhsh]

This was a needed reading!

We have seen compiler optimizations as different islands, each doing its own task. Of course, we have also seen generalizations, but it still seemed more like a "big bag of algorithms", just like the field of networking - according to Scott Shenker - was more like a "big bag of protocols" before the software-defined networking paradigm. It was heartening to see that there actually are systematic ways to abstract correctness for this bag, and to talk about it formally.

Specifically, I love the abstraction of "undefined" stuff. I have been constantly struggling with this in my optimizations this semester, as there always is this tension between "what to cover" and "what to leave for the developer". Turns out that the solution for a correctness analysis was just to abstract all that away to quantification over the possible values. Of course, this cannot capture all the ambiguity, since there might be infinite cases to consider. But even the limited version manages to capture subtle bugs. I am wondering whether this approach can be augmented with model checking, through (perhaps runtime) division of the state space into a finite set.

A cute part of the paper was the difference between undefined and poisoned variables. It reminded me of the difference between immediate domination and the dominance frontier. It seems like there is a fundamental role played by this difference between the immediate and post-immediate reach of an operation in compilers.

Finally, to go back to the big bag and abstraction issue, you might have noticed that some optimizations that we have been doing have a pretty solid algebraic structure. This is actually accurate, and there is a paper by Dexter and Maria-Cristina Patron that delves into it through the lens of the famous KAT framework:

Certification of Compiler Optimizations
using Kleene Algebra with Tests

[collinzrj]

In section 3.3.3, the author mentions that "Many SMT solvers do not support the theory of arrays efficiently", so they "explore encoding memory operations without arrays". This reminds me of the experience of generating zero-knowledge proofs. Zero-Knowledge proof usually also requires us compiling a high-level language to a set of constraints. In that case, we should also encode memory access with some other techniques, this may also produce a quadratic increase in the size of constraints. It's exciting to find a connection here.
The author mentioned that they encode memory access as ite operation. I don't actually believe this can actually speed things up, since for each memory access, we need n ite operations, and n is the size of the array. I know that there is a more efficient way to encode memory accesses in zero-knowledge proof literature. [1] It would be interesting to explore whether this technique can be applied here for memory access encoding.

[1] Efficient RAM and control flow in verifiable outsourced computation

[sampsyo]

I don't actually believe this can actually speed things up, since for each memory access, we need n ite operations, and n is the size of the array.

This encoding is certainly not fast or scalable, but the point they're making in the paper is not that it's good—it's that it's better than the solver's built-in theory of arrays. Which is not surprising because solver theories are weird and complicated and sometimes seek to prove more than you need them to.

In particular, using the solver's built-in theory of arrays essentially needs to do exactly the same thing, producing $n$-way conditionals at each index for $n$-sized arrays. It's just worse at doing the same thing than this custom encoding.

[alifarahbakhsh]

Slightly related to this is memory access patterns in cryptographic applications. For instance, in some applications access to memory can be a side channel, and therefore your code should obfuscate the access, e.g., read an entire array and not a specific index. Perhaps verifying such coarse-grained accesses might be easier in the Alive framework.

[alifarahbakhsh]

In case anyone was interested:
MAGE: Nearly Zero-Cost Virtual Memory for Secure Computation

[rcplane]

I found the verification efforts in this paper interesting to compare and contrast to hardware emulation, which also strives to perform a search over function-compatible building blocks but at the hardware gate level instead of the software instruction layer, for instance when developing AMD chips capable or reasonable x86 application performance [1]. In particular the use of a fast gate level FPGA hardware emulator makes me wonder about the exploration of available chip(let) design space for runtime optimization.

[1] Hardware Emulation for Functional Verification of K5