From 9ad8d551b9c68465e1d64fb0a8c0aee5359e8680 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 22 Jan 2025 10:17:00 +0000 Subject: [PATCH 01/18] Reduction semantics This patch populates the "Execution" section of the Explainer document with the reduction rules for stack switching. --- proposals/stack-switching/Explainer.md | 122 ++++++++++++++++++++++++- 1 file changed, 121 insertions(+), 1 deletion(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 152aef33..e2896ed7 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -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 *}` + +* A *tag instance* represents a control tag (from the exception + handling proposal) + - `taginst ::= {type }` + +* New store component `conts` for allocated continuations + - `S ::= {..., conts ?*}` + +* A continuation is a context annotated with its hole's arity + - `cont ::= (E : n)` + + +#### 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*]` + +* `(prompt{*} * end)` represents an active handler + - `(prompt{((a $l) | (b switch))*}? instr* end) : [t1*] -> [t2*]` + - iff `instr* : [t1*] -> [t2*]` + - 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 ::= ( $l) hdl | ( 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])*` + - and `S' = S with conts[ca] = epsilon` + +* `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` + +* `S; F; (prompt{(e $l)*}? v* end) --> S; F; v*` + +* `S; F; (prompt H^ea[(suspend $e)] end) --> S; F; trap` + - 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*` + - and `ea = F.tags[$e]` + - and `S.tags[ea].type ~~ [t1^n] -> [t2^m]` + - and `S' = S with conts += (H^ea : m)` + +* `S; F; (prompt{hdl* (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)` + ### Binary format We extend the binary format of composite types, heap types, and instructions. @@ -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 | | ------ | ------------------------ | ---------- | From db96405bcae51c268aa0820fde1e4be20428c6b2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 22 Jan 2025 10:20:58 +0000 Subject: [PATCH 02/18] Some type expansions --- proposals/stack-switching/Explainer.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index e2896ed7..7c4ece01 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -861,11 +861,11 @@ of event, even if they use the correct tag. * `(prompt{*} * end)` represents an active handler - `(prompt{((a $l) | (b switch))*}? instr* end) : [t1*] -> [t2*]` - iff `instr* : [t1*] -> [t2*]` - - and `(S.tags[a].type = [te1*] -> [te2*])*` - - and `(S.tags[b].type = [] -> [te2*])*` + - 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 `($ct' ~~ cont $ft')*` - and `([te2*] -> [t2*] <: $ft')*` The administrative structure `hdl` is defined as. From 2330933c41e49cbe68ef4be44aeaf65287a2d994 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 22 Jan 2025 10:21:49 +0000 Subject: [PATCH 03/18] Fix minor typo, hdl => hdl1 --- proposals/stack-switching/Explainer.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 7c4ece01..d4305f72 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -941,7 +941,7 @@ H^ea ::= - and `S.tags[ea].type ~~ [t1^n] -> [t2^m]` - and `S' = S with conts += (H^ea : m)` -* `S; F; (prompt{hdl* (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` +* `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*` From d8ad9ede01e858eb85e86a87df67ebafa29cb377 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 22 Jan 2025 10:23:20 +0000 Subject: [PATCH 04/18] Fix typo: stray ' --- proposals/stack-switching/Explainer.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index d4305f72..6f7bb21d 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -898,7 +898,7 @@ H^ea ::= * `S; F; (ref.null t) (cont.bind $ct $ct') --> S; F; trap` -* `S; F; (ref.cont ca) (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|)` From 79e59f64734715193a1e1bce1377d4d3224a8e85 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 6 Feb 2025 09:48:13 +0000 Subject: [PATCH 05/18] Address Andreas' feedback --- proposals/stack-switching/Explainer.md | 45 ++++++++++++-------------- 1 file changed, 21 insertions(+), 24 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 6f7bb21d..f352f9a4 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -835,14 +835,6 @@ 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 *}` - -* A *tag instance* represents a control tag (from the exception - handling proposal) - - `taginst ::= {type }` - * New store component `conts` for allocated continuations - `S ::= {..., conts ?*}` @@ -855,23 +847,33 @@ of event, even if they use the correct tag. * `(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*` + + and `(val : t1)^n` - and `$ct ~~ cont $ft` - and `$ft ~~ [t1^n] -> [t2*]` * `(prompt{*} * end)` represents an active handler - - `(prompt{((a $l) | (b switch))*}? instr* end) : [t1*] -> [t2*]` + - `(prompt{hdl*}? instr* end) : [t1*] -> [t2*]` - iff `instr* : [t1*] -> [t2*]` - - and `(S.tags[a].type ~~ [te1*] -> [te2*])*` - - and `(S.tags[b].type ~~ [] -> [te2*])*` + - and `(hdl : [t2^*])*` + +The administrative structure `hdl` is defined as +``` +hdl ::= ( $l) | ( switch) +``` + +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')*` -The administrative structure `hdl` is defined as. -``` -hdl ::= ( $l) hdl | ( switch) -``` +* `(a switch)` represents a tag-switch association + - `(a switch)` and `(S.tags[b].type ~~ [] -> [te2*])*` #### Handler contexts @@ -882,7 +884,7 @@ H^ea ::= 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'*) + prompt{hdl*} H^ea end (iff ea notin tagaddr(hdl*)) ``` @@ -916,7 +918,6 @@ H^ea ::= * `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])*` - and `S' = S with conts[ca] = epsilon` * `S; F; (ref.null t) (resume_throw $ct $e (on $t $l)*) --> S; F; trap` @@ -926,17 +927,13 @@ H^ea ::= * `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` -* `S; F; (prompt{(e $l)*}? v* end) --> S; F; v*` - -* `S; F; (prompt H^ea[(suspend $e)] end) --> S; F; trap` - - iff `ea = F.tags[$e]` +* `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 ea1*` + - iff `ea notin tagaddr(hdl1*)` - and `ea = F.tags[$e]` - and `S.tags[ea].type ~~ [t1^n] -> [t2^m]` - and `S' = S with conts += (H^ea : m)` @@ -944,7 +941,7 @@ H^ea ::= * `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 notin tagaddr(hdl1*)` - and `ea = F.tags[$e]` - and `$ct ~~ cont $ft` - and `$ft ~~ [t1* (ref $ct2)] -> [t2*]` From d7e176dcae4a1c341e661d2194731688ceb4c44a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 6 Feb 2025 10:18:02 +0000 Subject: [PATCH 06/18] Remove stray ^ --- proposals/stack-switching/Explainer.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index f352f9a4..c584112c 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -855,7 +855,7 @@ of event, even if they use the correct tag. * `(prompt{*} * end)` represents an active handler - `(prompt{hdl*}? instr* end) : [t1*] -> [t2*]` - iff `instr* : [t1*] -> [t2*]` - - and `(hdl : [t2^*])*` + - and `(hdl : [t2*])*` The administrative structure `hdl` is defined as ``` From 86c97787b1383f0c8b0a273fda8a4bdf6732c90c Mon Sep 17 00:00:00 2001 From: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Date: Fri, 22 Aug 2025 19:07:23 +0200 Subject: [PATCH 07/18] 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. --- proposals/stack-switching/Explainer.md | 41 ++++++++++++++++---------- 1 file changed, 25 insertions(+), 16 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index c584112c..704908fb 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -811,6 +811,7 @@ This abbreviation will be formalised with an auxiliary function or other means i - `suspend $t : [t1*] -> [t2*]` - iff `C.tags[$t] = tag $ft` - and `C.types[$ft] ~~ func [t1*] -> [t2*]` + - During the validation phase, the tag name `$t` is replaced by the corresponding `` - `switch ` - Switch to executing a given continuation directly, suspending the current execution. @@ -822,6 +823,7 @@ This abbreviation will be formalised with an auxiliary function or other means i - and `te1* <: t*` - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` - and `t* <: te2*` + - During the validation phase, the tag name `$t` is replaced by the corresponding `` ### Execution @@ -853,9 +855,9 @@ of event, even if they use the correct tag. - and `$ft ~~ [t1^n] -> [t2*]` * `(prompt{*} * end)` represents an active handler - - `(prompt{hdl*}? instr* end) : [t1*] -> [t2*]` - - iff `instr* : [t1*] -> [t2*]` - - and `(hdl : [t2*])*` + - `(prompt{hdl*}? instr* end) : [] -> [t*]` + - iff `instr* : [] -> [t*]` in the empty context + - and `(hdl : [t*])*` The administrative structure `hdl` is defined as ``` @@ -873,7 +875,10 @@ where - and `([te2*] -> [t2*] <: $ft')*` * `(a switch)` represents a tag-switch association - - `(a switch)` and `(S.tags[b].type ~~ [] -> [te2*])*` + - `(a switch) : [t2*]` + - iff `(S.tags[b].type ~~ [] -> [te2*])*` + +Note: `(a $l)` and `(a switch)` use a separate namespace for the name `a` #### Handler contexts @@ -884,7 +889,7 @@ H^ea ::= 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*)) + prompt{hdl*} H^ea end (iff ea notin hdl*) ``` @@ -903,7 +908,7 @@ H^ea ::= * `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|)` +* `S; F; v^n (ref.cont ca) (cont.bind $ct $ct') --> S'; F; (ref.cont |S.conts|)` - iff `S.conts[ca] = (E' : n')` - and `$ct' ~~ cont $ft'` - and `$ft' ~~ [t1'*] -> [t2'*]` @@ -911,38 +916,42 @@ H^ea ::= - 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.null t) (resume $ct hdl*) --> S; F; trap` -* `S; F; (ref.cont ca) (resume $ct (on $e $l)*) --> S; F; trap` +* `S; F; (ref.cont ca) (resume $ct hdl*) --> 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` +* `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` + - and `hdl'*` is obtained by translating the `` from `hdl*` into `` using `F.tag`: + - if `on $a $l` is in `hdl*` and `F.tags[$e]=ea`, then `ea $l` is in `hdl'*` + - if `on $a switch` is in `hdl'*` and `F.tags[$e]=ea`, then `ea switch` is in `hdl'*` -* `S; F; (ref.null t) (resume_throw $ct $e (on $t $l)*) --> S; F; trap` +* `S; F; (ref.null t) (resume_throw $ct $e hdl*) --> S; F; trap` -* `S; F; (ref.cont ca) (resume_throw $ct $e (on $t $l)*) --> S; F; trap` +* `S; F; (ref.cont ca) (resume_throw $ct $e hdl*) --> 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` +* `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` + - and `hdl'*` is obtained by translating the `` from `hdl*` into `` using `F.tag`: + - if `on $a $l` is in `hdl*` and `F.tags[$e]=ea`, then `ea $l` is in `hdl'*` + - if `on $a switch` is in `hdl'*` and `F.tags[$e]=ea`, then `ea switch` is in `hdl'*` * `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)` +* `S; F; (prompt{hdl1* (ea $l) hdl2*} H^ea[v^n (suspend ea)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)` - iff `ea notin tagaddr(hdl1*)` - - and `ea = F.tags[$e]` - 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` +* `S; F; (prompt{hdl1* (ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch $ct ea)] 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` From 97b28005eae51aceae5f035195a00bef547f919b Mon Sep 17 00:00:00 2001 From: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Date: Fri, 29 Aug 2025 14:19:33 +0200 Subject: [PATCH 08/18] 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. --- proposals/stack-switching/Explainer.md | 29 +++++++++++++++++++------- 1 file changed, 22 insertions(+), 7 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 704908fb..059e5752 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -808,10 +808,9 @@ This abbreviation will be formalised with an auxiliary function or other means i - `suspend ` - Use a control tag to suspend the current computation. - - `suspend $t : [t1*] -> [t2*]` - - iff `C.tags[$t] = tag $ft` + - `suspend $e : [t1*] -> [t2*]` + - iff `C.tags[$e] = tag $ft` - and `C.types[$ft] ~~ func [t1*] -> [t2*]` - - During the validation phase, the tag name `$t` is replaced by the corresponding `` - `switch ` - Switch to executing a given continuation directly, suspending the current execution. @@ -823,7 +822,6 @@ This abbreviation will be formalised with an auxiliary function or other means i - and `te1* <: t*` - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` - and `t* <: te2*` - - During the validation phase, the tag name `$t` is replaced by the corresponding `` ### Execution @@ -854,6 +852,18 @@ of event, even if they use the correct tag. - and `$ct ~~ cont $ft` - and `$ft ~~ [t1^n] -> [t2*]` +* `(suspend.addr ea)` represents a `(suspend $e)` instruction where the tag index `$e` has been replaced with the physical address `ea` of the tag. + - `suspend.addr ea : [t1*] -> [t2*]` + - iff `S.tags[ea].type ~~ [t1*] -> [t2*]` + +* `(switch.addr $ct ea)` represents a `(switch $ct $e)` instruction where the tag index `$e` has been replaced with the physical address `ea` of the tag. + - `switch.addr $ct ea : : [t1* (ref null $ct1)] -> [t2*]` + - iff `S.tags[$e].type ~~ [] -> [t*]` + - and `C.types[$ct] ~~ cont [t1* (ref null? $ct2)] -> [te1*]` + - and `te1* <: t*` + - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` + - and `t* <: te2*` + * `(prompt{*} * end)` represents an active handler - `(prompt{hdl*}? instr* end) : [] -> [t*]` - iff `instr* : [] -> [t*]` in the empty context @@ -878,7 +888,6 @@ where - `(a switch) : [t2*]` - iff `(S.tags[b].type ~~ [] -> [te2*])*` -Note: `(a $l)` and `(a switch)` use a separate namespace for the name `a` #### Handler contexts @@ -943,12 +952,18 @@ H^ea ::= * `S; F; (prompt{hdl*} v* end) --> S; F; v*` -* `S; F; (prompt{hdl1* (ea $l) hdl2*} H^ea[v^n (suspend ea)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)` +* `S; F; (suspend $e) --> S; F; (suspend.addr ea)` + - iff `ea = F.tags[$e]` + +* `S; F; (prompt{hdl1* (ea $l) hdl2*} H^ea[v^n (suspend.addr ea)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)` - iff `ea notin tagaddr(hdl1*)` - 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 ea)] end) --> S''; F; prompt{hdl1* (ea switch) hdl2*} E[v^n (ref.cont |S.conts|)] end` +* `S; F; (switch $ct $e) --> S; F; (switch.addr $ct ea)` + - iff `ea = F.tags[$e]` + +* `S; F; (prompt{hdl1* (ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch.addr $ct ea)] 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*)` From 515e806b9358d8f55f8dbfe3cc0ec1c8eb616ab2 Mon Sep 17 00:00:00 2001 From: Sam Lindley Date: Sat, 30 Aug 2025 00:06:33 +0100 Subject: [PATCH 09/18] Update proposals/stack-switching/Explainer.md Co-authored-by: Thomas Lively --- proposals/stack-switching/Explainer.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 059e5752..ee79a894 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -857,7 +857,7 @@ of event, even if they use the correct tag. - iff `S.tags[ea].type ~~ [t1*] -> [t2*]` * `(switch.addr $ct ea)` represents a `(switch $ct $e)` instruction where the tag index `$e` has been replaced with the physical address `ea` of the tag. - - `switch.addr $ct ea : : [t1* (ref null $ct1)] -> [t2*]` + - `switch.addr $ct ea : [t1* (ref null $ct1)] -> [t2*]` - iff `S.tags[$e].type ~~ [] -> [t*]` - and `C.types[$ct] ~~ cont [t1* (ref null? $ct2)] -> [te1*]` - and `te1* <: t*` From 12d2624a3fa369aedd7be77310ee5b9fd67c83f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 2 Oct 2025 10:54:34 +0100 Subject: [PATCH 10/18] Fix resume_throw semantics --- proposals/stack-switching/Explainer.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index ee79a894..8681ec3f 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -855,14 +855,14 @@ of event, even if they use the correct tag. * `(suspend.addr ea)` represents a `(suspend $e)` instruction where the tag index `$e` has been replaced with the physical address `ea` of the tag. - `suspend.addr ea : [t1*] -> [t2*]` - iff `S.tags[ea].type ~~ [t1*] -> [t2*]` - + * `(switch.addr $ct ea)` represents a `(switch $ct $e)` instruction where the tag index `$e` has been replaced with the physical address `ea` of the tag. - `switch.addr $ct ea : [t1* (ref null $ct1)] -> [t2*]` - iff `S.tags[$e].type ~~ [] -> [t*]` - and `C.types[$ct] ~~ cont [t1* (ref null? $ct2)] -> [te1*]` - and `te1* <: t*` - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` - - and `t* <: te2*` + - and `t* <: te2*` * `(prompt{*} * end)` represents an active handler - `(prompt{hdl*}? instr* end) : [] -> [t*]` @@ -942,10 +942,12 @@ H^ea ::= * `S; F; (ref.cont ca) (resume_throw $ct $e hdl*) --> 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` +* `S; F; v^m (ref.cont ca) (resume_throw $ct $e hdl*) --> S''; F; prompt{hdl'*} E[(ref.exn |S'.exns|) throw_ref] end` - iff `S.conts[ca] = (E : n)` - - and `S.tags[F.tags[$e]].type ~~ [t1^m] -> [t2*]` - - and `S' = S with conts[ca] = epsilon` + - and `ta = S.tags[F.tags[$e]]` + - and `ta.type ~~ [t1^m] -> [t2*]` + - and `S' = S with exns += {ta, v^m}` + - and `S'' = S' with conts[ca] = epsilon` - and `hdl'*` is obtained by translating the `` from `hdl*` into `` using `F.tag`: - if `on $a $l` is in `hdl*` and `F.tags[$e]=ea`, then `ea $l` is in `hdl'*` - if `on $a switch` is in `hdl'*` and `F.tags[$e]=ea`, then `ea switch` is in `hdl'*` From b09f2fa91a1d86677dfe5cf4197c699e7932ffa4 Mon Sep 17 00:00:00 2001 From: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Date: Thu, 2 Oct 2025 14:11:34 +0200 Subject: [PATCH 11/18] Update proposals/stack-switching/Explainer.md Committing tlively's suggested change Co-authored-by: Thomas Lively --- proposals/stack-switching/Explainer.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 8681ec3f..9634d405 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -878,11 +878,11 @@ 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')*` + - 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) : [t2*]` From 12ad434df654aa586636b3299c01b2ca622bac17 Mon Sep 17 00:00:00 2001 From: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Date: Thu, 2 Oct 2025 14:12:24 +0200 Subject: [PATCH 12/18] Update proposals/stack-switching/Explainer.md Committing tlively's suggested change Co-authored-by: Thomas Lively --- proposals/stack-switching/Explainer.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 9634d405..ed9ff332 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -886,7 +886,7 @@ where * `(a switch)` represents a tag-switch association - `(a switch) : [t2*]` - - iff `(S.tags[b].type ~~ [] -> [te2*])*` + - iff `S.tags[a].type ~~ [] -> [te2*]` #### Handler contexts From b570d38010b0c928a964ab510e2967e7e88c8bdd Mon Sep 17 00:00:00 2001 From: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Date: Thu, 2 Oct 2025 14:33:43 +0200 Subject: [PATCH 13/18] Applied all suggested changes except taguse Applied all suggested changes except taguse which is the last remaining issue --- proposals/stack-switching/Explainer.md | 28 +++++++++++++------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index ed9ff332..e1b7095a 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -836,10 +836,10 @@ of event, even if they use the correct tag. #### Store extensions * New store component `conts` for allocated continuations - - `S ::= {..., conts ?*}` + - `S ::= {..., conts ?*}` * A continuation is a context annotated with its hole's arity - - `cont ::= (E : n)` + - `continst ::= (E : n)` #### Administrative instructions @@ -886,7 +886,7 @@ where * `(a switch)` represents a tag-switch association - `(a switch) : [t2*]` - - iff `S.tags[a].type ~~ [] -> [te2*]` + - iff `S.tags[a].type ~~ [] -> [t2*]` #### Handler contexts @@ -933,9 +933,9 @@ H^ea ::= * `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` - - and `hdl'*` is obtained by translating the `` from `hdl*` into `` using `F.tag`: - - if `on $a $l` is in `hdl*` and `F.tags[$e]=ea`, then `ea $l` is in `hdl'*` - - if `on $a switch` is in `hdl'*` and `F.tags[$e]=ea`, then `ea switch` is in `hdl'*` + - and `hdl'*` by mapping the following translation onto `hdl*`: + - a clause of the form `on $a $l` becomes `ea $l` if `F.module.tags[$a]=ea` + - a clause of the form `on $a switch` becomes `ea switch` if `F.module.tags[$a]=ea` * `S; F; (ref.null t) (resume_throw $ct $e hdl*) --> S; F; trap` @@ -944,31 +944,31 @@ H^ea ::= * `S; F; v^m (ref.cont ca) (resume_throw $ct $e hdl*) --> S''; F; prompt{hdl'*} E[(ref.exn |S'.exns|) throw_ref] end` - iff `S.conts[ca] = (E : n)` - - and `ta = S.tags[F.tags[$e]]` + - and `ta = S.tags[F.module.tags[$e]]` - and `ta.type ~~ [t1^m] -> [t2*]` - and `S' = S with exns += {ta, v^m}` - and `S'' = S' with conts[ca] = epsilon` - - and `hdl'*` is obtained by translating the `` from `hdl*` into `` using `F.tag`: - - if `on $a $l` is in `hdl*` and `F.tags[$e]=ea`, then `ea $l` is in `hdl'*` - - if `on $a switch` is in `hdl'*` and `F.tags[$e]=ea`, then `ea switch` is in `hdl'*` + - and `hdl'*` by mapping the following translation onto `hdl*`: + - a clause of the form `on $a $l` becomes `ea $l` if `F.module.tags[$a]=ea` + - a clause of the form `on $a switch` becomes `ea switch` if `F.module.tags[$a]=ea` * `S; F; (prompt{hdl*} v* end) --> S; F; v*` * `S; F; (suspend $e) --> S; F; (suspend.addr ea)` - - iff `ea = F.tags[$e]` + - iff `ea = F.module.tags[$e]` * `S; F; (prompt{hdl1* (ea $l) hdl2*} H^ea[v^n (suspend.addr ea)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)` - - iff `ea notin tagaddr(hdl1*)` + - iff `forall $l', (ea $l') notin hdl1*` - and `S.tags[ea].type ~~ [t1^n] -> [t2^m]` - and `S' = S with conts += (H^ea : m)` * `S; F; (switch $ct $e) --> S; F; (switch.addr $ct ea)` - - iff `ea = F.tags[$e]` + - iff `ea = F.module.tags[$e]` * `S; F; (prompt{hdl1* (ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch.addr $ct ea)] 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 `(switch ea) notin hdl1*` - and `$ct ~~ cont $ft` - and `$ft ~~ [t1* (ref $ct2)] -> [t2*]` - and `$ct2 ~~ cont $ft2` From 6082dc53c67f1d23d58f6b43b6b0ef5abca4b970 Mon Sep 17 00:00:00 2001 From: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Date: Thu, 2 Oct 2025 16:57:42 +0200 Subject: [PATCH 14/18] Added tag uses --- proposals/stack-switching/Explainer.md | 38 ++++++++++++++------------ 1 file changed, 20 insertions(+), 18 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index e1b7095a..27b27296 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -748,6 +748,10 @@ We change the wellformedness condition for tag types to be more liberal, i.e. In other words, the return type of tag types is allowed to be non-empty. +We also introduce tag uses, which can be either tag indices or tag addresses: + +- `taguse ::= tagidx | tagaddr` + ### Instructions The new instructions and their validation rules are as follows. To simplify the presentation, we write this: @@ -806,13 +810,16 @@ This abbreviation will be formalised with an auxiliary function or other means i - iff `C.tags[$e] = tag $ft` - and `C.types[$ft] ~~ func [] -> [t*]` -- `suspend ` +- `suspend ` - Use a control tag to suspend the current computation. - `suspend $e : [t1*] -> [t2*]` - iff `C.tags[$e] = tag $ft` - and `C.types[$ft] ~~ func [t1*] -> [t2*]` + - `suspend ea : [t1*] -> [t2*]` + - iff `S.tags[ea] = tag $ft` + - and `C.types[$ft] ~~ func [t1*] -> [t2*]` -- `switch ` +- `switch ` - Switch to executing a given continuation directly, suspending the current execution. - The suspension and switch are performed from the perspective of a parent `(on $e switch)` handler, determined by the annotated control tag. - `switch $ct1 $e : [t1* (ref null $ct1)] -> [t2*]` @@ -822,6 +829,13 @@ This abbreviation will be formalised with an auxiliary function or other means i - and `te1* <: t*` - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` - and `t* <: te2*` + - `switch $ct1 ea : [t1* (ref null $ct1)] -> [t2*]` + - iff `S.tags[ea] = tag $ft` + - and `C.types[$ft] ~~ func [] -> [t*]` + - and `C.types[$ct1] ~~ cont [t1* (ref null? $ct2)] -> [te1*]` + - and `te1* <: t*` + - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` + - and `t* <: te2*` ### Execution @@ -852,18 +866,6 @@ of event, even if they use the correct tag. - and `$ct ~~ cont $ft` - and `$ft ~~ [t1^n] -> [t2*]` -* `(suspend.addr ea)` represents a `(suspend $e)` instruction where the tag index `$e` has been replaced with the physical address `ea` of the tag. - - `suspend.addr ea : [t1*] -> [t2*]` - - iff `S.tags[ea].type ~~ [t1*] -> [t2*]` - -* `(switch.addr $ct ea)` represents a `(switch $ct $e)` instruction where the tag index `$e` has been replaced with the physical address `ea` of the tag. - - `switch.addr $ct ea : [t1* (ref null $ct1)] -> [t2*]` - - iff `S.tags[$e].type ~~ [] -> [t*]` - - and `C.types[$ct] ~~ cont [t1* (ref null? $ct2)] -> [te1*]` - - and `te1* <: t*` - - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` - - and `t* <: te2*` - * `(prompt{*} * end)` represents an active handler - `(prompt{hdl*}? instr* end) : [] -> [t*]` - iff `instr* : [] -> [t*]` in the empty context @@ -954,18 +956,18 @@ H^ea ::= * `S; F; (prompt{hdl*} v* end) --> S; F; v*` -* `S; F; (suspend $e) --> S; F; (suspend.addr ea)` +* `S; F; (suspend $e) --> S; F; (suspend ea)` - iff `ea = F.module.tags[$e]` -* `S; F; (prompt{hdl1* (ea $l) hdl2*} H^ea[v^n (suspend.addr ea)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)` +* `S; F; (prompt{hdl1* (ea $l) hdl2*} H^ea[v^n (suspend ea)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)` - iff `forall $l', (ea $l') notin hdl1*` - and `S.tags[ea].type ~~ [t1^n] -> [t2^m]` - and `S' = S with conts += (H^ea : m)` -* `S; F; (switch $ct $e) --> S; F; (switch.addr $ct ea)` +* `S; F; (switch $ct $e) --> S; F; (switch $ct ea)` - iff `ea = F.module.tags[$e]` -* `S; F; (prompt{hdl1* (ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch.addr $ct ea)] end) --> S''; F; prompt{hdl1* (ea switch) hdl2*} E[v^n (ref.cont |S.conts|)] end` +* `S; F; (prompt{hdl1* (ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch $ct ea)] 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 `(switch ea) notin hdl1*` From b304d861124ac7f1e0d1a8507eb448e9d4b05c6a Mon Sep 17 00:00:00 2001 From: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Date: Thu, 2 Oct 2025 17:41:27 +0200 Subject: [PATCH 15/18] using taguse in hdl too --- proposals/stack-switching/Explainer.md | 44 ++++++++------------------ 1 file changed, 13 insertions(+), 31 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 27b27296..39f648be 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -797,7 +797,7 @@ This abbreviation will be formalised with an auxiliary function or other means i - and `C.types[$ft] ~~ func [te*] -> []` - and `(hdl : t2*)*` -- `hdl = (on ) | (on switch)` +- `hdl = (on ) | (on switch)` - Handlers attached to `resume` and `resume_throw`, handling control tags for `suspend` and `switch`, respectively. - `(on $e $l) : t*` - iff `C.tags[$e] = tag $ft` @@ -806,9 +806,17 @@ This abbreviation will be formalised with an auxiliary function or other means i - and `t1* <: t1'*` - and `C.types[$ct] ~~ cont [t2'*] -> [t'*]` - and `[t2*] -> [t*] <: [t2'*] -> [t'*]` + - `(on ea $l) : t*` + - iff `S.tags[ea].type ~~ [t1*] -> [t2*]` + - and `C.labels[$l] = [t1'* (ref null? $ct)]` + - and `t1* <: t1'*` + - and `C.types[$ct] ~~ cont [t2'*] -> [t'*]` + - and `[t2*] -> [t*] <: [t2'*] -> [t'*]` - `(on $e switch) : t*` - iff `C.tags[$e] = tag $ft` - and `C.types[$ft] ~~ func [] -> [t*]` + - `(on ea switch) : t*` + - iff `S.tags[ea].type ~~ [] -> [t*]` - `suspend ` - Use a control tag to suspend the current computation. @@ -816,8 +824,7 @@ This abbreviation will be formalised with an auxiliary function or other means i - iff `C.tags[$e] = tag $ft` - and `C.types[$ft] ~~ func [t1*] -> [t2*]` - `suspend ea : [t1*] -> [t2*]` - - iff `S.tags[ea] = tag $ft` - - and `C.types[$ft] ~~ func [t1*] -> [t2*]` + - iff `S.tags[ea].types ~~ func [t1*] -> [t2*]` - `switch ` - Switch to executing a given continuation directly, suspending the current execution. @@ -830,8 +837,7 @@ This abbreviation will be formalised with an auxiliary function or other means i - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` - and `t* <: te2*` - `switch $ct1 ea : [t1* (ref null $ct1)] -> [t2*]` - - iff `S.tags[ea] = tag $ft` - - and `C.types[$ft] ~~ func [] -> [t*]` + - iff `S.tags[ea].types ~~ func [] -> [t*]` - and `C.types[$ct1] ~~ cont [t1* (ref null? $ct2)] -> [te1*]` - and `te1* <: t*` - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` @@ -871,26 +877,6 @@ of event, even if they use the correct tag. - iff `instr* : [] -> [t*]` in the empty context - and `(hdl : [t*])*` -The administrative structure `hdl` is defined as -``` -hdl ::= ( $l) | ( switch) -``` - -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) : [t2*]` - - iff `S.tags[a].type ~~ [] -> [t2*]` - - #### Handler contexts ``` @@ -935,9 +921,7 @@ H^ea ::= * `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` - - and `hdl'*` by mapping the following translation onto `hdl*`: - - a clause of the form `on $a $l` becomes `ea $l` if `F.module.tags[$a]=ea` - - a clause of the form `on $a switch` becomes `ea switch` if `F.module.tags[$a]=ea` + - and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]` * `S; F; (ref.null t) (resume_throw $ct $e hdl*) --> S; F; trap` @@ -950,9 +934,7 @@ H^ea ::= - and `ta.type ~~ [t1^m] -> [t2*]` - and `S' = S with exns += {ta, v^m}` - and `S'' = S' with conts[ca] = epsilon` - - and `hdl'*` by mapping the following translation onto `hdl*`: - - a clause of the form `on $a $l` becomes `ea $l` if `F.module.tags[$a]=ea` - - a clause of the form `on $a switch` becomes `ea switch` if `F.module.tags[$a]=ea` + - and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]` * `S; F; (prompt{hdl*} v* end) --> S; F; v*` From ff3c5e00854f0ab7c40f758af0afd9a0e4a3acc7 Mon Sep 17 00:00:00 2001 From: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Date: Thu, 2 Oct 2025 18:18:25 +0200 Subject: [PATCH 16/18] factored typing rules and added keyword 'on' where now necessary --- proposals/stack-switching/Explainer.md | 49 +++++++++----------------- 1 file changed, 17 insertions(+), 32 deletions(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 39f648be..67376eff 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -751,6 +751,11 @@ In other words, the return type of tag types is allowed to be non-empty. We also introduce tag uses, which can be either tag indices or tag addresses: - `taguse ::= tagidx | tagaddr` + - `$a : [t1*] -> [t2*]` + - iff `C.tags[$e] = tag $ft` + - and `C.types[$ft] ~~ func [t1*] -> [t2*]` + - `ea : [t1*] -> [t2*]` + - iff `S.tags[ea].type ~~ [t1*] -> [t2*]` ### Instructions @@ -799,45 +804,25 @@ This abbreviation will be formalised with an auxiliary function or other means i - `hdl = (on ) | (on switch)` - Handlers attached to `resume` and `resume_throw`, handling control tags for `suspend` and `switch`, respectively. - - `(on $e $l) : t*` - - iff `C.tags[$e] = tag $ft` - - and `C.types[$ft] ~~ func [t1*] -> [t2*]` - - and `C.labels[$l] = [t1'* (ref null? $ct)]` - - and `t1* <: t1'*` - - and `C.types[$ct] ~~ cont [t2'*] -> [t'*]` - - and `[t2*] -> [t*] <: [t2'*] -> [t'*]` - - `(on ea $l) : t*` - - iff `S.tags[ea].type ~~ [t1*] -> [t2*]` + - `(on tu $l) : t*` + - iff `tu : [t1*] -> [t2*]` - and `C.labels[$l] = [t1'* (ref null? $ct)]` - and `t1* <: t1'*` - and `C.types[$ct] ~~ cont [t2'*] -> [t'*]` - and `[t2*] -> [t*] <: [t2'*] -> [t'*]` - - `(on $e switch) : t*` - - iff `C.tags[$e] = tag $ft` - - and `C.types[$ft] ~~ func [] -> [t*]` - - `(on ea switch) : t*` - - iff `S.tags[ea].type ~~ [] -> [t*]` + - `(on tu switch) : t*` + - iff `tu : [] -> [t*]` - `suspend ` - Use a control tag to suspend the current computation. - - `suspend $e : [t1*] -> [t2*]` - - iff `C.tags[$e] = tag $ft` - - and `C.types[$ft] ~~ func [t1*] -> [t2*]` - - `suspend ea : [t1*] -> [t2*]` - - iff `S.tags[ea].types ~~ func [t1*] -> [t2*]` + - `suspend tu : [t1*] -> [t2*]` + - iff `tu : func [t1*] -> [t2*]` - `switch ` - Switch to executing a given continuation directly, suspending the current execution. - The suspension and switch are performed from the perspective of a parent `(on $e switch)` handler, determined by the annotated control tag. - - `switch $ct1 $e : [t1* (ref null $ct1)] -> [t2*]` - - iff `C.tags[$e] = tag $ft` - - and `C.types[$ft] ~~ func [] -> [t*]` - - and `C.types[$ct1] ~~ cont [t1* (ref null? $ct2)] -> [te1*]` - - and `te1* <: t*` - - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` - - and `t* <: te2*` - - `switch $ct1 ea : [t1* (ref null $ct1)] -> [t2*]` - - iff `S.tags[ea].types ~~ func [] -> [t*]` + - `switch $ct1 tu : [t1* (ref null $ct1)] -> [t2*]` + - iff `tu : [] -> [t*]` - and `C.types[$ct1] ~~ cont [t1* (ref null? $ct2)] -> [te1*]` - and `te1* <: t*` - and `C.types[$ct2] ~~ cont [t2*] -> [te2*]` @@ -941,18 +926,18 @@ H^ea ::= * `S; F; (suspend $e) --> S; F; (suspend ea)` - iff `ea = F.module.tags[$e]` -* `S; F; (prompt{hdl1* (ea $l) hdl2*} H^ea[v^n (suspend ea)] end) --> S'; F; v^n (ref.cont |S.conts|) (br $l)` - - iff `forall $l', (ea $l') notin hdl1*` +* `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)` + - iff `forall $l', (on ea $l') notin hdl1*` - and `S.tags[ea].type ~~ [t1^n] -> [t2^m]` - and `S' = S with conts += (H^ea : m)` * `S; F; (switch $ct $e) --> S; F; (switch $ct ea)` - iff `ea = F.module.tags[$e]` -* `S; F; (prompt{hdl1* (ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch $ct ea)] end) --> S''; F; prompt{hdl1* (ea switch) hdl2*} E[v^n (ref.cont |S.conts|)] end` +* `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` - iff `S.conts[ca] = (E : n')` - and `n' = 1 + n` - - and `(switch ea) notin hdl1*` + - and `(on switch ea) notin hdl1*` - and `$ct ~~ cont $ft` - and `$ft ~~ [t1* (ref $ct2)] -> [t2*]` - and `$ct2 ~~ cont $ft2` From f44c8d18c60addefbee92c876635b306429bb684 Mon Sep 17 00:00:00 2001 From: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Date: Thu, 2 Oct 2025 19:37:18 +0200 Subject: [PATCH 17/18] Typo in typing rule for tag addresses --- proposals/stack-switching/Explainer.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 67376eff..6c1d9f08 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -755,7 +755,7 @@ We also introduce tag uses, which can be either tag indices or tag addresses: - iff `C.tags[$e] = tag $ft` - and `C.types[$ft] ~~ func [t1*] -> [t2*]` - `ea : [t1*] -> [t2*]` - - iff `S.tags[ea].type ~~ [t1*] -> [t2*]` + - iff `S.tags[ea].type ~~ func [t1*] -> [t2*]` ### Instructions From 73359699a8bff0df4e08a5ce31184480ea7bfdfc Mon Sep 17 00:00:00 2001 From: mlegoupil <90708290+mlegoupil@users.noreply.github.com> Date: Fri, 3 Oct 2025 14:38:42 +0200 Subject: [PATCH 18/18] corrected $a to $e and added switch failure rules --- proposals/stack-switching/Explainer.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md index 6c1d9f08..98f997d6 100644 --- a/proposals/stack-switching/Explainer.md +++ b/proposals/stack-switching/Explainer.md @@ -751,7 +751,7 @@ In other words, the return type of tag types is allowed to be non-empty. We also introduce tag uses, which can be either tag indices or tag addresses: - `taguse ::= tagidx | tagaddr` - - `$a : [t1*] -> [t2*]` + - `$e : [t1*] -> [t2*]` - iff `C.tags[$e] = tag $ft` - and `C.types[$ft] ~~ func [t1*] -> [t2*]` - `ea : [t1*] -> [t2*]` @@ -934,6 +934,11 @@ H^ea ::= * `S; F; (switch $ct $e) --> S; F; (switch $ct ea)` - iff `ea = F.module.tags[$e]` +* `S; F; (ref.null t) (switch $ct ea) --> S; F; trap` + +* `S; F; (ref.cont ca) (switch $ct ea) --> S; F; trap` + - iff `S.conts[ca] = epsilon` + * `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` - iff `S.conts[ca] = (E : n')` - and `n' = 1 + n`