Executable specifications in flang Performance: a reproducible measurement
0%

Performance: a reproducible measurement

Performance: a reproducible measurement

A number without a way to reproduce it is not a fact but a claim taken on faith. So this chapter does not quote “the speed of flang” in general. It gives you the harness examples/spec/benchmark/, with which you take the numbers on your own machine, and shows which numbers it produced on the machine where the course was prepared, and under what conditions.

Minimal example

The harness measures a model it builds itself. Here it is with three rules — the measurement uses 10, 30 and 100 rules:

модуль «Замер»

объект «Заявка»
  «объём»: неотрицательное
  «премиум клиент»: признак

тотальная функция «Правило 1»
  принимает заявка: «Заявка»
  возвращает число
  обеспечивает «правило 1 не больше единицы» результат не больше 1
  если заявка.«объём» не меньше 1
    то 1
    иначе 0

тотальная функция «Правило 2»
  принимает заявка: «Заявка»
  возвращает число
  обеспечивает «правило 2 не больше единицы» результат не больше 1
  если заявка.«объём» не меньше 2
    то 1
    иначе 0

тотальная функция «Правило 3»
  принимает заявка: «Заявка»
  возвращает число
  обеспечивает «правило 3 не больше единицы» результат не больше 1
  если заявка.«объём» не меньше 3
    то 1
    иначе 0

тотальная функция «Сумма правил»
  принимает заявка: «Заявка»
  возвращает число
  пример «все правила сработали»
    дано заявка равно запись «Заявка» с «объём» равным 3 и «премиум клиент» равным нет
    ожидается 3
  («Правило 1» от заявка) плюс («Правило 2» от заявка) плюс («Правило 3» от заявка)

Every rule carries a promise the kernel proves, and on the input “volume = number of rules” all rules fire — the call goes through every branch, not through a share that would depend on the data. The model text is deterministic: the createSource function in measure.mjs builds exactly the same one for you.

What the compiler does

The harness measures four operations:

Operation Command What happens inside
check_proof flang check --proof parsing, types, termination, proof kernel, report
test flang test the check plus running the examples
emit_js flang emit --target js the check plus printing the module
call a call of the printed function plain JavaScript, no compiler

The first three are compiler work: you pay for it in CI and when you edit the model. The last one is the cost of the rule at runtime in your application, once the model has been printed.

Either of the two compilers can do the work: the native flang binary (FLANG_BIN) or the WebAssembly build that powers the sandbox. The report says which of the two was measured.

Measurement method

  • Expensive operations — the median of five runs. The first run is discarded: for WebAssembly it compiles the module, for the binary it warms the disk cache. Each binary run is a new process, and process start-up is part of the number: that is how CI calls it.
  • The call — as a micro-benchmark. A single call takes microseconds, and at that scale the timer resolution is comparable to what is measured. The harness makes 5 warm-up calls, sizes a batch so that one measurement takes at least 2 ms, and divides the time by the batch size.
  • Median, not mean. One garbage-collection pause or a neighbouring process stealing a core drags the mean along and barely moves the median. min/max/p95 in the report show the spread.
  • A refusal is a result too. If the compiler did not perform an operation, the report row names the code and the reason instead of an invented number.

Your numbers with one command

node examples/spec/benchmark/measure.mjs
FLANG_BIN=~/.local/bin/flang node examples/spec/benchmark/measure.mjs

Output on the machine where this module was prepared: flang 0.7.29, node v26.7.0, linux/x64, AMD EPYC 7742 64-Core Processor, 256 cores. The machine is shared, and other jobs ran on it during the measurement — load average 34–37. Median in milliseconds, native flang binary:

Operation 10 rules 30 rules 100 rules
check_proof 317.68 1317.02 6586.19
test 122.67 445.21 1136.03
emit_js 196.51 648.48 1870.43
call 0.0007 0.0020 0.0066

The same in WebAssembly:

Operation 10 rules 30 rules 100 rules
check_proof 359.18 1437.29 refused
test 115.03 364.76 1071.64
emit_js 205.04 584.24 1801.61
call 0.0007 0.0022 0.0069

Full reports with mean/min/max/p95 are in examples/spec/benchmark/baseline-linux-x64-binary.json and examples/spec/benchmark/baseline-linux-x64-wasm.json, taken with the same command and the --out key.

What the numbers show:

  • The proof report is the most expensive part. When the model grows tenfold, check_proof becomes 20.7 times more expensive, while test and emit_js grow 9.3 and 9.5 times. The proof kernel grows faster than the model; parsing, types and examples grow roughly in step with it.
  • The call is cheap and grows linearly. 100 rules cost 6.6 microseconds per call, 9.4 times more than 10. The printed function is plain JavaScript, and the runtime cost of a rule is the cost of its branches.
  • WebAssembly has a step limit. With 100 rules, flang check --proof in WebAssembly stops:
FLANG_RECURSION_LIMIT: функция «Склеить до закрытия записи» исчерпала лимит шагов (2770894848) на глубине вызовов 0

The native binary checks the same file in 6.6 seconds. In WebAssembly test and emit_js pass on 100 rules: the limit is hit while building the report. A practical rule follows: check large models in CI with the binary, and use the sandbox for models the size of a course chapter.

Comparing with a baseline

node examples/spec/benchmark/compare.mjs my.json examples/spec/benchmark/baseline-linux-x64-binary.json

compare.mjs prints the deviation of the median in percent, operation by operation. Reports from other hardware or another compiler cannot be compared literally, and the tool warns about it. Here is a comparison of the two baselines of this machine — WebAssembly against the binary:

текущий:  flang 0.7.29 (WebAssembly), node v26.7.0, linux/x64, AMD EPYC 7742 64-Core Processor
baseline: flang 0.7.29 (двоичный), node v26.7.0, linux/x64, AMD EPYC 7742 64-Core Processor

ВНИМАНИЕ: отчёты сняты разными компиляторами (двоичный и WebAssembly) или разными версиями flang —
это сравнение двух инструментов, а не поиск регрессии.

operation             scale                 current_ms            baseline_ms           diff_%                
check_proof           10                    359.1829              317.6813              +13.1%                
test                  10                    115.0273              122.6653              -6.2%                 
emit_js               10                    205.0385              196.511               +4.3%                 
call                  10                    0.0007                0.0007                0%                    
check_proof           30                    1437.2911             1317.0195             +9.1%                 
test                  30                    364.7555              445.2098              -18.1%                
emit_js               30                    584.2429              648.4786              -9.9%                 
call                  30                    0.0022                0.002                 +10%                  
test                  100                   1071.6421             1136.0297             -5.7%                 
emit_js               100                   1801.605              1870.4332             -3.7%                 
call                  100                   0.0069                0.0066                +4.5%                 
check_proof@100: текущий — отказ, код 1, baseline — посчитано

On one machine the two compilers stay within tens of percent of each other; the gap between them is of the same order as the noise of a loaded machine. The useful signal is to compare today’s report with yesterday’s: same CPU, same compiler, same method. If check_proof on 100 rules suddenly triples on the same hardware, that is a regression of the model or the compiler, not noise.

The cost of one run without the harness

Two flang commands answer the cost question without any extra code.

flang run --cost prints the number of evaluator steps, peak memory and time to the error stream after the value:

flang run static/spec/models/order-discount.flang --trust --cost --function "Скидка по сумме" --args '{"сумма":20000,"постоянный":true}'
на веру: доказанность не считалась — запуск по ключу --trust
3000
цена прогона: шагов 118, пик памяти 19599360 байт, секунд 0.086407

Steps are a property of the program, seconds are a property of the machine. flang --machine measures the machine constant: how many parsing and lexing steps it performs per second, and it also reports the load:

машина
  ядер: 256
  занято ядер: 84.45
  свободно ядер: 171.55
  витков в секунду, разбор: 257340938
  витков в секунду, лексер: 542350029
  разброс: 0.47

The --step-limit N key raises the compiler’s own step limit for one run — use it to check a large model that hit the default. --max-steps N limits the evaluation of a function in flang run, and in flang emit it is baked into the printed program; it says nothing to the current run.

What these numbers do not mean

The harness measures the flang compiler and the printed function in Node.js. It does not measure:

  • a bundler build around the printed code or tsc over the whole project;
  • network and disk;
  • behaviour under concurrent load — the harness is single-threaded and sequential.

The order of magnitude is worth stating. Checking a model the size of a course chapter — dozens of fields and rules — takes tenths of a second or a couple of seconds. That is the cost of a CI step and of editing the model, not of a request: the compiler does not go into the runtime at all, where the printed function runs in microseconds. It is worth measuring explicitly when there are hundreds of rules: the proof report grows faster than the model, and at a hundred rules it already takes seconds.

Measuring in CI

A regression is caught not by an absolute threshold — noisy runners on a shared CPU spread so much that a fixed percentage either fires falsely or catches nothing — but by comparing with the previous report on the same runner:

- run: node examples/spec/benchmark/measure.mjs --out current.json
- run: node examples/spec/benchmark/compare.mjs current.json baseline.json
# baseline.json — артефакт предыдущего успешного прогона на master,
# сохранённый через actions/cache или actions/upload-artifact
- run: node examples/spec/benchmark/compare.mjs current.json baseline.json --json > diff.json

Next comes a small wrapper script (not part of the harness) that reads diff.json and fails if diff_percent for the chosen operation and scale exceeds a threshold with a margin for runner noise — say, twofold rather than 10 %. The point is to catch jumps of an order of magnitude, not to page the team on every percent. compare.mjs prints refusal rows separately: if an operation used to be computed and now hits a limit, that signal matters more than any percentage.

Practice in the sandbox

The sandbox shows time too: under the answer it prints “N ms” — how long the check took in your browser. This is not the same measurement as measure.mjs: in the sandbox it is a single run without warm-up and without a median, and the very first check is also slowed down by downloading the compiler — about 9.3 MB compressed, after which it comes from the browser cache. Such a number is useful as a feeling that “on this device it is fast”, but it is no good for comparing runs. The harness is meant for something else — a trend you can put into CI and compare day after day.

Checklist

  • Take the measure.mjs numbers on your own machine — do not pass off someone else’s as yours.
  • Name the compiler: the binary and WebAssembly are different tools.
  • Compare with compare.mjs against your previous report on the same hardware first; a foreign baseline only by the shape of growth.
  • Check large models in CI with the binary: WebAssembly has a lower step limit.
  • Remember that the expensive part is the proof report in CI, not the call of the printed function at runtime.
  • In CI compare with the previous run on the same runner and choose a threshold with a margin for noise.

Catalogue cases on this topic

Next: the end-to-end project

Spotted a mistake? Select a fragment of the text — a bug icon will appear next to it.

Нужен разбор именно вашей ситуации?

Статья описывает общий случай. Если у вас частный — можно разобрать его отдельно, платно. А если не хватает целого материала, предложите тему: её оплачивают вскладчину, и она выходит открытой для всех.

Доска запросов
Next