wnf_at is not thread-safe on shared cells

[o1lo01ol1o]

wnf_at is not thread-safe on shared cells

Under -T>=2 HVM4 returns different normal forms on different runs
for programs that share reducible subgraphs across multiple consumers.
The interaction calculus is confluent, so this is an implementation
bug in the C runtime, not a calculus-level issue.

Minimal reproduction

// repro.hvm
@name = "POLY_INPUT"
@main = #P{%env(@name), %env(@name)}

Build the runtime and run:

$ cd clang && clang -O2 -o main main.c

$ env POLY_INPUT=val1 ./main -C1 -T1 repro.hvm
#P{#OK{"val1"},#OK{"val1"}}                 # deterministic

$ for i in 1 2 3 4 5 6 7 8; do
    env POLY_INPUT=val1 ./main -C1 -T4 repro.hvm
  done
#P{#ERR{"ERROR(env): invalid `name`; expected #NIL or #CON(#CHR{NUM}, tail)"}, #OK{"val1"}}
#P{#OK{"val1"},#OK{"val1"}}
#P{#ERR{"ERROR(env): invalid `name`; ..."},#ERR{"ERROR(env): invalid `name`; ..."}}
#P{#OK{"val1"},#OK{"val1"}}
#P{#OK{"val1"},#OK{"val1"}}
#P{#ERR{"ERROR(env): invalid `name`; ..."},#OK{"val1"}}
#P{#OK{"val1"},#OK{"val1"}}
#P{#OK{"val1"},#OK{"val1"}}

Roughly 50% failure rate; also non-deterministic failure pattern
(sometimes left, sometimes right, sometimes both).

The empirical signature is consistent: the primitive %env's walker
chain (env_go_name → env_go_chr → env_go_num → env_go_io) observes
the character list in an inconsistent state — truncated or with BJV
placeholders at interior positions — and returns invalid \name``.

Root cause

The hot path in clang/wnf/_.c:831-858:

fn Term wnf_at(u64 loc) {
  Term cur = heap_read(loc);        // (1) atomic load
  switch (term_tag(cur)) {
    /* WNF-already cases ... */
    case C00 ... C16: return cur;
    ...
  }
  Term res = wnf(cur);              // (2) reduce off-heap
  if (res != cur) {
    heap_set(loc, res);             // (3) atomic store
  }
  return res;
}

Steps (1) and (3) are individually atomic, but the (read → reduce → write-back) triple is not. Two worker threads both enter
wnf_at(loc) with the same cur, both reduce it independently to
equivalent res values, both write back. Individually each write is
a valid result (confluence still holds), but consumers that read the
heap cells pointed to by res now see heap locations that were freshly
allocated by one thread and have already been rewritten by the other's
reduction, producing BJV/DP0/DP1 intermediates escaping into
primitive frames.

Compare the DP0/DP1 path on the same hot loop (clang/wnf/_.c:108)
which does use heap_take:

case DP0:
case DP1: {
  u64 loc = term_val(next);
  Term cell = heap_take(loc);       // atomic exchange: takes the cell
  ...
}

heap_take (clang/heap/take.c:11 — __atomic_exchange_n ... ACQUIRE)
gives one thread exclusive ownership of the cell for the duration of
the reduction. The other thread sees cell == 0 and is expected to
wait / retry. Every reduction step that commits a result back to
the heap needs this discipline, not just DP0/DP1.

Why user-level fixes don't help

• Wrapping an argument in !!x = val; body (strict let, clang/parse/term/dup.c:74-76)
  forces only the top-level WNF — not the char cells underneath.
  The sub-cells still race in wnf_at.
• Rebuilding the argument through a recursive strict fold (the same
  pattern used by @force_poly_bytes in callers' runtime preambles)
  does visit every sub-cell, but each visit still goes through the
  racy wnf_at path — at -T>=4 the fold itself deadlocks because
  two workers' write-backs to the same cell contend infinitely.
• Putting a pthread_mutex around a primitive doesn't help because
  HVM4 dispatches sub-primitives from worker threads independent of
  the caller's frame; the race is between the primitive's internal
  wnf calls and other workers reducing the same shared subgraph.
• Calling eval_normalize inside a primitive (clang/eval/normalize.c)
  spawns its own pthread pool, which compounds the same race
  because the inner SNF workers hit the same non-atomic wnf_at.

Proposed direction

Make every cache write-back in the reducers atomic with respect to
concurrent reads of the same cell. Concretely:

1. wnf_at (and the analogous cache steps at the end of interaction
   rules in clang/wnf/*.c) should heap_take the cell before
   reducing and write the result back through heap_set_rel (release-
   ordered store already exists as clang/heap/set_rel.c). When a
   second thread sees the cell 0, it either spins on heap_read
   until the writer publishes the result, or re-enters the original
   term through the ALO mechanism.
2. Every reduction rule that currently does ... = wnf(x); heap_set(loc, ...)
   needs the same lock-free discipline. A grep for heap_set inside
   clang/wnf/*.c is the full patch surface (≈20 sites).
3. Regression test: run the repro above for -T1..-T8 in the test
   harness and require byte-identical output.

The edits are mechanical but dense; the tricky part is picking the
right memory-order between the heap_take / heap_set_rel pair and
avoiding starvation when many workers hit the same cell. A reader-
waits-on-publication scheme parallels the existing term_sub_get /
term_sub_set SUB-bit protocol used in the DP0/DP1 path.

Scope

The fix is internal to clang/wnf/ and clang/heap/. No changes
needed to the language surface, the parser, or any primitive's
semantics. Single-threaded performance should not regress
appreciably: heap_take has identical cost to heap_read + first
write on the fast path.

Happy to begin implementing this if a maintainer 👍

[nicolas-abril]

Yes, and i'm almost sure it's on purpose for performance reasons. The bug is two threads calling wnf_at on the same location at the same time. The external task scheduling mechanism should make sure this doesn't happen

[o1lo01ol1o]

I don't understand how HVM side code could schedule (via forcing?) anything and remain confluent on -T>=2 because even if I sequence effectful primitives behind an interpreted free monad, eval_normalize still reduces all branches in parallel.

If you mean that implemented primitives in the C runtime should make sure that they are called at most once across all shared subgraphs, -- ie, they are somehow dedup'd -- that seems correct but it doesn't work for:

1. non-idempotent primitive calls and
2. primitives where an argument requires a reduction.

The problem in the first case is that pure lambda terms tolerate the mutate-in-place semantics of HVM's work stealing queue. Primitives in the runtime ("all effects") do not since they by definition are not pure terms.

The problem in the second is that the argument requires computation, we will trigger reduction that races on intermediate cells.

The only way I can see to handle this is to somehow dispatch the primitive at most once per shared argument. This means comparing closures of two shared calls and running them sequentially by blocking. But computing the closure is a lazy traversal and will race on the same cells we're trying to schedule.

So that's why the fix above proposes per-cell ownership.

I suppose you could also introduce a new soundness type in the core calculous that says "I'm not done computing yet" but I think that would shift the cost from atomic syncs in whnf_at to someplace else. Though, given the semantics may be closer to the "safe, correct" thing to do.

I would prefer of course to keep the performance and let user code sequnce effects but I don't see how this is possible.

[o1lo01ol1o]

Thinking more: The fundamental issue is effectual functions break confluence for ICs. Given that, either the evaluator needs to synchronize all writes (above) or the evaluator must be able to distinguish effectual reductions from pure reductions. Then, you could preserve the current whnf_at performance for pure code while scheduling effectual code. For example:

Tag primitives at interaction-rule dispatch. Extend the PRI case

  case PRI: {
    if (TWO_PHASE_ENABLED) {
      // Defer: record loc in the effect queue, leave the PRI cell alone,
      // surface the PRI term up the stack unchanged.
      effect_queue_push(loc);
      whnf = next;
      goto apply;
    }
    // current behavior
    WNF_S_POS = s_pos;
    next = wnf_pri(next);
    goto enter;
  }

Run SNF in two-phase loop — replace eval_normalize's single work-stealing sweep:

  fn Term eval_normalize(Term root) {
    loop:
      snf_sweep(root);              // parallel, -T>1, to quiescence
      if effect_queue.empty:
        return read(root);
      loc = effect_queue.pop();
      res = wnf_pri(heap_read(loc));  // single-threaded dispatch
      heap_set(loc, res);
      re_enqueue_for_snf(loc);
      goto loop;
  }

[nicolas-abril]

Arguments for effectful functions need to be normalized and if multithreaded this needs to be properly seuqenced to avoid reentry. The normalize function already does this and only dispatches each location once, but we can't reuse this mechanism directly for IO since locations can in fact be reused after the IO function returns.
It doesn't really surprise me that this doesn't work right now in hvm4, since the IO part is very underdeveloped.