[RFC] Provide intrinsics for speculative loads

LLVM Project
36

Here’s another fun example. Assume the undef/poison-generating semantics of speculative loads. Consider this program (in pseudocode)

# Assume two noalias pointers %x and %y such that
# ptrtoaddr(%y) == ptrtoaddr(%x)+1. All memory is 0.
%b = freeze i1 poison
%v = llvm.speculative.load.i16(%x)
if %b {
  store i16 1, ptr %y
} else {
  llvm.assume(freeze %v == freeze %v) # basically "assume there is no undef/poison"
}

In this program, every choice for %b is fine; the speculative load can decide to load the 2nd byte or not depending on the value of %b.

But if we reorder the two operations, things get a bit odd:

%v = llvm.speculative.load.i16(%x)
%b = freeze i1 poison
if %b {
  store i16 1, ptr %y
} else {
  llvm.assume(freeze %v == freeze %v)
}

This program has UB! freeze always has a way of causing UB, no matter the value of %v:

  • if %v is all-0, then the speculative load was a proper load of both bytes, so we can set %b to 1 and cause a noalias violation
  • if %v contains poison, then we can set %b to 0 and make the assume fail.

(I am here assuming the usual reasoning principles for how UB interacts with demonic choice such as freeze. For instance, if the program does %y = freeze i8 poison followed by an assume (%y != 42), the compiler is allowed to choose whatever value it finds most convenient for %y, including 42. This is also true if we replace 42 by %x, as long as %x is already in scope when the freeze happens.)

So, under these semantics, reordering freeze down across speculative loads is illegal. This is the typical problem with angelic choice.

Yeah we’d need an entire little DSL expressing this intent, or a short list of patterns we can hard-code. All not very appealing.

I think it just sweeps the problem under the rug. :confused:

To adjust the above example for these semantics, we add explicit freeze around the load (to make it clear that there is a demonic choice happening), and we have to replace the else branch by assume(%v == 0). Then the first program is still UB-free. The 2nd program becomes:

%v = freeze llvm.speculative.load.i16(%x)
%b = freeze i1 poison
if %b {
  store i16 1, ptr %y
} else {
  llvm.assume(%v == 0)
}

There are two demonic choices here, both of which are controlled by the compiler. We can prove this program has UB with a case distinction just after the angelic choice that determines whether we load the 2nd byte or not (or alternatively we look at the noalias state tracking to see if a load through %x has been recorded for the 2nd byte).

  • If we do/did load the 2nd byte, the first freeze is a NOP, that’s outside our control. But we can make the 2nd freeze return 1, leading to a noalias conflict.
  • If we do/did not load the 2nd byte, we can make the first freeze pick 0xFF for the poison byte, and then we can make %b be 0. Now the assume fails.

It may seem like cheating that the demon making the choices for freeze can access abstract/hidden state like whatever is tracking noalias conflicts, but that’s how demonic choice works. This is why the compiler is allowed to plug in any value for freeze poison without justifying where that value comes from. The demon is not confined to what can be observed inside the program, and the same goes for the angel that makes the angelic choices. I hope one day we’ll have a theory of demonic and angelic choice that somehow limits how those choices can be made, but we don’t have such a theory now, so we have no way of saying whether what LLVM does and will do with freeze is compatible with speculative loads.