avanhatt opened PR #9178 from wellesley-prog-sys:upstream-08-28
to bytecodealliance:main
:
Draft PR to upstream the ongoing ISLE verification work, as described in our ASPLOS 2024 paper: Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection. The motivation for this work is described in detail in the paper.
Using the tool is described in detail at cranelift/isle/veri/README.md.
Alternatives considered
We could continue to develop this work in a fork, but that runs the risk of becoming quickly out-of-date. In discussions with @cfallin, @fitzgen, and @jameysharp, we have designed the specifications and verification to sit alongside the ISLE source.
However, we have also discussed delaying the upstreaming effort to instead upstream the newer version under development by @mmcloughlin. But, this version is much further from having the coverage of the original prototype.
avanhatt updated PR #9178.
cfallin requested cfallin for a review on PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
alexcrichton commented on PR #9178:
@avanhatt for the deny/vet CI errors I have two commits at https://github.com/alexcrichton/wasmtime/commits/verifier which should resolve the issues.
- https://github.com/alexcrichton/wasmtime/commit/9c546728430b161a658e998d9a6decfdad2f0d7e - this undoes what looks like a
cargo update
that may have been performed during development? If you need the updates though let me know and we can try to get that working. That fixes bothcargo deny
andcargo vet
- https://github.com/alexcrichton/wasmtime/commit/f8e5f3e4cbfc163e1a274e829b27987bb2df8f0b - this flags the two new crates as
publish = false
to fix integration with the auto-publish workflow that we have. If you want these crates published though just let me know and I can help out with that tooNo need to preserve authorship on those, feel free to include the commits here however's easiest to you!
avanhatt updated PR #9178.
avanhatt commented on PR #9178:
@avanhatt for the deny/vet CI errors I have two commits at https://github.com/alexcrichton/wasmtime/commits/verifier which should resolve the issues.
@alexcrichton thanks so much for the help with these, passing all checks now!
avanhatt has marked PR #9178 as ready for review.
avanhatt requested wasmtime-compiler-reviewers for a review on PR #9178.
avanhatt requested wasmtime-default-reviewers for a review on PR #9178.
Last updated: Dec 23 2024 at 12:05 UTC