Stream: git-wasmtime

Topic: wasmtime / PR #7219 PCC: add basic "memory types".


view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 18:17):

cfallin requested elliottt for a review on PR #7219.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 18:17):

cfallin requested wasmtime-compiler-reviewers for a review on PR #7219.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 18:17):

cfallin requested fitzgen for a review on PR #7219.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 18:17):

cfallin opened PR #7219 from cfallin:pcc-memcap to bytecodealliance:main:

This PR adds a notion of "memory types" to the PCC (proof-carrying code) framework. To borrow a doc-comment:

A memory type is a struct-like definition -- fields with offsets, each field having a type and possibly an attached fact -- that we can use in proof-carrying code to validate accesses to structs and propagate facts onto the loaded values as well.

Memory types are meant to be rich enough to describe the layout of values in memory, but do not necessarily need to embody higher-level features such as subtyping directly. Rather, they should encode an implementation of a type or object system.

Note also that it is a non-goal for now for this type system to be "complete" or fully orthogonal: we have some restrictions now (e.g., struct fields are only primitives) because this is all we need for existing PCC applications, and it keeps the implementation simpler.

While developing this, we originally sketched out a more complete type-system that had arrays, allowed struct fields to be memory types themselves, and was in general more flexible. However, the possibility of cycles, non-statically-sized types, etc., was getting overly complex and I decided to YAGNI-simplify a bit for now. The Doc-comment on the module does sketch out what other types will be needed, and I think those plus a GV-bounded max fact will be enough to express PCC facts for all static and dynamic memories and table accesses in Wasmtime. (A partial further development of the more complete system, with some more validator checks for cycles, etc., is on this WIP branch.)

Part of this change was

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 18:17):

cfallin requested wasmtime-core-reviewers for a review on PR #7219.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 20:22):

fitzgen submitted PR review:

r=me with nitpick-y suggestions that you can take or leave but also a more important point about a git submodule that should definitely be addressed before landing

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 20:22):

fitzgen submitted PR review:

r=me with nitpick-y suggestions that you can take or leave but also a more important point about a git submodule that should definitely be addressed before landing

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 20:22):

fitzgen created PR review comment:

I don't think this change to the wasi-nn spec submodule was intended was it?

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 20:22):

fitzgen created PR review comment:

I don't think it matters if function names are duplicated but worth making sure

function %simple2(i64 vmctx, i32) -> i8 {

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 20:22):

fitzgen created PR review comment:

Note for the future that wasm gc will also require nullability, which almost but doesn't quite fit into the idea of discriminant tags.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 20:22):

fitzgen created PR review comment:

This could be

                ensure!(
                    self.memory_types[*ty].size().map_or(false, |s| end_offset <= s),
                    OutOfBounds
                );

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:15):

cfallin updated PR #7219.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:19):

cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:19):

cfallin created PR review comment:

Added another note for this in the doc-comment!

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:19):

cfallin updated PR #7219.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:19):

cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:19):

cfallin created PR review comment:

I thought a bit about this, but I think on balance I like the current form better, as we'll need to go back to it once we have dynamic limits.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:19):

cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:19):

cfallin created PR review comment:

Fixed!

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:19):

cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:19):

cfallin created PR review comment:

Ah, yes, unintended from a missed git submodule update; rebased out!

view this post on Zulip Wasmtime GitHub notifications bot (Oct 11 2023 at 23:20):

cfallin has enabled auto merge for PR #7219.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 12 2023 at 00:44):

cfallin merged PR #7219.


Last updated: Nov 22 2024 at 16:03 UTC