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
+118 −1
Open

Reduction semantics #109

Changes from all 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
119 changes: 118 additions & 1 deletion proposals/stack-switching/Explainer.md
View file
Original file line number Diff line number Diff line change
@@ -833,6 +833,123 @@ 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

* 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)`
+ iff `E[val^n] : t2*`
Copy link

Choose a reason for hiding this comment

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

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.

Copy link
Member

Choose a reason for hiding this comment

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

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

+ and `(val : t1)^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{hdl*}? instr* end) : [t1*] -> [t2*]`
Copy link

Choose a reason for hiding this comment

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

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.

Copy link
Member

Choose a reason for hiding this comment

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

You're correct, it's always empty, just like for other administrative block instructions.

- 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 `(hdl : [t2*])*`

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

Choose a reason for hiding this comment

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

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

Copy link
Member

Choose a reason for hiding this comment

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

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.


where

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

* `(a switch)` represents a tag-switch association
- `(a switch)` and `(S.tags[b].type ~~ [] -> [te2*])*`
Copy link

Choose a reason for hiding this comment

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

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…

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. It is a typo/mistake. It should be the trivial typing rule as you noted.


#### 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 tagaddr(hdl*))
```


#### 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 `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 `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{hdl*} v* end) --> S; F; v*`

* `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]`
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 tagaddr(hdl1*)`
- 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.
@@ -856,7 +973,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 |
| ------ | ------------------------ | ---------- |