ocaml-solo5/fuzz/ at main · gazagnaire.org/ocaml-solo5 · Tangled

gazagnaire.org / ocaml-solo5

0

Solo5 hvt ABI and MFT1/ABI1 note format as wire codecs

0

ocaml-solo5 / fuzz

4 files

at main

Thomas Gazagnaire solo5: write the walltime nsecs as two u32 words, not a boxed int64 3w ago

solo5: write the walltime nsecs as two u32 words, not a boxed int64 handle_walltime wrote the OUT nanosecond time via Hc.set_walltime_nsecs -> Guest.set_u64 (int64); now_ns's Int64.of_float boxed an int64 per WALLTIME hypercall (19.4M x 16 B = 226 MB, the last per-op allocation on the bench once Mmio.write and Continue_read were fixed). A wall-clock time in nanoseconds fits a native int (< 2^62 for ~146 years), so now_ns is int_of_float and set_walltime_nsecs writes the 8-byte field as two little-endian 32-bit words with no int64. The fuzz masks its OUT value to 62 bits and expects that round-trip; it also gains its mli and the pp_/suite-name conventions. All solo5 tests pass. bench total 15.30 GB -> 19.84 MB across the session; every per-frame / per-hypercall / per-register path is now allocation-free.

3 weeks ago

ocaml-solo5: Add shared tender and KVM backend Move the backend-independent hvt tender into solo5-tender and add the Linux KVM backend alongside HVF. Replace the old generated C ABI bindings with Wire codecs and direct hot-path accessors, add a single production benchmark suite with probe coverage, and update the tests and package metadata for the new layout.

1 month ago

solo5: write the walltime nsecs as two u32 words, not a boxed int64 handle_walltime wrote the OUT nanosecond time via Hc.set_walltime_nsecs -> Guest.set_u64 (int64); now_ns's Int64.of_float boxed an int64 per WALLTIME hypercall (19.4M x 16 B = 226 MB, the last per-op allocation on the bench once Mmio.write and Continue_read were fixed). A wall-clock time in nanoseconds fits a native int (< 2^62 for ~146 years), so now_ns is int_of_float and set_walltime_nsecs writes the 8-byte field as two little-endian 32-bit words with no int64. The fuzz masks its OUT value to 62 bits and expects that round-trip; it also gains its mli and the pp_/suite-name conventions. All solo5 tests pass. bench total 15.30 GB -> 19.84 MB across the session; every per-frame / per-hypercall / per-register path is now allocation-free.

3 weeks ago

solo5: write the walltime nsecs as two u32 words, not a boxed int64 handle_walltime wrote the OUT nanosecond time via Hc.set_walltime_nsecs -> Guest.set_u64 (int64); now_ns's Int64.of_float boxed an int64 per WALLTIME hypercall (19.4M x 16 B = 226 MB, the last per-op allocation on the bench once Mmio.write and Continue_read were fixed). A wall-clock time in nanoseconds fits a native int (< 2^62 for ~146 years), so now_ns is int_of_float and set_walltime_nsecs writes the 8-byte field as two little-endian 32-bit words with no int64. The fuzz masks its OUT value to 62 bits and expects that round-trip; it also gains its mli and the pp_/suite-name conventions. All solo5 tests pass. bench total 15.30 GB -> 19.84 MB across the session; every per-frame / per-hypercall / per-register path is now allocation-free.

3 weeks ago