Linearity bug in compiler?

Stream: lean4

[Kyle Miller]

@Patrick Massot and I were writing some array processing code and as an experiment we inserted dbgTraceIfShared to verify that some arrays were indeed not being shared, but we found instead that they were.

With a big more experimentation, the presence of dbgTraceIfShared was actually causing sharing. Here's a small example that shows the behavior:

import Lean

@[noinline]
def Array.add (a : Array Int) (c : Int) : Array Int := a.map (c + ·)

def test (a : Array Int) : Array Int := Id.run do
  let mut a := a
  for i in [0:a.size] do
    let c := a.getD i 0
    a := (dbgTraceIfShared "a" a).add c
  return a

def a : Array Int := #[1,2,3,4]

-- Sharing
#eval test a
/-
shared RC a
shared RC a
shared RC a
shared RC a
#[27, 28, 29, 30]
-/

@[noinline]
def Array.add' (a : Array Int) (c : Int) : Array Int := (dbgTraceIfShared "a" a).map (c + ·)

def test' (a : Array Int) : Array Int := Id.run do
  let mut a := a
  for i in [0:a.size] do
    let c := a.getD i 0
    a := a.add c
  return a

def a' : Array Int := #[1,2,3,4]

-- No sharing
#eval test' a'
/-
#[27, 28, 29, 30]
-/

[Kyle Miller]

Based on the IR, it looks like what's going on is that Array.getD is being unfolded and dbgTraceIfShared "a" a is being hoisted above a.get, leading to two live references to a.

[Scott Morrison]

A Heisenbug!

[Kyle Miller]

I don't know enough about the new vs old compiler to know if this worth reporting or not (or even whether #eval is using the new or old compiler) -- I'm assuming this is a bug though, given that it's transforming a program that uses a linearly into one that doesn't.

[Kyle Miller]

@Scott Morrison I like how this one is opposite of a normal Heisenbug -- here there's no bug until you look at it :smile:

[Johan Commelin]

So it's a coHeisenbug?

[Scott Morrison]

Maybe an anti-Heisenbug?

[Gabriel Ebner]

lean4#2218 The bad news is that this issue doesn't even need dbgTraceIfShared, you get the same nonlinearity when you write a.add 0 instead.