Reduction semantics #109
Reduction semantics #109
Conversation
This patch populates the "Execution" section of the Explainer document with the reduction rules for stack switching.
| - `ref.cont a : [] -> [(ref $ct)]` | ||
| - iff `S.conts[a] = epsilon \/ S.conts[a] = (E : n)` | ||
| - and `$ct ~~ cont $ft` | ||
| - and `$ft ~~ [t1^n] -> [t2*]` |
There was a problem hiding this comment.
This would also need to require that E returns t2*. I think we want to factor both out into a separate typing rule for continuations, which is just invoked here. That rule would be something like
(E : n) : t1^n → t2*
- iff s ⊢ E[val^n] : t2*
- and (s ⊢ val : t1)^n
There was a problem hiding this comment.
Doesn't:
S.conts[a] = epsilon / ...
allow for the possibility that the store does not contain the referenced continuation?
Do we want to allow that?
There was a problem hiding this comment.
Ah, no, empty isn't the same as being undefined. This says that S.conts[a] maps to the empty (i.e. dead) continuation. If S.conts does not contain a at all (i.e., is shorter than a), then the expression S.conts[a] is not even defined, and the whole rule becomes inapplicable as a consequence. IOW, the use of such an expression implies that the index must be in range.
|
|
||
| * `S; F; (prompt{(e $l)*}? v* end) --> S; F; v*` | ||
|
|
||
| * `S; F; (prompt H^ea[(suspend $e)] end) --> S; F; trap` |
There was a problem hiding this comment.
It looks like this rule was for barrier, so is obsolete?
There was a problem hiding this comment.
Yes, I think you are right. Though, shouldn't we have a rule that specifies when suspend traps? E.g. S; F; suspend $e --> S; F; trap?
There was a problem hiding this comment.
The rest of the wasm semantics is modular, e.g. if es --> es' then H[es] --> H[es'] for any context H. If we add a rule suspend $e --> trap, we break that modularity (placing under an appropriate context, the suspension can be handled instead of trapping). In other words, there is no guarantee that any given reduction rule will be applied at top-level, so I don't think it is a good idea to introduce this rule.
| - iff `ea = F.tags[$e]` | ||
|
|
||
| * `S; F; (prompt{hdl1* (ea $l) hdl2*} H^ea[v^n (suspend $e)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)` | ||
| - iff `ea notin ea1*` |
There was a problem hiding this comment.
| - iff `ea notin ea1*` | |
| - iff `ea notin tagaddr(hdl1*)` |
There was a problem hiding this comment.
We also need to make sure ea isn't handled by H^ea.
There was a problem hiding this comment.
Isn't that the very definition of H^ea?
There was a problem hiding this comment.
Maybe. Though, it isn't defined in the document currently as far as I can tell.
There was a problem hiding this comment.
Most of these comments are either
(1) those already discussed on zoom on the 6th of February
(2) sidenotes about small insignificant differences between this and the Iris-WasmFX mechanisation. I do not think it is necessary to incorporate these comments into the explainer document but I figured I would share these details.
The main exception is the comment on line 856 which might well require our attention.
|
|
||
| * `(prompt{<hdl>*} <instr>* end)` represents an active handler | ||
| - `(prompt{hdl*}? instr* end) : [t1*] -> [t2*]` | ||
| - iff `instr* : [t1*] -> [t2*]` |
There was a problem hiding this comment.
This explanation does not mention what typing context is used. Here, the body instr* of the prompt instruction should be typechecked under the empty context. This enforces that its body is closed, which is necessary since continuations live in the store and store objects should be closed.
| The administrative structure `hdl` is defined as | ||
| ``` | ||
| hdl ::= (<tagaddr> $l) | (<tagaddr> switch) | ||
| ``` |
There was a problem hiding this comment.
The resume instruction needs a list of tags, and prompt needs a list of (desugared) tag addresses. Hence we need to either define two separate notions hdl and hdlnew where hdl is as shown above and is used by prompt and hdlnew has tags instead of tag addresses and is used by resume; or we can keep one single hdl and allow it to either take tags or tag addresses as inputs. The former is the solution adopted by the Iris-WasmFX mechanisation
There was a problem hiding this comment.
Even if we define this as a separate syntactic class, I'd suggest to mirror the syntax of the index-based notation, i.e., keep the on.
|
|
||
| * `S; F; v^n (ref.cont ca) (resume $ct hdl*) --> S'; F; prompt{hdl*} E[v^n] end` | ||
| - iff `S.conts[ca] = (E : n)` | ||
| - and `S' = S with conts[ca] = epsilon` |
There was a problem hiding this comment.
hdl must be desugared here: on the LHS it contains tags and on the RHS it should contain tag addresses. The field F.tags in the frame converts one to the other.
| * `S; F; v^m (ref.cont ca) (resume_throw $ct $e hdl*) --> S'; F; prompt{hdl*} E[v^m (throw $e)] end` | ||
| - iff `S.conts[ca] = (E : n)` | ||
| - and `S.tags[F.tags[$e]].type ~~ [t1^m] -> [t2*]` | ||
| - and `S' = S with conts[ca] = epsilon` |
There was a problem hiding this comment.
Same comment as for resume: the list hdl must be desugared using F.tags
|
|
||
| * `S; F; (prompt{hdl1* (ea $l) hdl2*} H^ea[v^n (suspend $e)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)` | ||
| - iff `ea notin tagaddr(hdl1*)` | ||
| - and `ea = F.tags[$e]` |
There was a problem hiding this comment.
This is wrong, F is not always the right frame to use; instead the innermost frame in H should be used (in case H contains nested frame instructions). I can suggest two solutions. The first is to write a function innermost_frame that explores H and returns the innermost frame F_i from the innermost frame instruction in H; if no frame instruction is found, the function should return F (the current top-level frame). I find this tedious. The second solution is have two instructions suspend and suspend_desugared, the first taking a tag $e as an immediate argument, the second taking a tag address ea as an argument. Then the rule above should mention suspend_desugared ea instead of suspend $e, and we would need to add a reduction rule that reduces S; F; suspend $e --> S; F; suspend_desugared ea when F.tags[$e] = ea, conveniently using the closest frame F without needing to define a function that explores the context. For simplicity, we can also consider using a single instruction suspend that can take both a tag or a tag address as an immediate argument instead of two separate instructions. The Iris-WasmFX mechanisation uses two instructions as it is convenient to consider suspend as a basic instruction and suspend_desugared as an administrative instruction.
| * `(ref.cont a)` represents a continuation value, where `a` is a *continuation address* indexing into the store's `conts` component | ||
| - `ref.cont a : [] -> [(ref $ct)]` | ||
| - iff `S.conts[a] = epsilon \/ S.conts[a] = (E : n)` | ||
| + iff `E[val^n] : t2*` |
There was a problem hiding this comment.
There are two ways of doing this. The first is the one displayed here, where type-checking the ref.cont instructions requires typechecking the body of the continuation here and now. The other one (which is the one used in the Iris-WasmFX mechanisation) is to merely read a type annotation here; and instead add a clause to the (unshown here) store_typing predicate that describes a well-formed state, mandating that all continuations in the store must have a body that type-checks. From a theoretical point of view, I prefer the second solution. Besides, the second approach is the one used when typechecking the invoke administrative instruction.
There was a problem hiding this comment.
Hm, I'd generally prefer the first option, since that is a more faithful reflection of the intended runtime representation that erases these types. We really want to know that this is sound, so ideally, even a mechanised soundness proof would model the store without introducing additional type information that may affect the result in subtle ways.
Invoke is different in that functions are already type-annotated in the source program, and these types are in fact kept around in real implementations (e.g., to perform link-time type-checks).
| - `S ::= {..., conts <cont>?*}` | ||
|
|
||
| * A continuation is a context annotated with its hole's arity | ||
| - `cont ::= (E : n)` |
There was a problem hiding this comment.
Sidenote: the Iris-WasmFX mechanisation stores more than just the arity n together with the context E, it stores the actual expected type t1* -> t2*. Transforming the presentation from the mechanisation to this one is simple (n = length(t1*)).
There was a problem hiding this comment.
That is interesting. Is that merely for convenience (i.e., not having to guess the type non-deterministically in the proof), or would soundness actually break without fixing the types?
There was a problem hiding this comment.
This is so that the logical relation can later have more to go on. The type soundness could be proved in a mechanisation that only decorates contexts with the arity n with minor changes to the proofs
| - and `$ct ~~ cont $ft` | ||
| - and `$ft ~~ [t1^n] -> [t2*]` | ||
|
|
||
| * `(prompt{<hdl>*} <instr>* end)` represents an active handler |
There was a problem hiding this comment.
Sidenote: the Iris-WasmFX mechanisation adds one more immediate argument to the prompt instruction: the type t* expected for the body <instr>*. This is necessary to define the behaviour of the suspend instruction since the mechanisation stores each continuation together with its expected type t1* -> t2*. If the type annotation was not present in the prompt instruction, it would be impossible to know the return type t2* of the captured continuation when reducing suspend. It is easy to transform the presentation from the mechanisation into this one (just forget the type annonation).
| - and `$ft ~~ [t1^n] -> [t2*]` | ||
|
|
||
| * `(prompt{<hdl>*} <instr>* end)` represents an active handler | ||
| - `(prompt{hdl*}? instr* end) : [t1*] -> [t2*]` |
There was a problem hiding this comment.
Can [t1*] be non-empty? In the Iris-WasmFX mechanisation, this list is always empty… There is a mistake either here or in the mechanisation.
There was a problem hiding this comment.
You're correct, it's always empty, just like for other administrative block instructions.
| - and `$ct2 ~~ cont $ft2` | ||
| - and `$ft2 ~~ [t1'^m] -> [t2'*]` | ||
| - and `S' = S with conts[ca] = epsilon` | ||
| - and `S'' = S' with conts += (H^ea : m)` |
There was a problem hiding this comment.
Sidenote: the Iris-WasmFX mechanisation does not yet have the switch instruction. I will add it shortly, but cannot at present comment on this reduction rule. However on a first glance, it appears that this reduction rule might suffer from the same issue as the suspend rule: the tag $e should be desugared not with frame F but the innermost frame of H.
There was a problem hiding this comment.
Update: the Iris-WasmFX mechanisation now has the switch instruction and type soundness has been proven. The issue using the correct frame when desugaring $e is indeed present
| - and `([te2*] -> [t2*] <: $ft')*` | ||
|
|
||
| * `(a switch)` represents a tag-switch association | ||
| - `(a switch)` and `(S.tags[b].type ~~ [] -> [te2*])*` |
There was a problem hiding this comment.
These two lines make no sense, perhaps it was meant "(a switch) : [t2*] iff S.tags[a].type ~~ [] -> [t2*]"? I'm not sure what the typing rule is meant to be…
There was a problem hiding this comment.
Yes. It is a typo/mistake. It should be the trivial typing rule as you noted.
| - and `$ct2 ~~ cont $ft2` | ||
| - and `$ft2 ~~ [t1'^m] -> [t2'*]` | ||
| - and `S' = S with conts[ca] = epsilon` | ||
| - and `S'' = S' with conts += (H^ea : m)` |
There was a problem hiding this comment.
What happens if the first instance of ea in hdl* is of the wrong form (i.e. ea switch for the suspend instruction, or ea $l for the switch instruction)? Does it then reduce to trap? Perhaps we should add a rule in the explainer
There was a problem hiding this comment.
No trap. We always pick the first match (left to right). Any later instances are effectively shadowed. ea $l are not relevant since we are looking for a switch handler, so they are simply skipped.
You are right that this behaviour should be mentioned in the explainer, if it isn't already.
There was a problem hiding this comment.
I am a little confused.
Imagine I have a switch instruction that targets the tag address ea. If I am under a prompt that has a single clause ea $l targeting the same tag address but is of the wrong kind (ea $l instead of ea switch). You are saying this doesn't count and I should just look upstream for a higher-encompassing prompt that has a ea switch clause? In that case the definition of H^ea[e] needs to be amended, because right now H^ea[e] explicitly forbids going upstream if a clause mentions ea, no matter if it mentions it as ea $l or ea switch.
Or is there something enforcing that anywhere a ea $l clause is present, a ea switch clause must be present alongside it?
There was a problem hiding this comment.
Yes you are correct. I think it is already mentioned in the explainer somewhere, at least informally, that (ea $l) and (ea switch) live in two different spaces. The former can only be matched by a suspend whereas the latter can only be matched by a switch.
| - and `$ct2 ~~ cont $ft2` | ||
| - and `$ft2 ~~ [t1'^m] -> [t2'*]` | ||
| - and `S' = S with conts[ca] = epsilon` | ||
| - and `S'' = S' with conts += (H^ea : m)` |
There was a problem hiding this comment.
Update: the Iris-WasmFX mechanisation now has the switch instruction and type soundness has been proven. The issue using the correct frame when desugaring $e is indeed present
This patch populates the "Execution" section of the Explainer document with the reduction rules for stack switching.
Resolves #91.