FA-11481 / Compiler transformation correctness / Open access

Store forwarding crosses an intervening may-alias write · case 01

Store forwarding crosses an intervening may-alias write.

Verified by executionVariant 1 · 7 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

A candidate store value is forwarded without inspecting intervening writes.

VERIFIED REPAIR

Invalidate forwarding on must-alias or may-alias intervening writes.

Unsuccessful approach: Rejecting must-alias alone treats uncertainty as proof of disjointness.

Case contract

Return candidate value if every intervening write is proven disjoint; otherwise return None meaning retain the load. Alias facts are no, may, or must.

Why this case matters

A deterministic miniature compiler-pass model; inputs are explicit IR facts, not a production compiler.

1 / The failure

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(value, writes):
    return value
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('no writes', solve(N,[]), N)
check('disjoint write', solve(N,['no']), N)
check('must alias', solve(N,['must']), None)
check('may alias', solve(N,['may']), None)
check('may after disjoint', solve(N,['no','may']), None)
check('many disjoint', solve(N,['no']*N), N)
check('must after may', solve(N,['may','must']), None)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
no writes	`1`	`1`	Passed
disjoint write	`1`	`1`	Passed
must alias	`1`	`None`	Failed
may alias	`1`	`None`	Failed
may after disjoint	`1`	`None`	Failed
many disjoint	`1`	`1`	Passed
must after may	`1`	`None`	Failed

SHA-256 / e0e3a4a3ac9a0fe561b3298092e88c8deb11dec3da76435b593dba11196d9613

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(value, writes):
    return None if 'must' in writes else value
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('no writes', solve(N,[]), N)
check('disjoint write', solve(N,['no']), N)
check('must alias', solve(N,['must']), None)
check('may alias', solve(N,['may']), None)
check('may after disjoint', solve(N,['no','may']), None)
check('many disjoint', solve(N,['no']*N), N)
check('must after may', solve(N,['may','must']), None)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
no writes	`1`	`1`	Passed
disjoint write	`1`	`1`	Passed
must alias	`None`	`None`	Passed
may alias	`1`	`None`	Failed
may after disjoint	`1`	`None`	Failed
many disjoint	`1`	`1`	Passed
must after may	`None`	`None`	Passed

SHA-256 / 4df2c8e415b063cd17dc1a8a827c2c24adf0c15747ea12c72976bb9284a570ff

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(value, writes):
    return value if all(a == 'no' for a in writes) else None
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('no writes', solve(N,[]), N)
check('disjoint write', solve(N,['no']), N)
check('must alias', solve(N,['must']), None)
check('may alias', solve(N,['may']), None)
check('may after disjoint', solve(N,['no','may']), None)
check('many disjoint', solve(N,['no']*N), N)
check('must after may', solve(N,['may','must']), None)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
no writes	`1`	`1`	Passed
disjoint write	`1`	`1`	Passed
must alias	`None`	`None`	Passed
may alias	`None`	`None`	Passed
may after disjoint	`None`	`None`	Passed
many disjoint	`1`	`1`	Passed
must after may	`None`	`None`	Passed

SHA-256 / 3b469add7944bb189a3ebfefbb3e308b5f6cacfa938e7fe07666232bfae89e74

Verification & scope

This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.

Observations recorded using Python 3.12.14 at 2026-09-29T14:38:48.326718+00:00.

Case digest / 6dd322966b005961061337880e73ecaf5d2a0cf29c46e1e67c2292a4ee9f808a