Skip to content

Commit 389f6cc

Browse files
dhilmlegoupilslindleytlively
authored
Reduction semantics (#109)
* Reduction semantics This patch populates the "Execution" section of the Explainer document with the reduction rules for stack switching. * Some type expansions * Fix minor typo, hdl => hdl1 * Fix typo: stray ' * Address Andreas' feedback * Remove stray ^ * Incorporated comments Incorporated comments from before The biggest thing I am unsure of is lines 814 and 826. This pertains to what point the tag argument of suspend and switch is translated into a tag address. Doing it in the reduction rule for resume (as was the case in the previous version of Explainer.md) is wrong, for reasons explained in the comment I wrote at the time. I believe I was told in the actual implementation, the change happens during the validation phase, which is why I propose these lines 814 and 826; however my phrasing can perhaps be improved. * rectified the suspend address translation to its correct place Incorporating Thomas Lively's comment, I have rectified the spot where suspend and switch translate the tag index into a tag address, by creating new instructions suspend.addr and switch.addr that take addresses (rather than indices) as arguments. This allows for a rule focused on translating suspend to suspend.addr (and likewise for switch), enforcing that the correct wasm frame F is used. * Update proposals/stack-switching/Explainer.md Co-authored-by: Thomas Lively <tlively123@gmail.com> * Fix resume_throw semantics * Update proposals/stack-switching/Explainer.md Committing tlively's suggested change Co-authored-by: Thomas Lively <tlively123@gmail.com> * Update proposals/stack-switching/Explainer.md Committing tlively's suggested change Co-authored-by: Thomas Lively <tlively123@gmail.com> * Applied all suggested changes except taguse Applied all suggested changes except taguse which is the last remaining issue * Added tag uses * using taguse in hdl too * factored typing rules and added keyword 'on' where now necessary * Typo in typing rule for tag addresses * corrected $a to $e and added switch failure rules --------- Co-authored-by: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Co-authored-by: Sam Lindley <Sam.Lindley@ed.ac.uk> Co-authored-by: Thomas Lively <tlively123@gmail.com>
1 parent 804a076 commit 389f6cc

1 file changed

Lines changed: 133 additions & 16 deletions

File tree

‎proposals/stack-switching/Explainer.md‎

Lines changed: 133 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -923,6 +923,15 @@ We change the wellformedness condition for tag types to be more liberal, i.e.
923923

924924
In other words, the return type of tag types is allowed to be non-empty.
925925

926+
We also introduce tag uses, which can be either tag indices or tag addresses:
927+
928+
- `taguse ::= tagidx | tagaddr`
929+
- `$e : [t1*] -> [t2*]`
930+
- iff `C.tags[$e] = tag $ft`
931+
- and `C.types[$ft] ~~ func [t1*] -> [t2*]`
932+
- `ea : [t1*] -> [t2*]`
933+
- iff `S.tags[ea].type ~~ func [t1*] -> [t2*]`
934+
926935
### Instructions
927936

928937
The new instructions and their validation rules are as follows. To simplify the presentation, we write this:
@@ -968,31 +977,27 @@ This abbreviation will be formalised with an auxiliary function or other means i
968977
- and `C.types[$ft] ~~ func [te*] -> []`
969978
- and `(hdl : t2*)*`
970979

971-
- `hdl = (on <tagidx> <labelidx>) | (on <tagidx> switch)`
980+
- `hdl = (on <taguse> <labelidx>) | (on <taguse> switch)`
972981
- Handlers attached to `resume` and `resume_throw`, handling control tags for `suspend` and `switch`, respectively.
973-
- `(on $e $l) : t*`
974-
- iff `C.tags[$e] = tag $ft`
975-
- and `C.types[$ft] ~~ func [t1*] -> [t2*]`
982+
- `(on tu $l) : t*`
983+
- iff `tu : [t1*] -> [t2*]`
976984
- and `C.labels[$l] = [t1'* (ref null? $ct)]`
977985
- and `t1* <: t1'*`
978986
- and `C.types[$ct] ~~ cont [t2'*] -> [t'*]`
979987
- and `[t2*] -> [t*] <: [t2'*] -> [t'*]`
980-
- `(on $e switch) : t*`
981-
- iff `C.tags[$e] = tag $ft`
982-
- and `C.types[$ft] ~~ func [] -> [t*]`
988+
- `(on tu switch) : t*`
989+
- iff `tu : [] -> [t*]`
983990

984-
- `suspend <tagidx>`
991+
- `suspend <taguse>`
985992
- Use a control tag to suspend the current computation.
986-
- `suspend $t : [t1*] -> [t2*]`
987-
- iff `C.tags[$t] = tag $ft`
988-
- and `C.types[$ft] ~~ func [t1*] -> [t2*]`
993+
- `suspend tu : [t1*] -> [t2*]`
994+
- iff `tu : func [t1*] -> [t2*]`
989995

990-
- `switch <typeidx> <tagidx>`
996+
- `switch <typeidx> <taguse>`
991997
- Switch to executing a given continuation directly, suspending the current execution.
992998
- The suspension and switch are performed from the perspective of a parent `(on $e switch)` handler, determined by the annotated control tag.
993-
- `switch $ct1 $e : [t1* (ref null $ct1)] -> [t2*]`
994-
- iff `C.tags[$e] = tag $ft`
995-
- and `C.types[$ft] ~~ func [] -> [t*]`
999+
- `switch $ct1 tu : [t1* (ref null $ct1)] -> [t2*]`
1000+
- iff `tu : [] -> [t*]`
9961001
- and `C.types[$ct1] ~~ cont [t1* (ref null? $ct2)] -> [te1*]`
9971002
- and `te1* <: t*`
9981003
- and `C.types[$ct2] ~~ cont [t2*] -> [te2*]`
@@ -1017,6 +1022,118 @@ events and only `(on $e switch)` handlers can handle `switch`
10171022
events. The handler search continues past handlers for the wrong kind
10181023
of event, even if they use the correct tag.
10191024

1025+
#### Store extensions
1026+
1027+
* New store component `conts` for allocated continuations
1028+
- `S ::= {..., conts <continst>?*}`
1029+
1030+
* A continuation is a context annotated with its hole's arity
1031+
- `continst ::= (E : n)`
1032+
1033+
1034+
#### Administrative instructions
1035+
1036+
* `(ref.cont a)` represents a continuation value, where `a` is a *continuation address* indexing into the store's `conts` component
1037+
- `ref.cont a : [] -> [(ref $ct)]`
1038+
- iff `S.conts[a] = epsilon \/ S.conts[a] = (E : n)`
1039+
+ iff `E[val^n] : t2*`
1040+
+ and `(val : t1)^n`
1041+
- and `$ct ~~ cont $ft`
1042+
- and `$ft ~~ [t1^n] -> [t2*]`
1043+
1044+
* `(prompt{<hdl>*} <instr>* end)` represents an active handler
1045+
- `(prompt{hdl*}? instr* end) : [] -> [t*]`
1046+
- iff `instr* : [] -> [t*]` in the empty context
1047+
- and `(hdl : [t*])*`
1048+
1049+
#### Handler contexts
1050+
1051+
```
1052+
H^ea ::=
1053+
_
1054+
val* H^ea instr*
1055+
label_n{instr*} H^ea end
1056+
frame_n{F} H^ea end
1057+
catch{...} H^ea end
1058+
prompt{hdl*} H^ea end (iff ea notin hdl*)
1059+
```
1060+
1061+
1062+
#### Reduction
1063+
1064+
* `S; F; (ref.null t) (cont.new $ct) --> S; F; trap`
1065+
1066+
* `S; F; (ref.func fa) (cont.new $ct) --> S'; F; (ref.cont |S.conts|)`
1067+
- iff `S' = S with conts += (E : n)`
1068+
- and `E = _ (invoke fa)`
1069+
- and `$ct ~~ cont $ft`
1070+
- and `$ft ~~ [t1^n] -> [t2*]`
1071+
1072+
* `S; F; (ref.null t) (cont.bind $ct $ct') --> S; F; trap`
1073+
1074+
* `S; F; (ref.cont ca) (cont.bind $ct $ct') --> S; F; trap`
1075+
- iff `S.conts[ca] = epsilon`
1076+
1077+
* `S; F; v^n (ref.cont ca) (cont.bind $ct $ct') --> S'; F; (ref.cont |S.conts|)`
1078+
- iff `S.conts[ca] = (E' : n')`
1079+
- and `$ct' ~~ cont $ft'`
1080+
- and `$ft' ~~ [t1'*] -> [t2'*]`
1081+
- and `n = n' - |t1'*|`
1082+
- and `S' = S with conts[ca] = epsilon with conts += (E : |t1'*|)`
1083+
- and `E = E'[v^n _]`
1084+
1085+
* `S; F; (ref.null t) (resume $ct hdl*) --> S; F; trap`
1086+
1087+
* `S; F; (ref.cont ca) (resume $ct hdl*) --> S; F; trap`
1088+
- iff `S.conts[ca] = epsilon`
1089+
1090+
* `S; F; v^n (ref.cont ca) (resume $ct hdl*) --> S'; F; prompt{hdl'*} E[v^n] end`
1091+
- iff `S.conts[ca] = (E : n)`
1092+
- and `S' = S with conts[ca] = epsilon`
1093+
- and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]`
1094+
1095+
* `S; F; (ref.null t) (resume_throw $ct $e hdl*) --> S; F; trap`
1096+
1097+
* `S; F; (ref.cont ca) (resume_throw $ct $e hdl*) --> S; F; trap`
1098+
- iff `S.conts[ca] = epsilon`
1099+
1100+
* `S; F; v^m (ref.cont ca) (resume_throw $ct $e hdl*) --> S''; F; prompt{hdl'*} E[(ref.exn |S'.exns|) throw_ref] end`
1101+
- iff `S.conts[ca] = (E : n)`
1102+
- and `ta = S.tags[F.module.tags[$e]]`
1103+
- and `ta.type ~~ [t1^m] -> [t2*]`
1104+
- and `S' = S with exns += {ta, v^m}`
1105+
- and `S'' = S' with conts[ca] = epsilon`
1106+
- and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]`
1107+
1108+
* `S; F; (prompt{hdl*} v* end) --> S; F; v*`
1109+
1110+
* `S; F; (suspend $e) --> S; F; (suspend ea)`
1111+
- iff `ea = F.module.tags[$e]`
1112+
1113+
* `S; F; (prompt{hdl1* (on ea $l) hdl2*} H^ea[v^n (suspend ea)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)`
1114+
- iff `forall $l', (on ea $l') notin hdl1*`
1115+
- and `S.tags[ea].type ~~ [t1^n] -> [t2^m]`
1116+
- and `S' = S with conts += (H^ea : m)`
1117+
1118+
* `S; F; (switch $ct $e) --> S; F; (switch $ct ea)`
1119+
- iff `ea = F.module.tags[$e]`
1120+
1121+
* `S; F; (ref.null t) (switch $ct ea) --> S; F; trap`
1122+
1123+
* `S; F; (ref.cont ca) (switch $ct ea) --> S; F; trap`
1124+
- iff `S.conts[ca] = epsilon`
1125+
1126+
* `S; F; (prompt{hdl1* (on ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch $ct ea)] end) --> S''; F; prompt{hdl1* (on ea switch) hdl2*} E[v^n (ref.cont |S.conts|)] end`
1127+
- iff `S.conts[ca] = (E : n')`
1128+
- and `n' = 1 + n`
1129+
- and `(on switch ea) notin hdl1*`
1130+
- and `$ct ~~ cont $ft`
1131+
- and `$ft ~~ [t1* (ref $ct2)] -> [t2*]`
1132+
- and `$ct2 ~~ cont $ft2`
1133+
- and `$ft2 ~~ [t1'^m] -> [t2'*]`
1134+
- and `S' = S with conts[ca] = epsilon`
1135+
- and `S'' = S' with conts += (H^ea : m)`
1136+
10201137
### Binary format
10211138

10221139
We extend the binary format of composite types, heap types, and instructions.
@@ -1040,7 +1157,7 @@ The opcode for heap types is encoded as an `s33`.
10401157

10411158
#### Instructions
10421159

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

10451162
| Opcode | Instruction | Immediates |
10461163
| ------ | ------------------------ | ---------- |

0 commit comments

Comments
 (0)