Stream: general

Topic: interpreters which mirror structure of spec

nagisa (Aug 02 2022 at 10:40):

Does anybody know of any interpreters that closely follow the shape and structure of the specification? My goal is to pretty much use it as a reference implementation for some tests after modifying it with changes to the spec that I have in mind. I want to avoid missing implementation-specific details with the modifications, and so for that reason specifically it would be nice if the implementation was mirroring the spec as close to 1:1 as possible, including the instruction reduction mechanism used in the spec. As far as Rust implementations go, wain seems to fit the bill the best so far, but that implementation has chosen to eschew the reduction approach for the more straightforward loop { match { ... } }.

Chris Fallin (Aug 02 2022 at 16:20):

@nagisa the spec repository itself has the reference interpreter, which seems to be the best fit I can think of for your request; it's written in a way that basically mirrors the spec's reduction rules into OCaml

Chris Fallin (Aug 02 2022 at 16:21):

@Conrad Watt has done work to make it fast with a few tweaks (otherwise it has some unfortunate quadratic behavior) and we use that version as an oracle for fuzzing

Conrad Watt (Aug 02 2022 at 17:43):

just to add, you should _definitely_ use the unmodified reference interpreter if you can get away with it, rather than my fork, which contains code generated using a theorem prover and isn't really human-readable

nagisa (Aug 02 2022 at 17:49):

Yeah performance is of little concern in my case, integrability into a typical Rust crate’s test suite and ability to modify it is however. I think might be able to live with ocaml as a dep, but I’ll need to see if I can get up to speed with the impl reasonably quickly.

Robin Freyler (Aug 08 2022 at 13:49):

It would be pretty useful to have the OCaml based Wasm spec interpreter as a Rust crate on crates.io. I see it fruitful for things like fuzz testing Wasm validation and runtime execution against the Wasm spec interpreter.

Andrew Brown (Aug 08 2022 at 15:01):

@Hero Bird, with a little bit of work, the wasm-spec-interpreter crate in Wasmtime (here) could be adapted and published on crates.io. Are you interested in that?

Robin Freyler (Aug 08 2022 at 15:13):

@Andrew Brown If the BytecodeAlliance team appreciates the idea I'd definitely be interested in publishing the wasm-spec-interpreter to crates.io. I could really use this for wasmi. :)

Andrew Brown (Aug 08 2022 at 15:17):

Well I think it's a fine idea personally, I think there's a couple of things to figure out:

• should we move the code to a separate BA repository?
• who should have publication rights? (I think it would be great if you wanted to be the primary publisher but we might want to have some other BA maintainers there as well)
• the code probably needs a bit of tweaking: e.g., we probably want a way (Cargo feature?) to decide between using @Conrad Watt's interpreter and the reference interpreter, certainly more documentation is needed (esp. about build dependencies necessary for this to work), etc.

Andrew Brown (Aug 08 2022 at 15:18):

I will bring this up in the Cranelift meeting in a few minutes to see what people think

Robin Freyler (Aug 08 2022 at 15:22):

Okay thanks a lot for this information and thanks for bringing up the idea at the next Cranelift meeting! :)
I'd just make the BytecodeAlliance the publisher of the crate as with all other BytecodeAlliance crates. Please keep me updated about this.

Robin Freyler (Aug 08 2022 at 15:24):

Maybe having an issue where we can discuss this would be valuable once the decision for this idea has been made.

Conrad Watt (Aug 08 2022 at 15:31):

Sorry if I've misunderstood, but will this be discussed at the Wasmtime meeting on the 18th? I can dial in.

EDIT: ah, I guess I missed the relevant call, no worries :)

Andrew Brown (Aug 08 2022 at 15:33):

Sure, I can add it as an agenda topic for the Wasmtime meeting as well

Conrad Watt (Aug 08 2022 at 15:34):

btw, the version of the interpreter I maintain has a command line switch that lets you use the "original" interpreter definitions

Conrad Watt (Aug 08 2022 at 15:34):

so there wouldn't be a strict need for any further configuration on that front

Conrad Watt (Aug 08 2022 at 15:35):

(although maybe some work is needed in the top-level interpret.ml file of the crate to expose this)

Robin Freyler (Aug 08 2022 at 15:54):

Where can I find a link to @Conrad Watt 's interpreter. Is this interpreter also meant to be a spec reference implementation of Wasm?

Conrad Watt (Aug 08 2022 at 16:13):

link: https://github.com/conrad-watt/spec/tree/wasmtime_fuzzing/interpreter

its story is a little more complicated - the interpreter is based on a logical model of the spec written in the Isabelle theorem prover - the model is the "reference", and the interpreter isn't meant to be directly readable, but instead trusted because there's a proof that it's correct wrt the model

paper: https://vtss.doc.ic.ac.uk/publications/Watt2021Two.pdf

Conrad Watt (Aug 08 2022 at 16:15):

this approach means I can implement optimisations without breaking the "trust story"

Andrew Brown (Aug 08 2022 at 16:17):

Ok, here is the agenda topic for the 18th: https://github.com/bytecodealliance/meetings/pull/12. @Hero Bird, can you make it to that meeting as well?

Robin Freyler (Aug 08 2022 at 16:57):

@Conrad Watt Thanks for the link and explanations!
@Andrew Brown Never took part in such a meeting but I guess it is about time, right?

Conrad Watt (Aug 17 2022 at 20:18):

Unfortunately I've just found out that I'll only be able to join the meeting for the first 30 minutes. I'm very sorry about this, and if it turns out not to be enough time I'm happy to call/message anyone who's interested out-of-band.

Robin Freyler (Aug 18 2022 at 07:48):

@Andrew Brown Do I need to contact someone in order to participate in the meeting later or am I already signed up?

Andrew Brown (Aug 18 2022 at 13:20):

Not totally sure; perhaps contact @fitzgen (he/him)?

Robin Freyler (Aug 18 2022 at 13:23):

okay will do

Alex Crichton (Aug 18 2022 at 16:44):

I've created https://github.com/bytecodealliance/wasm-spec-interpreter for a repo here

Robin Freyler (Aug 19 2022 at 16:00):

Maybe I am just stupid but GitHub does not allow me to fork the repo or create a bare PR for it because the repo is empty.

Andrew Brown (Aug 19 2022 at 16:06):

I'll move the code there in a few minutes so we can get started...

Andrew Brown (Aug 19 2022 at 16:16):

@Robin Freyler, what is your GitHub handle?

Andrew Brown (Aug 19 2022 at 17:06):

never mind, I think I figured it out

Andrew Brown (Aug 19 2022 at 17:09):

@Robin Freyler, @Conrad Watt, @Alex Crichton: I could use some reviews on the setup of that repository, https://github.com/bytecodealliance/wasm-spec-interpreter/pulls. (Not sure what I did wrong in the CI infrastructure one because I thought it would run the CI even in the PR; maybe we need to merge it first to activate GitHub Actions?).

Alex Crichton (Aug 19 2022 at 17:10):

you'll need to merge to main to trigger CI on future PRs

Alex Crichton (Aug 19 2022 at 17:10):

CI added just in a PR for the first time doesn't trigger a run automatically

Last updated: Nov 22 2024 at 16:03 UTC