stack overflow hangs instead of aborting when the fault lands inside the allocator

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The SIGSEGV handler in src/runtime/stack_overflow.cpp calls pthread_getattr_np (line 60) to get
the current thread's stack bounds. On glibc that function calls realloc and free, so it is not
async-signal-safe. If the stack overflows while the thread is inside malloc with the arena lock
held, the handler blocks on the same lock on the same thread. The process hangs instead of printing
Stack overflow detected. Aborting. and exiting 134.

This happens with ordinary Lean code. Non-tail recursion doing bignum Nat arithmetic overflows
inside GMP's realloc, which goes through glibc. Recursion that only allocates Lean objects is fine
because those go through mimalloc, which is why the existing tests/compile/StackOverflow.lean
passes.

78bf3988 (2022) replaced fprintf with write in this handler, but the stack bounds lookup was
left as is.

Context

Found while testing resource exhaustion in a Lean project, where deep recursion in a decoder hung
the process instead of crashing. No prior Zulip discussion.

Steps to Reproduce

Repro.lean, no imports:

def sumFrom : Nat → Nat → Nat
  | 0,     _     => 0
  | n + 1, start => start + sumFrom n (start + 1)

def main (args : List String) : IO Unit := do
  let count := (args[0]!).toNat!
  let start := (args[1]!).toNat!
  IO.println (sumFrom count start)

$ lake build repro

$ LEAN_STACK_SIZE_KB=1024 ./.lake/build/bin/repro 100000 1
Stack overflow detected. Aborting.
$ echo $?
134

$ LEAN_STACK_SIZE_KB=1024 ./.lake/build/bin/repro 100000 18446744073709551616
(no output, never exits)

Same binary, same depth, same stack size. Starting from 1 keeps every intermediate below 2^63,
so nothing allocates; starting from 2^64 makes every addition a GMP bignum. 30 runs each: 30/30
clean aborts vs 30/30 hangs. The small stack only makes it fast; the default stack size hangs the
same way with a count of 40,000,000.

Expected behavior: both runs print Stack overflow detected. Aborting. and exit 134.

Actual behavior: the second run prints nothing and has to be killed.

Versions

Lean 4.34.0-rc2
Target: x86_64-unknown-linux-gnu Linux

Also reproduced on v4.33.0 and v4.33.1. stack_overflow.cpp is identical from v4.33.0 through
current master.

Linux 6.8, Debian 12, glibc 2.36. Only this glibc was tested. macOS is not affected: the __APPLE__
branch uses pthread_get_stackaddr_np, which does not allocate. musl not checked.

Additional Information

Backtrace of the hung process (gdb with handle SIGSEGV nostop noprint pass):

#0  futex_wait (private=0, expected=2, futex_word=0x7fffa8000030)
#1  __lll_lock_wait_private (futex=0x7fffa8000030)
#2  __libc_malloc (bytes=32)                            at malloc.c:3321
#3  __libc_realloc (oldmem=0x0, bytes=32)               at malloc.c:3412
#4  __pthread_getattr_np (...)                          at pthread_getattr_np.c:180
#5  segv_handler ()
#6  <signal handler called>
#7  _int_realloc (av=0x7fffa8000030, oldp=0x7fffa8002b70, oldsize=32, nb=32) at malloc.c:4825
#8  __libc_realloc (oldmem=0x7fffa8002b80, bytes=16)    at malloc.c:3489
#9  __gmp_default_reallocate ()
#10 __gmpz_realloc ()
#11 __gmpz_add ()
#12 lean::mpz::mpz(unsigned long) ()
#13 lean_nat_big_add ()
#14 lp_repro_sumFrom ()          <- repeated to the bottom of the stack

The futex in #0 is the arena lock av in #7. The handler is waiting on a lock held by the frame it
interrupted.

In glibc 2.36 the allocations are the realloc loop for the cpuset in pthread_getattr_np, the
realloc in pthread_attr_setaffinity_np it calls, and the frees in pthread_attr_destroy
(line 63). On the main thread there is also fopen("/proc/self/maps").

LD_PRELOADing a shim that replaces only pthread_getattr_np with a version returning bounds
captured at thread start turns the hang into a clean abort.

#eval is not affected because the interpreter's check_system throws before the guard page is
reached. Compiled code has no such check, and lean and lake are compiled Lean programs running
on an lthread with this handler.

Suggested fix: compute the stack bounds once at thread start and have the handler only read
them. stack_guard is already constructed on every runtime thread (thread.cpp:128) and on the
main thread, so its constructor is the natural place. sysconf(_SC_PAGESIZE) (line 66) can move
there too. This is what Rust does, including in the revision linked at line 52: the
pthread_getattr_np call Lean ported from there runs at thread start in Rust, not in the handler.

I opened PR with a fix - https://github.com/leanprover/lean4/pull/14993

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Read src/runtime/stack_overflow.cpp and the stack_guard construction in thread.cpp:128, then reproduce the two Repro.lean commands on Linux with glibc. Compare the existing tests/compile/StackOverflow.lean coverage with the allocator case. Done means both cases print the abort message and exit 134 without hanging.