max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: use general allocator for closures (#10982)

Browse source 
This PR changes the closure allocator to use the general allocator
instead of the small object one.
This is because users may create closures with a gigantic amount of
closed variables which in turn
boost the size of the closure beyond the small object threshold.

This issue was uncovered by #10979. Detecting that the small object
threshold is at fault requires
building mimalloc in debug mode at which point it yields:
```
mimalloc: assertion failed: at "/home/henrik/lean4/build/debug/mimalloc/src/mimalloc/src/alloc.c":132, mi_heap_malloc_small_zero
  assertion: "size <= MI_SMALL_SIZE_MAX"
```
The generated code at fault here looks as follows:
```c
LEAN_EXPORT lean_object* l_initExec___at___00res_spec__0(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_2 = lean_alloc_closure((void*)(l_initializer_ext___at___00initExec___at___00res_spec__0_spec__0___lam__0___boxed), 3, 0);
x_3 = l_initExec___redArg___closed__0;
x_4 = l_initExec___redArg___closed__1;
x_5 = l_instMonadLiftNonDetT___closed__0;
x_6 = l_initExec___redArg___closed__2;
x_7 = l_initExec___at___00res_spec__0___closed__0;
lean_inc_ref(x_2);
x_8 = lean_alloc_closure((void*)(l_initExec___at___00res_spec__0___lam__29___boxed), 213, 212);
lean_closure_set(x_8, 0, x_3);
lean_closure_set(x_8, 1, x_2);
lean_closure_set(x_8, 2, x_4);
lean_closure_set(x_8, 3, x_3);
lean_closure_set(x_8, 4, x_4);
lean_closure_set(x_8, 5, x_3);
lean_closure_set(x_8, 6, x_4);
lean_closure_set(x_8, 7, x_3);
lean_closure_set(x_8, 8, x_4);
lean_closure_set(x_8, 9, x_3);
lean_closure_set(x_8, 10, x_4);
lean_closure_set(x_8, 11, x_3);
lean_closure_set(x_8, 12, x_4);
lean_closure_set(x_8, 13, x_3);
lean_closure_set(x_8, 14, x_4);
lean_closure_set(x_8, 15, x_5);
lean_closure_set(x_8, 16, x_6);
lean_closure_set(x_8, 17, x_5);
lean_closure_set(x_8, 18, x_5);
lean_closure_set(x_8, 19, x_5);
lean_closure_set(x_8, 20, x_5);
lean_closure_set(x_8, 21, x_5);
lean_closure_set(x_8, 22, x_5);
...
```
With the crash happening in `lean_alloc_closure` where we
unconditionally invoke the small allocator
which cannot cope with closures this large. Hopefully changing this to
the general purpose allocator
doesn't have too much of an impact on performance.

Closes: #10979
This commit is contained in:
Henrik Böving 2025-10-27 11:16:59 +01:00 • committed by GitHub
parent 8fe260de55
commit 334fa475b4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 260 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/include/lean/lean.h
View file

@ -715,7 +715,7 @@ static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lea
static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) {
assert(arity > 0);
assert(num_fixed < arity);
lean_closure_object * o = (lean_closure_object*)lean_alloc_small_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
lean_closure_object * o = (lean_closure_object*)lean_alloc_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
lean_set_st_header((lean_object*)o, LeanClosure, 0);
o->m_fun = fun;
o->m_arity = arity;

258
tests/compiler/large_closure_bug.lean Normal file
View file

@ -0,0 +1,258 @@
import Lean
import Std
abbrev IteratedProd (ts : List Type) : Type :=
ts.foldr Prod Unit
abbrev IteratedArrow (codomain : Type) (ts : List Type) : Type :=
ts.foldr (· → ·) codomain
section IteratedProdInstances
macro "infer_instance_for_iterated_prod" : tactic =>
`(tactic| repeat' (first | infer_instance | constructor ))
end IteratedProdInstances
section SingleField
variable (fieldDomain : List Type) (FieldCodomain : Type)
local macro "⌞" t1:ident t2:ident* "⌟" : term => `($t1 $(Lean.mkIdent `fieldDomain) $t2:ident*)
local macro "⌞_" t1:ident t2:ident* "⌟" : term => `(⌞ $t1 $(Lean.mkIdent `FieldCodomain) $t2:ident* ⌟)
abbrev FieldUpdatePat : Type := IteratedProd (fieldDomain.map Option)
abbrev CanonicalField : Type := IteratedArrow FieldCodomain fieldDomain
abbrev FieldUpdateDescr := List (⌞ FieldUpdatePat ⌟ × ⌞_ CanonicalField ⌟)
class FieldRepresentation (FieldTypeConcrete : Type) where
set : ⌞_ FieldUpdateDescr ⌟ → FieldTypeConcrete → FieldTypeConcrete
instance canonicalFieldRepresentation {fieldDomain : List Type} {FieldCodomain : Type} :
(⌞_ FieldRepresentation ⌟) (⌞_ CanonicalField ⌟) where
set favs fc := favs.foldr (init := fc) fun (_, v) _ => v
end SingleField
inductive NonDetT (m : Type u -> Type v) : (α : Type u) -> Type _ where
| pure {α} (ret : α) : NonDetT m α
| vis {α} {β} (x : m β) (f : β → NonDetT m α) : NonDetT m α
def NonDetT.bind (x : NonDetT m α) (f : α → NonDetT m β) : NonDetT m β :=
match x with
| pure ret => f ret
| vis x f' => vis x fun y => bind (f' y) f
instance : Monad (NonDetT m) where
pure := NonDetT.pure
bind := NonDetT.bind
instance : MonadLift m (NonDetT m) where
monadLift x := NonDetT.vis x pure
abbrev VeilM (σ α : Type) := NonDetT ((StateT σ (ExceptT Int Option))) α
inductive ExtractNonDet {m} : {α : Type u} -> NonDetT m α -> Type _ where
| pure {α} : ∀ (x : α), ExtractNonDet (NonDetT.pure x)
| vis {α} {β} (x : m β) (f : β → NonDetT m α) :
(∀ y, ExtractNonDet (f y)) → ExtractNonDet (.vis x f)
set_option linter.unusedVariables false in
def ExtractNonDet.bind :
(_ : ExtractNonDet x) -> (_ : ∀ y, ExtractNonDet (f y)) -> ExtractNonDet (x >>= f)
| .pure x, inst => by
dsimp [Bind.bind, NonDetT.bind]; exact (inst x)
| .vis x f inst, inst' => by
dsimp [Bind.bind, NonDetT.bind]; constructor
intro y; apply ExtractNonDet.bind <;> solve_by_elim
instance ExtractNonDet.pure' : ExtractNonDet (Pure.pure (f := NonDetT m) x) := by
dsimp [Pure.pure, NonDetT.pure]; constructor
instance ExtractNonDet.liftM (x : m α) :
ExtractNonDet (liftM (n := NonDetT m) x) := by
dsimp [_root_.liftM, monadLift, MonadLift.monadLift]; constructor
intro y; apply ExtractNonDet.pure'
macro "extract_step" : tactic =>
`(tactic|
first
| apply ExtractNonDet.bind
| apply ExtractNonDet.pure'
| apply ExtractNonDet.liftM
| split )
macro "extract_tactic" : tactic =>
`(tactic| repeat' (intros; extract_step <;> try dsimp))
abbrev VeilExecM (ε σ α : Type) := σ → Option (Except ε (α × σ))
def NonDetT.extract {α : Type} : (s : VeilM σ α) → (ex : ExtractNonDet s) → VeilExecM Int σ α
| .pure x, _ => fun s => (Option.some (Except.ok (x, s)))
| .vis x f, .vis _ _ _ =>
fun s =>
match x s with
| Option.some (Except.ok (y, s')) =>
extract (f y) (by rename_i a ; exact a y) s'
| Option.none => (Option.none)
| Option.some (Except.error e) => (Option.some (Except.error e))
inductive State.Label : Type where
| m_client_request
| m_marked_client_request
def State.Label.toDomain (l : State.Label) : List Type :=
State.Label.casesOn l [Bool] [Bool, Bool, Bool]
structure State (χ : State.Label → Type) where mk ::
m_client_request : χ State.Label.m_client_request
m_marked_client_request : χ State.Label.m_marked_client_request
def initializer.ext {χ : State.Label → Type}
[χ_rep : (f : State.Label) →
FieldRepresentation (State.Label.toDomain f) Bool (χ f)] : VeilM (State χ) Unit :=
do
let mut __veil_state := (← MonadState.get)
let mut m_client_request_conc := __veil_state.m_client_request
let mut m_marked_client_request_conc := __veil_state.m_marked_client_request
let __veil_bind_m_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
(fun _ => (false)))] m_client_request_conc
m_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
let __veil_bind_m_marked_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
(fun _ _ _ => (false)))] m_marked_client_request_conc
m_marked_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_marked_client_request,
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
-- NOTE: the following are just multiple copy & pastes of the do-elements above
let __veil_bind_m_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
(fun _ => (false)))] m_client_request_conc
m_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
let __veil_bind_m_marked_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
(fun _ _ _ => (false)))] m_marked_client_request_conc
m_marked_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_marked_client_request,
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
let __veil_bind_m_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
(fun _ => (false)))] m_client_request_conc
m_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
let __veil_bind_m_marked_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
(fun _ _ _ => (false)))] m_marked_client_request_conc
m_marked_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_marked_client_request,
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
let __veil_bind_m_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
(fun _ => (false)))] m_client_request_conc
m_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
let __veil_bind_m_marked_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
(fun _ _ _ => (false)))] m_marked_client_request_conc
m_marked_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_marked_client_request,
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
let __veil_bind_m_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
(fun _ => (false)))] m_client_request_conc
m_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
let __veil_bind_m_marked_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
(fun _ _ _ => (false)))] m_marked_client_request_conc
m_marked_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_marked_client_request,
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
let __veil_bind_m_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
(fun _ => (false)))] m_client_request_conc
m_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
let __veil_bind_m_marked_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
(fun _ _ _ => (false)))] m_marked_client_request_conc
m_marked_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_marked_client_request,
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
let __veil_bind_m_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
(fun _ => (false)))] m_client_request_conc
m_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
let __veil_bind_m_marked_client_request :=
(χ_rep _).set
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
(fun _ _ _ => (false)))] m_marked_client_request_conc
m_marked_client_request_conc ←
MonadState.modifyGet
(fun st =>
((__veil_bind_m_marked_client_request,
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
def initExec (χ : State.Label → Type) [χ_rep : ∀ f, FieldRepresentation (State.Label.toDomain f) Bool (χ f)]
: VeilExecM Int (State χ) Unit :=
NonDetT.extract (@initializer.ext χ χ_rep) (by (extract_tactic))
def res := initExec (fun f => CanonicalField ( (State.Label.toDomain) f) Bool) {
m_client_request := fun _ => false,
m_marked_client_request := fun _ _ _ => false
}
def main : IO Unit :=
IO.println s!"{[res].length}"

1
tests/compiler/large_closure_bug.lean.expected.out Normal file
View file

@ -0,0 +1 @@
1