Performance monitoring of the Everest build

[msprotz]

Following up on https://github.com/FStarLang/FStar/issues/2757...

@mtzguido you showed in https://github.com/FStarLang/FStar/pull/2734 how to monitor resource usage throughout the Everest build... including in F* and HACL*. Can we make this a regular feature, say, as part of the Everest upgrade CI job, and report very prominently the top files for memory consumption and/or time?

Rationale.

We have had a number of performance regressions over the past few months (https://github.com/FStarLang/FStar/issues/2757, https://github.com/hacl-star/hacl-star/issues/541, https://github.com/hacl-star/hacl-star/issues/539) and most of these are detected by accident, after the fact. (For instance, because we start having OOMs on HACL builds, or because I notice builds are starting to take much longer in Slack notifications, or because I keep an eye on my local build and notice some file taking an insane amount of time...)

This isn't super productive, and this prevents the F* team from having good feedback on the impact of their changes.

Concrete proposal.

I suggest adding a $(RUNLIM) variable in the HACL* build. Then, the Everest script exports RUNLIM="runlim -o [email protected]" so that the HACL* build collects the desired output. And then @mtzguido, your script can be used to report on the memory (or time) usage.

What do you think? CCing @tahina-pro for the Everest script part.

Thanks,

Jonathan

[mtzguido]

Hi Jonathan, I'm all for it! F* already has the infrastructure and will generate the report files if MON=1 is set. (Though it may be better as you say to have something more generic that takes any command, maybe MON=1 is a shortcut for that.) It should be straightforward to monitor other projects similarly (for HACL, it's a one liner). There's a performance hit from the monitoring, but only a few percent.

What I don't know is how to install runlim on the build machine. The packaged version (for debian at least) is quite old, so maybe we can build it ourselves? It's a single small file, so even doing it on every run wouldn't be too bad.

I can help with implementing this but I'm not familiar with the current CI. Is .github/workflows/linux-x64.yaml the entrypoint for CI runs? And the building proper is done by build_fstar in .docker/build/build_funs.sh?

[msprotz]

If we are talking about adding this to Everest regressions, then I suspect the plan of action would be:

• modify the everest script to package runlim (if applicable)
• modify the everest script to export M=1 and RUNLIM="runlim -o \$3.runlim" when doing everest make
• run your custom script to tally the results after everest make

Then, @tahina-pro knows how to hook this up to the Slack notifications for Everest upgrade in #everest-build.

Tahina, what would be the easiest way to accomplish this?

Guido, I've pushed branch protz_runlim on HACL* that should help hook up the resource monitoring to the build.

Thanks!

[mtzguido]

I pushed some branches to F*, karamel and HACL* adding MON and RUNLIM (for F*: just renaming a bit). The idea is that setting MON=1 will define RUNLIM=runlim -p -o [email protected] and that is used as a prefix for every "interesting" command in rules. For Karamel I just added this to krmllib.

(Actually seems I cannot push to the HACL* repo? So I'm attaching the patch below)

Detail, possibly unimportant: for HACL* I am using $@ instead of $3 as suggested. Other projects use $@ (they have no run-with-log equivalent) and it "just works", though it does depend on macro expansion of $(RUNLIM).

If this looks sane, I think we can just merge it: it is not used by the build system until we flip MON=1, and we can already start using it ourselves.

As for the summary script, I will tweak it a bit more. What's a good place for it to live? Maybe in everest repo? It's currently in F*, but we could remove it and put it in everest, and possibly all of us can keep a copy in our ~/bin.

https://github.com/FStarLang/FStar/commit/dfc027def50250f1b9d17f8724fb447990c0b250 https://github.com/FStarLang/karamel/commit/67cee42a13aa8ac4a112e1ab9af77cb071f6cb85

From e2acea245390bf06f95cd3a9437baac94d379b7c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <[email protected]>
Date: Sun, 20 Nov 2022 10:59:15 -0300
Subject: [PATCH] Makefile: introduce resource monitoring with $(MON) and
 $(RUNLIM)

---
 .gitignore |  1 +
 Makefile   | 10 +++++++++-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index dc0ad8154d..22d36a4273 100644
--- a/.gitignore
+++ b/.gitignore
@@ -32,3 +32,4 @@ doc/_build
 config.h
 *.smt2
 flake.lock
+*.runlim
diff --git a/Makefile b/Makefile
index da210a9d83..7b6a08e3c8 100644
--- a/Makefile
+++ b/Makefile
@@ -201,6 +201,13 @@ endif
 
 SHELL:=$(shell which bash)
 
+# Passing MON=1 to this Makefile will create .runlim files throughout
+# the tree with resource information. The $(RUNLIM) variable can also be
+# defined directly if needed.
+ifneq ($(MON),)
+  RUNLIM = runlim -p -o [email protected]
+endif
+
 # A helper to generate pretty logs, callable as:
 #   $(call run-with-log,CMD,TXT,STEM)
 #
@@ -211,6 +218,7 @@ SHELL:=$(shell which bash)
 ifeq (,$(NOSHORTLOG))
 run-with-log = \
   @echo "$(subst ",\",$1)" > $3.cmd; \
+  $(RUNLIM) \
   $(TIME) -o $3.time sh -c "$(subst ",\",$1)" > $3.out 2> >( tee $3.err 1>&2 ); \
   ret=$$?; \
   time=$$(cat $3.time); \
@@ -226,7 +234,7 @@ run-with-log = \
     false; \
   fi
 else
-run-with-log = $1
+run-with-log = $(RUNLIM) $1
 endif
 
 
-- 
2.35.1

[mtzguido]

Oh: and runlim needs to be a relatively recent version that supports -p. This is the source repo, and I don't think any packaged version is recent.

[msprotz]

Thanks Guido!

Regarding PR on HACL: you should be able to submit a PR onto the hacl-star/hacl-star repository from an external fork (the usual GitHub fork + pr workflow).

Your patch looks good; three comments:

• we generally try to avoid abbreviations, it might not be obvious for everyone that MON means "monitor" (it could mean "monad", or "mono" in the context of .net); for consistency with other variables (NOSHORTLOG, NOOPENSSL, NODEPEND, SKIPDEPEND), please expand to MONITOR (or better, RESOURCEMONITOR)
• all of our build products go into the obj/ directory -- please make sure .runlim files are output in obj/
• there's a list of known variables for this Makefile, around line 13 -- you might want to add RESOURCEMONITOR in there

Thanks again, very much looking forward to keeping an eye on memory regressions... cheers

[mtzguido]

Hi Jonathan, thanks for reviewing!

• we generally try to avoid abbreviations, it might not be obvious for everyone that MON means "monitor" (it could mean "monad", or "mono" in the context of .net); for consistency with other variables (NOSHORTLOG, NOOPENSSL, NODEPEND, SKIPDEPEND), please expand to MONITOR (or better, RESOURCEMONITOR)

Agreed, changed it to RESOURCEMONITOR.

• all of our build products go into the obj/ directory -- please make sure .runlim files are output in obj/

This one may be a bit tricky. Currently we are just creating a file name TARG.runlim where TARG is the target of the relevant rule. Since most rules (that go via run-with-log) generate files in obj/, then the runlim files also live there. The only exceptions after a full build are:

$ find . -name '*.runlim' | grep -v '^\./obj/'
./.fstar-depend-make.runlim
./.fstar-depend-full.runlim
./.vale-depend.runlim

which makes sense to me that they live there..? WDYT?

Also note that the rules for generating the C files in dist/ do not go via run-with-log, hence they're not monitored. If we want to monitor them then we do need to modify the rule to prefix an obj/ to the path, or something similar.

It sounds doable, though possibly flaky (relative vs absolute paths, need to mkdir, etc). How do you feel about it? If you think that's better I can do it.

• there's a list of known variables for this Makefile, around line 13 -- you might want to add RESOURCEMONITOR in there

Done, will post a draft PR from my fork soon.

[msprotz]

Ok, thanks for pointing that out -- let's not bother with relative paths into obj/, I think the rule is fine as-is and having .runlim files for the .depend files is not a big deal.

Rest looks good. Thanks again!

[mtzguido]

Made some PRs for this in the subprojects:

https://github.com/FStarLang/FStar/pull/2781 https://github.com/FStarLang/karamel/pull/317 https://github.com/hacl-star/hacl-star/pull/727