[llvm] [DA] Introduce domain for monotonicity (PR #176367)

Tue Jan 20 08:40:40 PST 2026

kasuga-fj wrote:

@sjoerdmeijer For now, I have written down my current understanding. Please let me know if you have any questions or suggestions.

---

# Problem

I will start with an example that illustrates the problem.

```llvm
; Example 1
;
; for (i = 0; i < (1ULL << 60); i++) {
;   A[i] = 0;
;
;   offset = 32*i + (1ULL << 62);
;
;   // This condition is to avoid violating the limitation of the size of an allocated object
;   if (offset < (1ULL << 63))
;     A[offset] = 1;
; }
;
define void @f(ptr %A) {
entry:
  %tc = shl i64 1, 60
  %const.1 = shl i64 1, 62
  br label %loop.header

loop.header:
  %i = phi i64 [ 0, %entry ], [ %i.next, %loop.latch ]
  %idx.0 = getelementptr inbounds i8, ptr %A, i64 %i
  store i8 0, ptr %idx.0
  %offset.tmp = mul i64 %i, 32
  %offset = add i64 %offset.tmp, %const.1
  %if.cond = icmp sge i64 %offset, 0
  br i1 %if.cond, label %if.then, label %loop.latch

if.then:
  %idx.1 = getelementptr inbounds i8, ptr %A, i64 %offset
  store i8 1, ptr %idx.1
  br label %loop.latch

loop.latch:
  %i.next = add nuw nsw i64 %i, 1
  %exit.cond = icmp eq i64 %i.next, %tc
  br i1 %exit.cond, label %exit, label %loop.header

exit:
  ret void
}
```

Currently DA reports that there is no dependency between the two stores `A[i] = 0` and `A[offset] = 1` ([godbolt](https://godbolt.org/z/bGbe8ba6s)), which is incorrect. Actually, they can access the same memory location. Here are some examples:

|| `i = 0` | `i = 2^59 - 2^57` | `i = 2^59 - 2^57 + 2^55 - 1` | `i = 2^60 - 32` |
|-|-|-|-|-|
| `A[i]`| `A[0]`||| `A[2^60 - 32]`|
| `A[32*i + 2^62]` || `A[0]`| `A[2^60 - 32]`||

The root cause of the problem is that DA doesn't take addrec overflows into account (in other words, it assumes *monotonicity* for addrecs without any checks). As a result, DA considers that the values at the first and last iteration of an addrec correspond to the its minimum or maximum value, respectively, which leads to missing some possible dependencies.

# Challenges (?)

If it were non-nested loops, the problem would be easier: just checking the nowrap property of addrecs would be sufficient. One might think that recursively checking the nowrap property of addrecs would work fine, but it may not sufficient. For example, consider the following code:

```llvm
; Example 2
;
; for (i = 0; i < INT64_MAX; i++)
;   if (i < 1000)
;     for (j = 0; j < INT64_MAX - 1000; j++)
;       A[i + j] = 0;
;
define void @g(ptr %A) {
entry:
  br label %loop.i.header

loop.i.header:
  %i = phi i64 [ 0, %entry ], [ %i.next, %loop.i.latch ]
  br label %loop.j.pr

loop.j.pr:
  %guard = icmp slt i64 %i, 1000
  br i1 %guard, label %loop.j, label %loop.i.latch

loop.j:
  %j = phi i64 [ 0, %loop.j.pr ], [ %j.next, %loop.j ]
  %offset = add nuw nsw i64 %i, %j
  %gep = getelementptr inbounds i8, ptr %A, i64 %offset
  store i8 0, ptr %gep
  %j.next = add i64 %j, 1
  %ec.j = icmp eq i64 %j.next, 9223372036854774808 ; 2^63 - 1000
  br i1 %ec.j, label %loop.i.latch, label %loop.j

loop.i.latch:
  %i.next = add i64 %i, 1
  %ec.i = icmp eq i64 %i.next, 9223372036854775807 ; 2^63 - 1
  br i1 %ec.i, label %exit, label %loop.i.header

exit:
  ret void
}
```

As I tested ([godbolt](https://godbolt.org/z/jcbK91nTT)), SCEV yielded `{{0,+,1}<nuw><nsw><%loop.i.header>,+,1}<nuw><nsw><%loop.j>` for `%offset`. However, evaluating this addrec at the last iteration of the i-loop can overflow in a signed sense. Also, as a matter of fact, DA includes logic that effectively evaluates addrecs at the last iteration of non-innermost loops (e.g., the Benerjee MIV test).

# Monotonicity

As a solution to the problem, I introduced the concept of *monotonicity* for addrecs in #162280. That said, I don't have much to say about monotonicity here, since the functionalities added in #162280 are quite simple. In short, I added:

- A definition of monotonicity for addrecs.
    - Regarding an addrec as a function $F(i_1, ..., i_n)$ where $i_k$ is the iteration number of the k-th loop, for example, "monotonically increasing w.r.t. k-th loop" means that $F(..., i_k, ...) < F(..., i_k + 1, ...)$ holds for any values of other iteration numbers.
- A simple monotonicity checker, which recursively checks nowrap properties (currently only `nsw`) of addrecs.
    - So, yes, it's not sufficient. But it's a first step.

## Why Monotonicity / Why Not "No Overflow"?

I like the term monotonicity because I feel it's intuitive and clarifies the assumptions on which DA is based. However, it seems that others don't feel the same way.
The choice of the term monotonicity is also motivated by potential future extensions (see https://github.com/llvm/llvm-project/issues/168823#issuecomment-3612636989 for more details). That said, it's true that the current implementation is almost (or even completely) equivalent to "no overflow" or "affine".

Still, I don't think "no overflow" is a good term, because it's unclear which arithmetic operation it refers to. For example, in the addrec `{c,+,a}<nsw>`, it means that all additions in `((c + a) + a) + ...` (n times) don't overflow in a signed sense, but `a * n` may overflow.

## What Does This PR (#176367) Do?

It may be slightly off-topic, but I would like to mention the motivation of #176367 here. As shown in Example 2, simple recursive checking of nowrap properties may not be sufficient. However, it's not straightforward to detect loop-guards and handle them properly. In addition, there are several dependence tests that don't use backedge-taken counts of loops. For such tests, it's not necessary to consider loop-guards. Therefore, #176367 introduces a concept of a *monotonicity domain*. I'm not sure whether the naming is appropriate, but it adds two domains:

- Entire: The whole iteration space, i.e., `[0, BTC_1] x ... x [0, BTC_n]` where `BTC_k` is the exact backedge-taken count of the k-th loop.
- Effective: Certain superset of the space where the addrec is actually executed. Any superset is acceptable, but it must be consective.

## What Does Monotonicity Checker Ultimately Do?

At the moment, it simply recursively traverses an addrec and checks for the presence of `nsw` flags. Since there seem to be some misunderstandings, I would like to clarify that for non-nested addrecs (i.e., in the cases of ZIV, SIV, and RDIV), **the monotonicity check for an addrec `AR` is almost equivalent to `AR->hasNoSignedWrap()`**. So, if we follow the YAGNI principle, the concept of monotonicity may be overkill for now.

# An Alternative

This is one of the reasons why #162281 became too long, but there are two distinct topics discussed there:

- The choice of the term monotonicity.
- The necessity of introducing the concept of domains for monotonicity

As for the former, I have explained my intention above. Here, I will therefore focus on the latter. 

## Problem

I will explain the problem using the Strong SIV test as an example. The Strong SIV test attempts to disprove independence between two addrecs `{c0,+,a}<L>` and `{c1,+,a}<L>`. It includes logic to ensure that the "distance" between them is large enough that they cannot overflow. Concretely, it checks whether `BTC * |a| <s |c0 - c1|` holds, where `BTC` is the exact backedge-taken count of the loop `L`. 

Of course, overflow checks are necessary when calculating `c0 - c1` and `BTC * |a|`. In fact, in the Strong SIV test, the overflow checks are performed properly. However, there are several dependence tests that include similar logic but don't check overflows. I will describe two approaches to fix this problem.

## Approach 1

This is proposed by me (@kasuga-fj). The idea is that if we know the addrecs are monotonic over the entire iteration space (i.e., `[0, BTC]` for a single loop), the inequality `BTC * |a| <s |c0 - c1|` can be rewritten into a form that doesn't require additional overflow checks. Specifically, we can rewrite it as `max(c0, a*BTC + c0) <s min(c1, a*BTC + c1) || max(c1, a*BTC + c1) <s min(c0, a*BTC + c0)`.

I'd also like to note that the original formulation `BTC * |a| <s |c0 - c1|` is based on the paper [Practical Dependence Testing](https://softlib.rice.edu/pub/CRPC-TRs/reports/CRPC-TR90103-S.pdf). In that paper, the expression is transformed to make symbolic computation easier. However, the transformation assumes the absence of overflow, which I believe is not LLVM-friendly. Therefore I don't think we have to follow the paper strictly.

## Approach 2

This is proposed by @amehsan. Approach 1 requires the monotonicity over the entire iteration space, but it's unnecessary with this approach. https://github.com/llvm/llvm-project/issues/168823#issuecomment-3591966501 gives a proof that the current implementation of the Strong SIV test is correct even without such an assumption.

## Pros / Cons

DISCLAIMER: Probably the following pros and cons are strongly biased by my personal opinion.

- Approach 1
    - Pros
        - Simple and easy to implement.
    - Cons
        - Requires a stronger assumption (monotonicity in the entire iteration space).
            - This is I was actually pointed out in #162281, but as long as we are dealing with ZIV, SIV, and RDIV tests (i.e., the addrecs are not nested), the conditions "they have nowrap flags" and "the exact backedge-taken count is computable" imply this assumption. So in practice, I believe this may not be a big issue.
- Approach 2
    - Pros
        - Doesn't require a stronger assumption, which may allow more optimizations in the future.
            - In #162281, @amehsan mentioned the case where the memory accesses are conditionally executed thus SCEV cannot transfer nowrap flags from IR. @amehsan called this behavior as "conservative" and seemed to expect future improvements. I don't think it's appropriate to call it "conservative" and I believe such improvements would likely require significant engineering efforts.
    - Cons
        - The proof is too complex and is hard to verify its correctness. Also we need to keep the consistency between the implementation and the proof.

https://github.com/llvm/llvm-project/pull/176367