CakeML / CakeML/cakeml

Repeated Array.sub of the same array and index retains a redundant bounds check

Open
#1,454 0 comments 0 reactions 0 assignees View on GitHub
high reward performance
Dominant language
Standard ML
Stars
1.2k
Forks
104
Avg merge
2d 21h
Merged PRs (30d)
16

Description

## Summary

Two consecutive safe array reads using the same array and index retain two
identical bounds checks, even when there is no intervening call, store, or other
mutation. The compiler does eliminate the duplicate element load, but not the
second check and its failure branch.

This is a realistic missed optimization for code that reuses an array element
within an expression or basic block. In a small x64-64 benchmark, manually
binding the element once made the loop 1.44–1.56× faster.

## Reproducer

Repeated source form:

```sml
fun get_twice a i = Array.sub a i + Array.sub a i;

fun repeat n a acc =
if n = 0 then acc
else repeat (n - 1) a (acc + get_twice a 5);

fun main () =
let
val n = Option.valOf
(Int.fromString (List.hd (CommandLine.arguments ())))
val a = Array.tabulate 10 (fn i => i)
in
print_int (repeat n a 0);
print "\n"
end;

main ();
```

Source-hoisted control:

```sml
fun get_twice a i =
let val x = Array.sub a i
in x + x end;

fun repeat n a acc =
if n = 0 then acc
else repeat (n - 1) a (acc + get_twice a 5);

fun main () =
let
val n = Option.valOf
(Int.fromString (List.hd (CommandLine.arguments ())))
val a = Array.tabulate 10 (fn i => i)
in
print_int (repeat n a 0);
print "\n"
end;

main ();
```

Compile both normally for x64-64 and run each with argument `100000000`.
For example, from an x64-64 build directory:

```sh
./cake < repeated.cml > repeated.S
cc -O2 repeated.S basis_ffi.c -lm -o repeated
./repeated 100000000
```

Three paired runs gave:

| Form | Run 1 | Run 2 | Run 3 |
|---|---:|---:|---:|
| Repeated `Array.sub` | 0.58 s | 0.59 s | 0.39 s |
| Source-hoisted element | 0.38 s | 0.41 s | 0.25 s |

Both programs print the same result. The paired slowdown of the repeated form
was 1.44–1.56×. Exact timings will vary; the generated-code difference below is
the primary evidence.

The measurements used CakeML
`535ff9fb8b11b2f49662e21b3f95401ea5f8ed0e`. The relevant lowering files are
unchanged at `0fe74ee25d03a7d6d72892927edcaf5ae9677e10`.

## Generated-code evidence

For the repeated form, `get_twice` contains:

1. one load of the array header/length;
2. a bounds comparison and branch to the `Subscript` path;
3. one load of the selected element;
4. the same bounds comparison and another branch to the `Subscript` path;
5. the addition of the already-loaded element to itself.

There is no call, store, index change, or array change between the two checks.
The two relevant x64 fragments are:

```asm
cmp %r8,%rax
jb
...
:
...
mov 0x8(%rdx),%rdx
cmp %r8,%rax
jb
...
```

The source-hoisted control has one header/length load, one bounds check, and one
element load. In this build, the repeated `get_twice` body was 172 bytes versus
148 bytes for the control.

Safe `Array.sub` is still represented explicitly as a bounds test followed by
the element read when it enters ClosLang
([`flat_to_closScript.sml`](https://github.com/CakeML/cakeml/blob/0fe74ee25d03a7d6d72892927edcaf5ae9677e10/compiler/backend/flat_to_closScript.sml#L198-L200)).
The check is expanded into a header load and unsigned comparison during
DataLang-to-WordLang lowering
([`data_to_wordScript.sml`](https://github.com/CakeML/cakeml/blob/0fe74ee25d03a7d6d72892927edcaf5ae9677e10/compiler/backend/data_to_wordScript.sml#L1725-L1737)).

## Expected result

When a safe access to the same array and index is dominated by an already
successful identical check, and nothing relevant has changed, the second check
should be eliminated. The generated code should retain one element load and one
possible `Subscript` path for this example.

Useful regression coverage would include:

- the direct repeated-access example above;
- checks dominated through a simple successful branch;
- changed array or index values, for which the earlier check is insufficient;
- intervening calls or mutations, according to the chosen analysis policy;
- the corresponding vector, byte-array, byte-vector, and string operations.

## Design note

This report intentionally does not prescribe an IR or pass. The semantic bounds
operation exists at several higher levels and becomes a machine comparison
later, so local path facts, common-subexpression treatment, range analysis, and
other designs are all plausible. The requested outcome is the removal of
provably redundant checks while preserving `Subscript` behavior.

_Written by Codex (OpenAI)._

Contributor guide

No contributing guide indexed for this repository

Research direction

Start with compiler/backend/flat_to_closScript.sml and compiler/backend/data_to_wordScript.sml at the cited lowering points. Compile the repeated and source-hoisted reproducers in an x64-64 build and inspect the generated assembly. Done means provably redundant safe-access checks are removed while Subscript behavior and changed-value cases remain correct.

Written by the indexing model from the issue text.

Assessment

Domain
compilers, performance
Issue type
Bug
Difficulty
5/5
Estimated time
Over a week
Activity status
Quiet
Clarity
Mostly clear
Newbie friendliness
45/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.