CUDA differs from Rust

[enricozb]

Reproducing the behavior

This program:

@List/Cons = (a (b ((@List/Cons/tag (a (b c))) c)))

@List/Cons/tag = 1

@List/Nil = ((@List/Nil/tag a) a)

@List/Nil/tag = 0

@id = (a a)

@list = c
  & @List/Cons ~ (1 (b c))
  & @List/Cons ~ (2 (a b))
  & @List/Cons ~ (3 (@List/Nil a))

@main = e
  & @map ~ ((a b) (d e))
  & @map ~ (a (@list b))
  & @List/Cons ~ (@id (@List/Nil d))

// @main__C0 = (a b)
//   & @map ~ (a (@list b))

@map = (a ((@map__C1 (a b)) b))

@map__C0 = (* (a (d ({(a b) c} f))))
  & @List/Cons ~ (b (e f))
  & @map ~ (c (d e))

@map__C1 = (?(((* @List/Nil) @map__C0) a) a)

Reduces to (in the rust runtime):

Result: ((@List/Cons/tag (((@List/Cons/tag (1 (((@List/Cons/tag (* (((@List/Cons/tag (* (@List/Nil vc4))) vc4) vb3))) vb3) va2))) va2) (@List/Nil vec))) vec)
- ITRS: 179
- TIME: 0.00s
- MIPS: 11.22

Reduces to (in the c runtime):

Result: ((@List/Cons/tag (((@List/Cons/tag (1 (((@List/Cons/tag (* (((@List/Cons/tag (* (@List/Nil xc00003b))) xc00003b) xc00002b))) xc00002b) xc00001b))) xc00001b) (@List/Nil x10000003))) x10000003)
- ITRS: 181
- TIME: 0.00s
- MIPS: 0.22

Reduces to (in the cuda runtime):

Result: ((@List/Nil/tag x2081) x2081)
- ITRS: 181
- LEAK: 2
- TIME: 0.10s
- MIPS: 0.00

[enricozb]

Narrowed it down to the following:

• when running CUDA and C without IO, then they agree with the rust implementation.
• The C and CUDA runtimes disagree with each other because of the following code difference:

// C implementation
Port expand(Net* net, Book* book, Port port) {
  Port old = vars_load(net, get_val(ROOT));
  Port got = peek(net, port);
  while (get_tag(got) == REF) {
    boot_redex(net, new_pair(new_port(REF,get_val(got)), ROOT));
    normalize(net, book);
    got = peek(net, vars_load(net, get_val(ROOT)));
  }
  // "offending" line below. 
  vars_create(net, get_val(ROOT), old);
  return got;
}

Port gnet_expand(GNet* gnet, Port port) {
  // missing an equivalent "vars_load"
  Port got = gnet_peek(gnet, port);
  while (get_tag(got) == REF) {
    gnet_boot_redex(gnet, new_pair(new_port(REF,get_val(got)), ROOT));
    gnet_normalize(gnet);
    got = gnet_peek(gnet, gnet_vars_load(gnet, get_val(ROOT)));
  }
  // missing an equivalent `vars_create`
  return got;
}

It's unclear to me which is correct.

[enricozb]

This difference in gnet_expand and expand was a bug is fixed here: #401, this might resolve this issue.