Hello, I'm a masters student at Aarhus university. We built a verified compiler targeting Wasm (https://popl24.sigplan.org/details/CoqPL-2024-papers/3/CertiCoq-Wasm-Verified-compilation-from-Coq-to-WebAssembly), which includes a correctness proof that the modules we generate instantiates according to the spec, i.e. they are well-typed.
Given these guarantees, is there an option, that would allow us to omit certain runtime checks to improve performance? We're evaluating the binaries with Node.js, which doesn't seem to have (publicly documented) flags to disable e.g. type-checking. I included some numbers below. Best, Wolfgang All times in ms, benchmarks are described in Chapter 8.2 in http://zoep.github.io/thesis_final.pdf startup: load binary+instantiation main: main function pp: pretty printing the resulting S-expression, works by calling an imported function print_char character-wise, thus somewhat slow, but not too important for my question here Node.js: v18.19.1 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-users mailing list v8-users@googlegroups.com http://groups.google.com/group/v8-users --- You received this message because you are subscribed to the Google Groups "v8-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to v8-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/v8-users/d9b421f9-2fff-4215-8143-3f7e3633a854n%40googlegroups.com.
