-
Notifications
You must be signed in to change notification settings - Fork 1.3k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
PCC: support x86-64. #7352
PCC: support x86-64. #7352
Conversation
This PR extends the proof-carrying-code infrastructure to support x86-64 as well as aarch64. In the process, many of the mechanisms had to be made a little more general. One important change is that the PCC leaves more "breadcrumbs" on the frontend now, avoiding the need for magic handling of facts on constant values, etc., in the backend. For the first time a lowering rule also gains the ability to add a fact to a vreg to preserve the chain as well. With these changes, we can validate compilation of SpiderMonkey.wasm with Wasm static memories on x86-64 and aarch64: ``` cfallin@fastly2:~/work/wasmtime% target/release/wasmtime compile -C pcc=yes --target x86_64 ../wasm-tests/spidermonkey.wasm cfallin@fastly2:~/work/wasmtime% target/release/wasmtime compile -C pcc=yes --target aarch64 ../wasm-tests/spidermonkey.wasm cfallin@fastly2:~/work/wasmtime% ```
…fairly expensive.
A performance measurement, also:
or in other words, ~1% overhead. Prior to this PR, turning on PCC automatically enabled the regalloc checker as well; I found this to have much higher overhead:
or about 68% above just PCC. Given that, IMHO a good design tradeoff point is to run PCC in production, but not the regalloc checker; we already fuzz continuously with the latter. It can always be turned on explicitly. |
An inquisitive member of the peanut gallery would like to know if you have written anything high-level about your goals for this work? I've seen the PRs flying by and it sounds really cool, but I don't understand any of the context. In particular, I've been wondering:
|
@jeffparsons great questions! I haven't written anything beyond the initial issue proposing this work in #6090 -- the last section of that issue writeup describes the proof-carrying code / "memory capabilities" model. I plan to write more eventually. The goal doesn't have anything to do with perf -- the generated code doesn't change, and this doesn't allow any more aggressive strategies to be used -- but rather, risk mitigation. We've had a few CVEs that have allowed sandbox escapes from Wasmtime due to miscompiles, and so I want to build infrastructure that does translation validation to prove a given compilation artifact doesn't have such an issue. Long-term, it could also be used to verify other invariants (e.g., @fitzgen and I have talked a bit about how it could be used to provide additional safety in the implementation of Wasm GC). |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice!!
A few comments below.
… explicitly match every instruction kind.
I reworked the whole PCC implementation for x64 based on the above feedback -- removing the ability to pattern-match into |
This PR extends the proof-carrying-code infrastructure to support x86-64 as well as aarch64. In the process, many of the mechanisms had to be made a little more general.
One important change is that the PCC leaves more "breadcrumbs" on the frontend now, avoiding the need for magic handling of facts on constant values, etc., in the backend. For the first time a lowering rule also gains the ability to add a fact to a vreg to preserve the chain as well.
With these changes, we can validate compilation of SpiderMonkey.wasm with Wasm static memories on x86-64 and aarch64: