Hi Andreas, thanks a lot for the quick response! This is precisely what I was looking for.
We indeed know, that memory accesses are always in bounds, so we can safely use the flag `--no-wasm-bounds-checks`. This speeds up one of our benchmarks by ~5% thanks! (for the others, the difference is not really measurable) Here is the Coq definition for instantiation [0] which we proved, this includes that the module is well-typed [1], so omitting the function validation check you suggested (ValidateFunctionBody) should be safe. However, doing that didn't affect the performance in a measurable way: It seems, function validation is quite cheap. (I compared the current master of Node.js (v8 version: 11.9.169.7) with and without the function validation check, by commenting out lines 87-101, 103 [2]. Our modules have <150 functions with around 10-1000 instructions and a main function with typically >50k instructions.) We also know that all programs terminate, but I guess we can still overflow the call stack, e.g. when the source program is big enough (and non-tail-recursive). Best, Wolfgang [0]: https://github.com/WasmCert/WasmCert-Coq/blob/1fda06ea0d52caae1ece83af109b48a9838b3869/theories/instantiation_spec.v#L530 [1]: https://github.com/WasmCert/WasmCert-Coq/blob/1fda06ea0d52caae1ece83af109b48a9838b3869/theories/instantiation_spec.v#L389 [2]: https://source.chromium.org/chromium/chromium/src/+/main:v8/src/wasm/function-compiler.cc;l=87;drc=d176526630b2049486a8be93fd89482d0aba6cfc;bpv=1;bpt=1 On Monday, March 25, 2024 at 11:16:00 PM UTC+1 [email protected] wrote: > Hi Wolfgang, > > The command "nodejs --help --v8-options" seems to print all V8 command > line options. It's not clear what runtime checks you would like to adjust. > Here are some flags I can think of: > > You could use --wasm-lazy-validation to avoid function validation during > module compilation and module instantiation, but function validation would > still happen lazily when a function gets executed for the first time. If > you want to prevent even the lazy function validation, then you have to > adjust the code at [1]. > > You can use `--no-wasm-stack-checks` if you can guarantee that there will > not be a stack overflow, e.g. because of an unbounded recursion. > > You can use `--no-wasm-bounds-checks` if you can guarantee that memory > accesses are always in-bounds. > > Cheers, Andreas > > [1] > https://source.chromium.org/chromium/chromium/src/+/main:v8/src/wasm/function-compiler.cc;l=97;drc=d176526630b2049486a8be93fd89482d0aba6cfc > > On Sun, Mar 24, 2024 at 7:41 PM Wolfgang <[email protected]> wrote: > >> Hello, >> I'm a masters student at Aarhus university. >> >> We built a provably correct compiler (using Coq) targeting Wasm: Link >> <https://womeier.de/files/certicoqwasm-coqpl24-abstract.pdf> >> This includes a proof that the modules our compiler generates instantiate >> according to the spec, i.e. they are well-typed. >> >> We are evaluating the performance with Node.js, is there a way to improve >> our performance >> by e.g. disabling some runtime-checks, given that we have the stronger >> correctness guarantees? >> >> Node.js doesn't seem to have (publicly documented) flags to allow that. >> >> I included some of our numbers below. >> >> Best, >> Wolfgang >> >> All times in ms, avarage of 10 runs: >> startup=load binary+instantiate >> main=main function >> pp=pretty printing the result as an S-expression, we call an imported >> function >> for every character, thus somewhat slow, but not that relevant for >> my question >> >> For a description of the benchmarks, see: Chapter 8.2, >> https://zoep.github.io/thesis_final.pdf >> >> Node.js: v18.19.0: >> demo1-opt_coalesce-locals : startup: 6, main: 0, pp: 28, >> sum: 34 >> demo2-opt_coalesce-locals : startup: 3, main: 0, pp: 8, >> sum: 11 >> list_sum-opt_coalesce-locals : startup: 3, main: 0, pp: 2, >> sum: 5 >> vs_easy-opt_coalesce-locals : startup: 10, main: 33, pp: 1, sum: >> 44 >> vs_hard-opt_coalesce-locals : startup: 10, main: 101, pp: 1, sum: >> 112 >> binom-opt_coalesce-locals : startup: 18, main: 10, pp: 24, >> sum: 52 >> sha_fast-opt_coalesce-locals : startup: 65, main: 70, pp: 7, >> sum: 142 >> color-opt_coalesce-locals : startup: 132, main: 44, pp: 2, >> sum: 178 >> >> Node.js: v20.11.1 >> demo1-opt_coalesce-locals : startup: 1, main: 3, pp: 24, sum: >> 28 >> demo2-opt_coalesce-locals : startup: 2, main: 0, pp: 12, sum: >> 14 >> list_sum-opt_coalesce-locals : startup: 2, main: 0, pp: 2, >> sum: 4 >> vs_easy-opt_coalesce-locals : startup: 4, main: 38, pp: 4, >> sum: 46 >> vs_hard-opt_coalesce-locals : startup: 3, main: 110, pp: 3, sum: >> 116 >> binom-opt_coalesce-locals : startup: 3, main: 26, pp: 23, >> sum: 52 >> sha_fast-opt_coalesce-locals : startup: 4, main: 228, pp: 10, sum: >> 242 >> color-opt_coalesce-locals : startup: 12, main: 332, pp: 2, >> sum: 346 >> >> >> >> -- >> -- >> v8-dev mailing list >> [email protected] >> http://groups.google.com/group/v8-dev >> --- >> You received this message because you are subscribed to the Google Groups >> "v8-dev" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/v8-dev/e7e5b6c8-0f7b-4787-b66f-592f02873950n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/v8-dev/e7e5b6c8-0f7b-4787-b66f-592f02873950n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > > > -- > > Andreas Haas > > Software Engineer > > [email protected] > > > Google Germany GmbH > > Erika-Mann-Straße 33 > > 80636 München > > > Geschäftsführer: Paul Manicle, Liana Sebastian > > Registergericht und -nummer: Hamburg, HRB 86891 > > Sitz der Gesellschaft: Hamburg > > > Diese E-Mail ist vertraulich. Falls sie diese fälschlicherweise erhalten > haben sollten, leiten Sie diese bitte nicht an jemand anderes weiter, > löschen Sie alle Kopien und Anhänge davon und lassen Sie mich bitte wissen, > dass die E-Mail an die falsche Person gesendet wurde. > > > > This e-mail is confidential. If you received this communication by > mistake, please don't forward it to anyone else, please erase all copies > and attachments, and please let me know that it has gone to the wrong > person. > > -- -- v8-dev mailing list [email protected] http://groups.google.com/group/v8-dev --- You received this message because you are subscribed to the Google Groups "v8-dev" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/v8-dev/5aa215cc-ed00-4577-bc54-d322161d44a3n%40googlegroups.com.
