Skip to content

Reduction semantics #109

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.

Sign up for GitHub

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

Open
wants to merge 6 commits into
base: main
Choose a base branch
from
Open

Reduction semantics #109

Changes from 4 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
9ad8d55
Reduction semantics
dhil Jan 22, 2025
db96405
Some type expansions
dhil Jan 22, 2025
2330933
Fix minor typo, hdl => hdl1
dhil Jan 22, 2025
d8ad9ed
Fix typo: stray '
dhil Jan 22, 2025
79e59f6
Address Andreas' feedback
dhil Feb 6, 2025
d7e176d
Remove stray ^
dhil Feb 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
122 changes: 121 additions & 1 deletion proposals/stack-switching/Explainer.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -833,6 +833,126 @@ events and only `(on $e switch)` handlers can handle `switch`
events. The handler search continues past handlers for the wrong kind
of event, even if they use the correct tag.

#### Store extensions

* A store component `tags` for allocated tags (from the exception
handling proposal)
- `S ::= {..., tags <taginst>*}`

* A *tag instance* represents a control tag (from the exception
handling proposal)
- `taginst ::= {type <tagtype>}`

* New store component `conts` for allocated continuations
- `S ::= {..., conts <cont>?*}`

* A continuation is a context annotated with its hole's arity
- `cont ::= (E : n)`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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*)).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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



#### Administrative instructions

* `(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)`
- and `$ct ~~ cont $ft`
- and `$ft ~~ [t1^n] -> [t2*]`
Copy link
Member

@rossberg rossberg Jan 22, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member

@rossberg rossberg Jan 22, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


* `(prompt{<hdl>*} <instr>* end)` represents an active handler
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

- `(prompt{((a $l) | (b switch))*}? instr* end) : [t1*] -> [t2*]`
- iff `instr* : [t1*] -> [t2*]`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

- and `(S.tags[a].type ~~ [te1*] -> [te2*])*`
- and `(S.tags[b].type ~~ [] -> [te2*])*`
- and `(label $l : [te1'* (ref null? $ct')])*`
- and `([te1*] <: [te1'*])*`
- and `($ct' ~~ cont $ft')*`
- and `([te2*] -> [t2*] <: $ft')*`

The administrative structure `hdl` is defined as.
```
hdl ::= (<tagaddr> $l) hdl | (<tagaddr> switch)
```

#### Handler contexts

```
H^ea ::=
_
val* H^ea instr*
label_n{instr*} H^ea end
frame_n{F} H^ea end
catch{...} H^ea end
prompt{hdl*} H^ea end (iff ea notin ea'*)
```


#### Reduction

* `S; F; (ref.null t) (cont.new $ct) --> S; F; trap`

* `S; F; (ref.func fa) (cont.new $ct) --> S'; F; (ref.cont |S.conts|)`
- iff `S' = S with conts += (E : n)`
- and `E = _ (invoke fa)`
- and `$ct ~~ cont $ft`
- and `$ft ~~ [t1^n] -> [t2*]`

* `S; F; (ref.null t) (cont.bind $ct $ct') --> S; F; trap`

* `S; F; (ref.cont ca) (cont.bind $ct $ct') --> S; F; trap`
- iff `S.conts[ca] = epsilon`

* `S; F; v^n (ref.cont ca) (cont.bind $ct $ct') --> S'; F; (ref.const |S.conts|)`
- iff `S.conts[ca] = (E' : n')`
- and `$ct' ~~ cont $ft'`
- and `$ft' ~~ [t1'*] -> [t2'*]`
- and `n = n' - |t1'*|`
- and `S' = S with conts[ca] = epsilon with conts += (E : |t1'*|)`
- and `E = E'[v^n _]`

* `S; F; (ref.null t) (resume $ct (on $e $l)*) --> S; F; trap`

* `S; F; (ref.cont ca) (resume $ct (on $e $l)*) --> S; F; trap`
- iff `S.conts[ca] = epsilon`

* `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 `(ea = F.tags[$t])*`
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Something is missing here. Neither ea* nor $t* are bound. Moreover, the defined syntax of hdl on the l.h.s. and r.h.s. is different, i.e., there's a meta type mismatch.

I'd suggest to unify the syntax of hdl for resume and prompt by having it contain a taguse. Analogous to a typeuse, that is statically a tagidx, but is internally extended to also allow a tagaddr. Then the hdl on the r.h.s. can be obtained from the hdl on the l.h.s. by substituting the $t* by the ea* looked up in the frame.

- and `S' = S with conts[ca] = epsilon`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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; (ref.null t) (resume_throw $ct $e (on $t $l)*) --> S; F; trap`

* `S; F; (ref.cont ca) (resume_throw $ct $e (on $t $l)*) --> S; F; trap`
- iff `S.conts[ca] = epsilon`

* `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 `(ea = F.tags[$t])*`
- and `S.tags[F.tags[$e]].type ~~ [t1^m] -> [t2*]`
- and `S' = S with conts[ca] = epsilon`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same comment as for resume: the list hdl must be desugared using F.tags


* `S; F; (prompt{(e $l)*}? v* end) --> S; F; v*`

* `S; F; (prompt H^ea[(suspend $e)] end) --> S; F; trap`
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks like this rule was for barrier, so is obsolete?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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*`
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
- iff `ea notin ea1*`
- iff `ea notin tagaddr(hdl1*)`

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We also need to make sure ea isn't handled by H^ea.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't that the very definition of H^ea?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe. Though, it isn't defined in the document currently as far as I can tell.

- and `ea = F.tags[$e]`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

- and `S.tags[ea].type ~~ [t1^n] -> [t2^m]`
- and `S' = S with conts += (H^ea : m)`

* `S; F; (prompt{hdl1* (ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch $ct $e)] end) --> S''; F; prompt{hdl1* (ea switch) hdl2*} E[v^n (ref.cont |S.conts|)] end`
- iff `S.conts[ca] = (E : n')`
- and `n' = 1 + n`
- and `ea notin ea1*`
- and `ea = F.tags[$e]`
- and `$ct ~~ cont $ft`
- and `$ft ~~ [t1* (ref $ct2)] -> [t2*]`
- and `$ct2 ~~ cont $ft2`
- and `$ft2 ~~ [t1'^m] -> [t2'*]`
- and `S' = S with conts[ca] = epsilon`
- and `S'' = S' with conts += (H^ea : m)`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


### Binary format

We extend the binary format of composite types, heap types, and instructions.
Expand All @@ -856,7 +976,7 @@ The opcode for heap types is encoded as an `s33`.

#### Instructions

We use the use the opcode space `0xe0-0xe5` for the seven new instructions.
We use the use the opcode space `0xe0-0xe5` for the six new instructions.

| Opcode | Instruction | Immediates |
| ------ | ------------------------ | ---------- |
Expand Down