Jason Gross (Oct 03 2022 at 14:15): Jason Gross (Oct 03 2022 at 14:15):How do I interpret the performance impact of https://github.com/mit-plv/rewriter/compare/8e4f92994633157b1e2d529c905ae2eb10915768...a2c8528deefda5743a924b0626da65f07534b102 at https://github.com/mit-plv/fiat-crypto/pull/1403/commits/b6b6d877b5b0d4f6f08d19c588b3552edb1b9190. It adds about 6s to fiat-crypto overall, and I can't tell whether or not I should interpret this as noise, or if it's about the overhead of doing let negb := 'negb in ... in cases where I previously wasn't, or if it's about the overhead of Ltac2 interpretation and closure allocation, or ....
image.png
Jason Gross (Oct 03 2022 at 14:18):Also https://github.com/mit-plv/fiat-crypto/pull/1403/commits/ff59eb31274f1cec841492b992295c7e20ed00cb / https://github.com/mit-plv/rewriter/compare/86dc030755216e713bb37f5ba9d9902d04c77028...e2cc315d40b5159cb8e224bf1ba20912da6eba7c
Removing a bunch of if statements and integer comparisons and indirections adds 11-12s to overall compilation time. Wth is going on here? (This is not noise, because https://github.com/mit-plv/fiat-crypto/pull/1403/commits/59eba23d08e83cd49d26c17d555746b5520c8567 reverts the change with https://github.com/mit-plv/rewriter/compare/e2cc315d40b5159cb8e224bf1ba20912da6eba7c...d57046bffdd5b70d6687bec0beaea9deabd23364 and gets the same timing result in the other direction (-12s instead of +11s))
Last updated: Oct 12 2024 at 12:01 UTC