From 7f19e275caf7a17383720e922913437738f062c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 21 Mar 2026 14:01:52 -0700 Subject: [PATCH 1/3] Precise memory measurent Our bench pipeline measures memory usage via ramon, which reports the memory of the whole cgroup (including Z3). This can be fixed, but can vary significantly anyway due to randomness is the system and the OCaml GC. Luckily, OCaml provides a way to query the peak bytes used by the heap, which we can write out and parse when benchmarking. This makes memory measurements much more stable (but not fully determistic). --- .github/workflows/bench.yml | 4 ++-- .scripts/ramon-report.py | 22 ++++++++++++++++++---- mk/common.mk | 4 +++- src/ml/FStarC_MemReport.ml | 17 +++++++++++++++++ stage1/dune/main.ml | 3 +++ stage2/dune/main.ml | 3 +++ stage3/dune/main.ml | 3 +++ 7 files changed, 49 insertions(+), 7 deletions(-) create mode 100644 src/ml/FStarC_MemReport.ml diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml index ef5707fbd88..a07bee1eb14 100644 --- a/.github/workflows/bench.yml +++ b/.github/workflows/bench.yml @@ -125,8 +125,8 @@ jobs: - name: Collect ramon files run: | mkdir -p ramon-files/base ramon-files/head - (cd fstar-base && find . -name '*.ramon' -exec cp --parents {} ../ramon-files/base/ \;) || true - (cd fstar-head && find . -name '*.ramon' -exec cp --parents {} ../ramon-files/head/ \;) || true + (cd fstar-base && find . \( -name '*.ramon' -o -name '*.fstarmem' \) -exec cp --parents {} ../ramon-files/base/ \;) || true + (cd fstar-head && find . \( -name '*.ramon' -o -name '*.fstarmem' \) -exec cp --parents {} ../ramon-files/head/ \;) || true - name: Upload artifacts uses: actions/upload-artifact@v4 diff --git a/.scripts/ramon-report.py b/.scripts/ramon-report.py index 9091164acdf..a27c1b4d14e 100755 --- a/.scripts/ramon-report.py +++ b/.scripts/ramon-report.py @@ -69,6 +69,19 @@ def load_ramon_file(fn): return None if "rc" not in ret or "time" not in ret or "mem" not in ret: return None + + # Prefer F*-only memory (excludes Z3) from companion .fstarmem file. + fstarmem_fn = fn.removesuffix(".ramon") + ".fstarmem" + try: + with open(fstarmem_fn) as f: + for line in f: + parts = line.split(None, 1) + if len(parts) >= 2 and parts[0] == "fstar.mempeak": + ret["mem"] = int(parts[1].strip()) + break + except FileNotFoundError: + pass + return ret def find_ramon_files(root): @@ -299,8 +312,8 @@ def md_table(items, n=20): # ── Notes ── L.append("---\n") - L.append("> **Note:** Time measurements are from single runs and may be noisy, especially for fast tests. " - "Memory measurements are generally more deterministic. " + L.append("> **Note:** Memory values report the peak OCaml heap of the F\\* process (excluding Z3 subprocesses). " + "Time measurements are from single runs and may be noisy, especially for fast tests. " "Tests with baseline time < 0.1s are excluded from time statistics. " "The geometric mean (Geo Mean) of the patched/baseline ratio is the most robust summary " "statistic for performance comparisons (1.0× = no change, <1× = improvement).") @@ -474,8 +487,9 @@ def stat_class(val, invert=False):
-Note on measurement reliability: Time measurements are from single runs and may be noisy, -especially for tests completing in under 5 seconds. Memory measurements are generally more deterministic. +Note on measurement reliability: Memory values report the peak OCaml heap of the F* process, +excluding Z3 subprocesses. Time measurements are from single runs and may be noisy, +especially for tests completing in under 5 seconds. Tests with baseline time < 0.1s are excluded from time statistics. The geometric mean (Geo Mean) of the patched/baseline ratio is the most robust summary statistic for performance comparisons (1.0× = no change, <1× = improvement). diff --git a/mk/common.mk b/mk/common.mk index 6d890774617..2e60cf300a6 100644 --- a/mk/common.mk +++ b/mk/common.mk @@ -46,7 +46,9 @@ ifneq ($(RESOURCEMONITOR),) ifneq ($(MONID),) MONPREFIX=$(MONID). endif - RAMON=ramon -o $@.$(MONPREFIX)ramon -- + # NB: this sets the Make variable RAMON to the string "FSTAR_MEM_REPORT=... ramon ...". + # In the recipe, the shell interprets FSTAR_MEM_REPORT=... as an env var for ramon. + RAMON=FSTAR_MEM_REPORT=$@.$(MONPREFIX)fstarmem ramon -o $@.$(MONPREFIX)ramon -- endif # Ensure that any failing rule will not create its target file. diff --git a/src/ml/FStarC_MemReport.ml b/src/ml/FStarC_MemReport.ml new file mode 100644 index 00000000000..496ea7d6c8f --- /dev/null +++ b/src/ml/FStarC_MemReport.ml @@ -0,0 +1,17 @@ +(* If FSTAR_MEM_REPORT is set, register an at_exit handler that writes + the peak OCaml heap size (in bytes) to the given file path. This + reports F*-only memory excluding Z3 subprocesses, which makes + memory benchmarks more deterministic. *) +let setup () = + match Sys.getenv_opt "FSTAR_MEM_REPORT" with + | Some fn -> + at_exit (fun () -> + try + let stat = Gc.quick_stat () in + let peak_bytes = stat.Gc.top_heap_words * (Sys.word_size / 8) in + let oc = open_out fn in + Printf.fprintf oc "fstar.mempeak %d\n" peak_bytes; + close_out oc + with _ -> () + ) + | None -> () diff --git a/stage1/dune/main.ml b/stage1/dune/main.ml index 93e5ff5c1e9..70195c626cf 100644 --- a/stage1/dune/main.ml +++ b/stage1/dune/main.ml @@ -27,4 +27,7 @@ let x = (* Tweak garbage collector parameters. *) Gc.set { (Gc.get()) with Gc.minor_heap_size = 1048576; Gc.major_heap_increment = 4194304; Gc.space_overhead = 150; }; + (* Set up peak heap memory reporting (for benchmarking). *) + Fstarcompiler.FStarC_MemReport.setup (); + Fstarcompiler.FStarC_Main.main () diff --git a/stage2/dune/main.ml b/stage2/dune/main.ml index 93e5ff5c1e9..70195c626cf 100644 --- a/stage2/dune/main.ml +++ b/stage2/dune/main.ml @@ -27,4 +27,7 @@ let x = (* Tweak garbage collector parameters. *) Gc.set { (Gc.get()) with Gc.minor_heap_size = 1048576; Gc.major_heap_increment = 4194304; Gc.space_overhead = 150; }; + (* Set up peak heap memory reporting (for benchmarking). *) + Fstarcompiler.FStarC_MemReport.setup (); + Fstarcompiler.FStarC_Main.main () diff --git a/stage3/dune/main.ml b/stage3/dune/main.ml index ab9489972ec..9d7686eff04 100644 --- a/stage3/dune/main.ml +++ b/stage3/dune/main.ml @@ -27,6 +27,9 @@ let x = (* Tweak garbage collector parameters. *) Gc.set { (Gc.get()) with Gc.minor_heap_size = 1048576; Gc.major_heap_increment = 4194304; Gc.space_overhead = 150; }; + (* Set up peak heap memory reporting (for benchmarking). *) + Fstarcompiler.FStarC_MemReport.setup (); + (* Only on stage3: we've baked Pulse into the compiler, which brings in the plugin library. Make sure F* knows this so it will not try to load it again. *) From 8067f9763acaf077aca1c602d989130c5e0a237c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 21 Mar 2026 14:34:27 -0700 Subject: [PATCH 2/3] Add !rebase command in github --- .github/workflows/rebase.yml | 85 ++++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 .github/workflows/rebase.yml diff --git a/.github/workflows/rebase.yml b/.github/workflows/rebase.yml new file mode 100644 index 00000000000..4c52d5dc966 --- /dev/null +++ b/.github/workflows/rebase.yml @@ -0,0 +1,85 @@ +name: Rebase PR + +# Triggered by posting a comment containing "!rebase" on a pull request. +# Rebases the PR branch onto its base branch and force-pushes the result. + +on: + issue_comment: + types: [created] + +defaults: + run: + shell: bash + +jobs: + rebase: + if: > + github.event.issue.pull_request && + contains(github.event.comment.body, '!rebase') && + contains(fromJSON('["OWNER","MEMBER","COLLABORATOR"]'), github.event.comment.author_association) + runs-on: ubuntu-latest + permissions: + pull-requests: write + contents: write + + steps: + - name: React to comment + uses: actions/github-script@v7 + with: + script: | + await github.rest.reactions.createForIssueComment({ + owner: context.repo.owner, + repo: context.repo.repo, + comment_id: context.payload.comment.id, + content: 'eyes' + }); + + - name: Get PR info + id: pr + uses: actions/github-script@v7 + with: + script: | + const pr = await github.rest.pulls.get({ + owner: context.repo.owner, + repo: context.repo.repo, + pull_number: context.issue.number, + }); + core.setOutput('head_ref', pr.data.head.ref); + core.setOutput('base_ref', pr.data.base.ref); + core.setOutput('head_repo_full_name', pr.data.head.repo.full_name); + core.setOutput('is_fork', pr.data.head.repo.full_name !== pr.data.base.repo.full_name); + + - name: Check if fork + if: steps.pr.outputs.is_fork == 'true' + run: | + echo "::error::Cannot rebase PRs from forks (no push access to ${{ steps.pr.outputs.head_repo_full_name }})" + exit 1 + + - name: Checkout PR branch + uses: actions/checkout@v4 + with: + ref: ${{ steps.pr.outputs.head_ref }} + fetch-depth: 0 + token: ${{ secrets.GITHUB_TOKEN }} + + - name: Rebase onto base + run: | + git config user.name "${{ github.event.comment.user.login }}" + git config user.email "${{ github.event.comment.user.id }}+${{ github.event.comment.user.login }}@users.noreply.github.com" + git fetch origin ${{ steps.pr.outputs.base_ref }} + git rebase origin/${{ steps.pr.outputs.base_ref }} + + - name: Force-push + run: git push --force-with-lease + + - name: React with result + if: always() + uses: actions/github-script@v7 + with: + script: | + await github.rest.reactions.createForIssueComment({ + owner: context.repo.owner, + repo: context.repo.repo, + comment_id: context.payload.comment.id, + content: '${{ job.status }}' === 'success' ? 'rocket' : '-1' + }); From 4b0f18243df1818595ed7b96552ded070fc02d1b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 19 Mar 2026 20:46:14 -0700 Subject: [PATCH 3/3] Improve substitution to avoid eager composition and preserve sharing Port key ideas from PR #3970 (subst improvements): 1. delay: Don't coalesce nested Tm_delayed nodes. Previously, delay would compose substitutions when encountering an existing Tm_delayed, which breaks structural sharing and causes quadratic memory blowup on deeply nested let-expressions (issue #3800). 2. push_subst: Handle Tm_delayed by recursing through compress_subst instead of failing. This allows nested delayed substitutions to be resolved incrementally. 3. Tm_uvar: Use simple compose_subst instead of compose_uvar_subst in push_subst. 4. compress: Simplified to a single recursive function that resolves uvars and pushes substitutions in one pass. Benchmarks (1116 matched tests, heavy tests > 100 MiB): Memory: median +0.0%, mean -0.1%, range [-20.4%, +4.3%] (Main impact is on pathological cases like issue #3800.) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/syntax/FStarC.Syntax.Subst.fst | 101 +++++++++-------------------- 1 file changed, 31 insertions(+), 70 deletions(-) diff --git a/src/syntax/FStarC.Syntax.Subst.fst b/src/syntax/FStarC.Syntax.Subst.fst index 840f24395a6..c001e0e7cd2 100644 --- a/src/syntax/FStarC.Syntax.Subst.fst +++ b/src/syntax/FStarC.Syntax.Subst.fst @@ -64,18 +64,14 @@ let compose_subst (s1 s2 : subst_ts) : subst_ts = | _ -> snd s1 in (s, ropt) -//apply a delayed substitution s to t, -//composing it with any other delayed substitution that may already be there +// Apply a delayed substitution s to t. +// This may nest Tm_delayed nodes, that is fine. If we coalesce +// them, that implies composing the substitutions and potentially breaking +// sharing. +let delay' (t:term) (s : subst_ts) rng : ML term = + mk_Tm_delayed (t, s) rng let delay (t:term) (s : subst_ts) : ML term = - match t.n with - | Tm_delayed {tm=t'; substs=s'} -> - //s' is the subsitution already associated with this node; - //s is the new subsitution to add to it - //compose substitutions by concatenating them - //the order of concatenation is important! - mk_Tm_delayed (t', compose_subst s' s) t.pos - | _ -> - mk_Tm_delayed (t, s) t.pos + delay' t s t.pos (* force_uvar' (t:term) : term * bool @@ -198,11 +194,11 @@ let rec subst' (s:subst_ts) (t:term) : ML term = | Tm_fvar _ -> tag_with_range t0 s //fvars are never subject to substitution | Tm_delayed {tm=t';substs=s'} -> - //s' is the subsitution already associated with this node; - //s is the new subsitution to add to it - //compose substitutions by concatenating them - //the order of concatenation is important! - mk_Tm_delayed (t', compose_subst s' s) t.pos + (* I really just want this: + delay t s + Or to remove this completely and fall in the default case above. + But somehow, that's incredibly bad for ranges. *) + delay' t' (compose_subst s' s) t.pos | Tm_bvar a -> apply_until_some_then_map (subst_bv a) (fst s) subst_tail t0 @@ -214,10 +210,7 @@ let rec subst' (s:subst_ts) (t:term) : ML term = mk (Tm_type (subst_univ (fst s) u)) (mk_range t0.pos s) | _ -> - //NS: 04/12/2018 - // Substitutions on Tm_uvar just gets delayed - // since its solution may eventually end up being an open term - mk_Tm_delayed (t0, s) (mk_range t.pos s) + delay' t0 s (mk_range t.pos s) let subst_dec_order' s = function | Decreases_lex l -> Decreases_lex (l |> List.map (subst' s)) @@ -367,16 +360,14 @@ let compose_uvar_subst (u:ctx_uvar) (s0:subst_ts) (s:subst_ts) : ML subst_ts = | s' -> [s'], snd s // -// If resolve_uvars is true, it will lookup the unionfind graph -// and use uvar solution, if it has already been solved -// see the Tm_uvar case in this function -// Otherwise it will just compose s with the uvar subst +// Push a substitution one level down. // -let rec push_subst_aux (resolve_uvars:bool) s t : ML _ = +let rec push_subst (s : subst_ts) (t : term) : ML _ = //makes a syntax node, setting it's use range as appropriate from s let mk t' = Syntax.mk t' (mk_range t.pos s) in match t.n with - | Tm_delayed _ -> failwith "Impossible (delayed node in push_subst)" + | Tm_delayed _ -> + push_subst s (compress_subst t) | Tm_lazy i -> begin match i.lkind with @@ -385,7 +376,7 @@ let rec push_subst_aux (resolve_uvars:bool) s t : ML _ = * The hope is that this does not occur often and so * we still get good performance. *) let t = Option.must !lazy_chooser i.lkind i in // Can't call Syntax.Util from here - push_subst_aux resolve_uvars s t + push_subst s t | _ -> (* All others must be closed, so don't bother *) tag_with_range t s @@ -396,14 +387,7 @@ let rec push_subst_aux (resolve_uvars:bool) s t : ML _ = | Tm_unknown -> tag_with_range t s //these are always closed | Tm_uvar (uv, s0) -> - let fallback () = - tag_with_range ({t with n = Tm_uvar(uv, compose_uvar_subst uv s0 s)}) s - in - if not resolve_uvars - then fallback () - else (match (Unionfind.find uv.ctx_uvar_head) with - | None -> fallback () - | Some t -> push_subst_aux resolve_uvars (compose_subst s0 s) t) + tag_with_range ({t with n = Tm_uvar(uv, compose_subst s0 s)}) s | Tm_type _ | Tm_bvar _ @@ -490,17 +474,14 @@ let rec push_subst_aux (resolve_uvars:bool) s t : ML _ = | Tm_meta {tm=t; meta=m} -> mk (Tm_meta {tm=subst' s t; meta=m}) -let push_subst s t : ML _ = push_subst_aux true s t - // // Only push the pending substitution down, // no resolving uvars // -let compress_subst (t:term) : ML term = +and compress_subst (t:term) : ML term = match t.n with | Tm_delayed {tm=t; substs=s} -> - let resolve_uvars = false in - push_subst_aux resolve_uvars s t + push_subst s t | _ -> t (* compress: @@ -513,41 +494,21 @@ let compress_subst (t:term) : ML term = 2. eliminate any top-level (Tm_uvar uv) node, when uv has been assigned a solution already - `compress` should will *not* memoize the result of uvar - solutions (since those could be reverted), nor the result - of `push_subst` (since it internally uses the unionfind - graph too). - - The function is broken into a fast-path where the - result can be easily determined and a recursive slow - path. - - Warning: if force_uvar changes to operate on inputs other than - Tm_uvar then the fastpath out match in compress will need to be - updated. - - This function should NEVER return a Tm_delayed. If you do any - non-trivial change to it, it would be wise to uncomment the check - below and run a full regression build. + This function should NEVER return a Tm_delayed, nor a resolved uvar. If + you do any non-trivial change to it, it would be wise to uncomment the + check below and run a full regression build. *) -let rec compress_slow (t:term) : ML _ = +let rec compress (t:term) : ML term = + let r = let t = force_uvar t in match t.n with | Tm_delayed {tm=t'; substs=s} -> - compress (push_subst s t') - | _ -> - t -and compress (t:term) : ML term = - match t.n with - | Tm_delayed _ | Tm_uvar _ -> - let r = compress_slow t in - (* begin match r.n with *) - (* | Tm_delayed _ -> failwith "compress attempting to return a Tm_delayed" *) - (* | _ -> () *) - (* end; *) - r + compress (push_subst s t') | _ -> - t + t + in + // compress_post_check r; + r let subst s t : ML _ = subst' ([s], NoUseRange) t let set_use_range r t : ML _ = subst' ([], SomeUseRange (Range.set_def_range r (Range.use_range r))) t