WasmFX direct switching w/ dynamic lookup

[tlively]

The continuations explainer includes a section on direct (i.e. symmetric) switching: https://github.com/WebAssembly/stack-switching/blob/main/proposals/continuations/Explainer.md#direct-switching

The second design in that section, reproduced below, gives typing rules for direct switching with dynamic handler lookup:

  switch : [ t1* (ref $ct1) ] -> [ t2* ]
  where:
  - $ct1 = cont ([ (ref $ct2) t1* ] -> [ t3* ])
  - $ct2 = cont ([ t2* ] -> [ t3* ])

My question is about the result type t3* of the new and previous continuations. For soundness, t3* needs to be the result type expected by the resume instruction where the handler was installed, but the proposed typing above has no way to constrain t3* to match that type. Is it expected that there would be a runtime check that they types match?

Perhaps another solution would be to introduce a kind of special tag that can only be handled in resumes where the tag parameter type matches the resume result type. We could then give switch a tagidx immediate like resume, but constrain it so that the tag must be one of these special tags. That would allow us to know at validation time what t3* should be by inspecting the tag.

Besides named handlers and switch_to, which don't have this problem, are there other ways we could ensure that t3* is the type the resume instruction expects to receive?

[tlively]

cc @fgmccabe, since we were wondering how the typing of symmetric switching in WasmFX should work.

[conrad-watt]

I think a different "kind" of tag isn't strictly necessary, but you're right that the way to do this soundly would be to express intent to switch directly on the handler rather than at the suspend point. I'm drawing from recent conversations with @rossberg and @slindley for the rest of this comment - my understanding is they've considered the possibility of this but IIUC it's not been documented.

So a regular handler case attached to a resume looks like on $e $l, and when it handles a suspend signal with tag $e it jumps to label $l for processing. To support "direct" switching we'd introduce a new handler case, on $e switch, where $e must be a tag type which carries a continuation (to directly switch to) plus its arguments. Instead of jumping to a label, on $e switch would immediately resume the continuation carried by the tag. One of the arguments to this continuation would be the continuation we just suspended.

At the suspend point, you would just use a regular suspend instruction, but the type of the tag would need to be compatible with the on $e switch handler you intend to hit - e.g. you would need to provide the "switch-to continuation" and its arguments at the suspension point.

This has the advantage that the runtime doesn't need to do two separate stack switches with user code in between, although you still need a "linear search" to find the parent handler from whose perspective the direct switch is occurring - this is fundamental to the delimited approach, so that you know where to go if the "switched to" continuation fully returns. In the case that the "direct switch" handler is the immediate parent, this is just a constant overhead (depending on implementation strategy).

Sketched reduction rules (courtesy of @rossberg from an earlier conversation)

S;  F; (handle{hdl*} H^ea[v^n (ref.cont ca) (suspend $e)])
-->
S'; F; (handle{hdl*} E[v^n (ref.cont |S.conts|)])

-- if hdl* = (ea1 $l1)* (ea switch) (ea2 $l2)*
-- if ea = F.tags[$e]
-- if ea notin ea1*
-- if S.conts[ca] = (E : n + 1)
-- if S.tags[ea].type = t1^n rt -> t2^m
-- if S' = (S with conts[ca] = eps) with conts += (H^ea : m)

[rossberg]

FWIW, here is the complete version of what I suggested at the time:

Here is my early morning take on a very minimal possible design. Let’s say we merely extend resume's handler syntax to allow handlers of the form (on $e switch), i.e., instead of a label, they can also just have a switch keyword:

   hdl  ::=  on $e $l  |  on $e switch

Then performing a switch is simply initiated by a suspend with a tag that has a switch handler. Such a tag needs to have a continuation parameter. When a switch handler is matched, it resumes the passed continuation, reinstalling the same handler.

(There could be a separate switch instruction and other constraints/annotations on the tag for better optimisability, but semantically, this is all it takes.)

The direct-parent-only restriction for handler search would apply naturally to this as well. When imposed, it would be similar to the BoS stack switch, except that parent edges are explicit and switch handlers can be nested, allowing e.g. proper virtualisation. The “main” stack would simply become the one that did the original resume. Moreover, thanks to tags, a single handler can perform switches for multiple different continuation types, which is not possible in the BoS design.

The desugaring would be something like this (showing the single switch case only, generalisable in the obvious manner). I need cont.bind to unify the types of the incoming continuations:

(resume $ct hdl1* (on $e switch) hdl2*)
==
(cont.bind $ct $ct')
(loop $l
 (block $x
   (block $le
     (resume $ct' hdl1* (on $e $le) hdl2*)
     (br $x)
   )
   (cont.bind $cte $ct')
   (br $l)
 )
)

where

 $e : te1* -> te2*
 $ct ~~ cont t1* -> t2*
 $ct' ~~ cont eps -> t2*
 $cte ~~ cont te1* (ref $cte') -> t2*

Typing rules (no warranty):

resume $ct hdl* : t1* (ref null $ct) -> t2*
-- if $ct ~~ cont $ft
-- if $ft ~~ func t1* -> t2*
-- if (hdl : t2*)*

on $e $l : t*
-- if tag $e : te1* -> te2*
-- if label $l : tl1* (ref null? $ct)
-- if (te1 <: tl1)*
-- if $ct ~~ cont $ft
-- if func te2* -> t* <: $ft

on $e switch : t*
-- if tag $e : te1* (ref null? $ct1) -> te2*
-- if $ct1 ~~ cont $ft1
-- if $ft1 ~~ <: func te1* (ref null? $ct2) -> t*
-- if $ct2 ~~ cont $ft2
-- if func te2* -> t* <: $ft2

I believe the direct reduction rule would be something like

S;  F; (handle{hdl*} H^ea[v^n (ref.cont ca) (suspend $e)])
-->
S'; F; (handle{hdl*} E[v^n (ref.cont |S.conts|)])

-- if hdl* = (ea1 $l1)* (ea switch) (ea2 $l2)*
-- if ea = F.tags[$e]
-- if ea notin ea1*
-- if S.conts[ca] = (E : n + 1)
-- if S.tags[ea].type = t1^n rt -> t2^m
-- if S' = (S with conts[ca] = eps) with conts += (H^ea : m)

(This is a general formulation, we can orthogonally apply the direct-parent restriction, here and elsewhere, by cutting the definition of H contexts appropriately to not include handlers.)

[rossberg]

The trick here is that we use a tag to enforce the necessary type consistency across places in the code.

[lukewagner]

I believe we would be able to further optimize the direct-switch instruction sequence if, as an additional validation rule: tag declarations could declare they were "switching", (on $e switch) required $e to "switching" and (on $e $l) required $e to not be "switching". Otherwise, at the point of a suspend $e, you have to compile a instruction sequence that can either do a symmetric switch or a suspend-to-handler.

[conrad-watt]

Otherwise, at the point of a suspend $e, you have to compile a instruction sequence that can either do a symmetric switch or a suspend-to-handler.

I think things end up being fairly unified - the code you have to generate at the suspend point is "find the closest handler", which will lead you to some switch-like code associated with the handler that dispatches based on the tag. If the handler+tag is a normal one, you perform a switch to the associated parent stack and dispatch to the relevant user code. If the handler+tag is a "direct switch" one, you dispatch to some optimised runtime procedure for the direct switch. I'd expect that any cost inherent to distinguishing between the two kinds of handler is already absorbed by the cost of distinguishing between different tags (e.g. even with a distinguished "switching" tag, you'd still need the same dispatch to see which switching tag is matched at the handler site).

EDIT: my instinct is against adding a distinguished tag "kind", because tags could show up in many other places (e.g. the types of continuations themselves) where "switching"-ness seems irrelevant.

[lukewagner]

If we statically know at the resume-site that we're definitely doing a direct switch (or else we're trapping), we don't need to dispatch to a separate runtime procedure that does the direct switch, we can just emit the code to do the direct-switch inline (after a trapping branch), thereby eliminating an indirection. My assumptions here are that (1) the inline switching code won't be so slow as to make this optimization negligible and (2) languages like Go will use this feature intensively and so it's worth optimizing this to the same degree as calls and loads/stores, where we've historically tried to eliminate every branch and indirection by design to achieve predictable performance. But maybe I'm wrong about one of these and we can measure.

[tlively]

I guess the inline code would be a fast path for the case where the innermost handler is the correct one, and if that's not the case, it would fall back to the more general procedure for looking up the handler then trapping or doing the switch?

[conrad-watt]

The point about inlining is fair. I guess we could interpret the "switching"-ness bit as just saying that it's a validation error for the tag to be part of any handler except a switch handler, so in other contexts it can still be interpreted as normal.

This could be added later as an optimisation though based on our experiments - ordinary tags could go everywhere, and would always do the out-of-line thing, and then later the "switch-only" tags could be added on top.

[tlively]

If we take as a requirement that the compiler must know at the suspend site when it is going to perform a switch¹ and consider that we can signal a switch in some combination of the handler, the tag attribute, and the suspend/switch instruction, here are all of the possible designs:

handler	tag attribute	switch instruction	feasible and reasonable?
		✔️	❌ - underconstrained continuation result type
	✔️		❌ - handler label unused
	✔️	✔️	✅ - "continuation-switched"
✔️			❌ - switching unknown at suspend site
✔️		✔️	❌ - dynamic type check for result type
✔️	✔️		✅ - "handler-switched"
✔️	✔️	✔️	❌ - feasible but redundant

Thankfully the "continuation-switched" and "handler-switched" designs are the two we've already identified.

In the "continuation-switched" design, the tag attribute means that the tag may be used for direct switches, but since the continuation is in control of whether a switch or suspend will occur, there's no reason to disallow the special tags from being used for normal suspensions as well. This design is analogous to tail calls, where the callee (or the continuation) can perform a tail call (or a symmetric switch) as an implementation detail that the caller (or the handler) does not participate in. The handler still has to be aware of the possibility of a symmetric switch because it has to use one of the special tags, though, so the encapsulation is not complete.

In the "handler-switched" design, the tag attribute means that the tag must be used only for direct switches so the compiler can know for sure at the switch point where a switch is occurring. As discussed above, we could allow the tag to be used for normal suspensions and force the inline fast paths for switches to have a bailout for normal suspensions, but that seems like an unnecessary complication. Similarly, it would be possible to allow switches with normal tags, but then the compiler would not know to inline a fast path at the switch site at all. It seems cleaner to enforce a strict division between tags for normal suspension and tags for switching. In this design, both the handler and continuation have to explicitly participate in the switch by using one of the special tags.

Personally, I prefer the "continuation-switched" design because it allows more flexibility for the continuation to use symmetric switching or not at its own discretion and I like the similarities to tail calls. That being said, the two designs are equally expressive and I can't see any reason one would have performance benefits over the other.

Footnotes

1. Taking this as a requirement is not strictly necessary, as @conrad-watt pointed out, but I think it's nice to have and doesn't seem to cost us anything. ↩

[conrad-watt]

In the "continuation-switched" design, the tag attribute means that the tag may be used for direct switches, but since the continuation is in control of whether a switch or suspend will occur, there's no reason to disallow the special tags from being used for normal suspensions as well. This design is analogous to tail calls, where the callee (or the continuation) can perform a tail call (or a symmetric switch) as an implementation detail that the caller (or the handler) does not participate in. The handler still has to be aware of the possibility of a symmetric switch because it has to use one of the special tags, though, so the encapsulation is not complete.

This design seems a little strange, because if the handler has a "switching" tag, IIUC it would still need to provide a body/label target just in case the tag is used for a suspend signal instead.

In the "handler-switched" design, the tag attribute means that the tag must be used only for direct switches so the compiler can know for sure at the switch point where a switch is occurring. As discussed above, we could allow the tag to be used for normal suspensions and force the inline fast paths for switches to have a bailout for normal suspensions

In the handler+tag attribute design, the suspend point knows that if it's using such a "switching" tag, the only two possible outcomes are that a switch will occur (because the only handlers allowed to use this tag are "switching" ones), or a trap/propagation to the next handler will occur (because the tag was never handled). I don't think we would ever allow the use of such a "switching" tag on non-"switching" handlers. I do think it's possible to allow non-"switching" tags on "switching" handlers, if only because it opens up the incremental path of starting with just these and adding the "switching" tags later.

So my preferred approach would be

1. experiment with just switching handlers
2. if it shows a performance benefit, incrementally add switching tags that can only be used in switching handlers (now any suspend site using such a tag can statically inline a switch fast path)

The alternative (as @tlively suggested) is that we add switching tags right away, and only allow these to be used in switching handlers, which I'd be fine with if it's preferred.

[tlively]

In the "continuation-switched" design, the tag attribute means that the tag may be used for direct switches, but since the continuation is in control of whether a switch or suspend will occur, there's no reason to disallow the special tags from being used for normal suspensions as well. This design is analogous to tail calls, where the callee (or the continuation) can perform a tail call (or a symmetric switch) as an implementation detail that the caller (or the handler) does not participate in. The handler still has to be aware of the possibility of a symmetric switch because it has to use one of the special tags, though, so the encapsulation is not complete.

This design seems a little strange, because if the handler has a "switching" tag, IIUC it would still need to provide a body/label target just in case the tag is used for a suspend signal instead.

True. I imagine this would be useful in the same kind of situations that retire instructions would be useful in the Bag-o-stacks design, where you really want to do a non-local return rather than a suspension.

[rossberg]

If I understand correctly, then I suspect that the "continuation-switched" design won't be type-sound. Note how the typing rules I sketched use the tag to tie the types from switch/suspend site and handler together. In particular, only the handler site can enforce that the return type of the target continuation has the right return type as required by the handler. If that wasn't enforced, the target continuation could later return (regularly) with a wrong type of value. So, the handler site has to be involved somehow.

[tlively]

Right, I described a solution for that back in the opening post:

Perhaps another solution would be to introduce a kind of special tag that can only be handled in resumes where the tag parameter type matches the resume result type. We could then give switch a tagidx immediate like resume, but constrain it so that the tag must be one of these special tags. That would allow us to know at validation time what t3* should be by inspecting the tag.

[rossberg]

Wouldn't that essentially be the last row in your table?

[tlively]

Kind of, except that with that design there would be nothing stopping the special tags from being used for asymmetric switching as well, so the handler only knows that symmetric may occur rather than knowing it must occur. I would imagine the last row of the table would have a firmer distinction at the handler.

[tlively]

To make things more concrete, here's the typing I would propose for the continuation-switched design. Note that the continuation result type t_3* is constrained by the tag parameters for soundness as discussed above, but the tag result type t_4* is completely unconstrained. The result type of the instruction is determined by the type of the continuation received at the destination, just like in the bag-o-stacks type system, rather than by the result type of the tag as in a normal suspend. This flexibility allows bag-o-stacks to be compiled to typed continuations using only a single trivial [] -> [] tag for all symmetric switches, no matter what the continuation parameter types are.

C |- switch y x : t_1* (ref null x) -> t_2* rt
-- C.TAGS[y].TYPE = func t_3* -> t4*
-- C.TAGS[y].ATTR = SYMMETRIC
-- expand(C.TYPES[x]) = cont ft_1
-- expand(C.TYPES[ft_1]) = func t_1* (ref null? z) -> t_3*
-- expand(C.TYPES[z]) = cont ft_2
-- expand(C.TYPES[ft_2]) = func t_2* rt -> t_3*

In contrast, the handler-switched design would use a normal suspend, so the result type of the instruction would be the result type of the tag¹, and separate validation of the tag would ensure that this result type has the right shape for symmetric switching. When compiling from bag-o-stacks with this design, the single resume used as the delimiter for all symmetric switch would need a separate handler tag for every single possible choice of continuation parameters in the module.

If we're serious about supporting programs that primarily use symmetric switching with a single, top-level handler, then we should choose the continuation-switched design and allow those programs to use just a single tag for their symmetric switching.

Footnotes

1. Unless we type suspend differently depending on the tag attribute, but that would be gross. ↩

[conrad-watt]

This seems unsound because you don't preserve the information about the required return result of the switched-to continuation, which needs to match the output type associated the handler. Consider what happens if you return all the way from the switched-to continuation back to the resume point where the handler is located - if the initially-resumed continuation had output type t*, all the switched-to continuations also need to have type <something> -> t*. It only seems possible to enforce this by restricting the allowed tags on the handler side, to prevent any ill-typed switches.

EDIT: I might have missed some of the implications of the conversation above - apologies if I'm making an objection that's already been addressed - trying to understand now

EDIT2: I'm not sure I understand how t_3* is known to be the return type of the "current" continuation, if this is the intention. There's nothing in the typing context of the switch that can statically give you this information. Are we back to having a distinguished switch handler?

If you want to uniformly use one tag for all of your symmetric switching (which I think should be possible), you need to establish a uniform ABI so that each switch point has the same type.

Side question for @rossberg - for principle types, does resume need an explicit type annotation for the initial input configuration?

[conrad-watt]

If I'm understanding correctly that this design assumes the existence of a distinguished "may switch" handler, this seems to lead to codegen inefficiencies on the handler side that are analogous to the potential codegen inefficiencies on the resume side in assuming that every tag may participate in a switch - the handler doesn't know whether it's switching statically, so it needs to generate an additional conditional check to deal with both cases.

[tlively]

The missing piece is once again this part from the opening post:

Perhaps another solution would be to introduce a kind of special tag that can only be handled in resumes where the tag parameter type matches the resume result type. We could then give switch a tagidx immediate like resume, but constrain it so that the tag must be one of these special tags. That would allow us to know at validation time what t3* should be by inspecting the tag.

I should have made this explicit, but the idea is that resume only validates if all of the SYMMETRIC tags that appear in its handlers have output types that match the resumed continuation's output type. So the t_3* above is known to match the result type expected by the resume because the tag is SYMMETRIC.

If you want to uniformly use one tag for all of your symmetric switching (which I think should be possible), you need to establish a uniform ABI so that each switch point has the same type.

But that would be an unnecessary source of inefficiency and loss of type precision. The continuation-switched design allows switching between continuations with any mutually compatible parameter types, just like in bag-o-stacks, as long as their result types match.

If I'm understanding correctly that this design assumes the existence of a distinguished "may switch" handler, this seems to lead to codegen inefficiencies on the handler side that are analogous to the potential codegen inefficiencies on the resume side in assuming that every tag may participate in a switch - the handler doesn't know whether it's switching statically, so it needs to generate an additional conditional check to deal with both cases.

Maybe, but I would expect all the codegen to take place on the suspend/switch side and for the handler to only install some data somewhere marking the fact that the handler exists. If that's wrong, then I would suggest going with a combination of the continuation-switched and handler-switched designs where SYMMETRIC tags cannot be used with normal suspends and therefore do not need to take labels when used as handlers. This really would be the bottom row of my table above.

[tlively]

Side question for @rossberg - for principle types, does resume need an explicit type annotation for the initial input configuration?

It needs a type annotation for the resumed continuation type, which will determine the rest of the input types and the output type.

[conrad-watt]

Ah I think I understand - so the point is that in switch y x, y is the type of the "signal" used to find the matching handler, but only its result type matters, and there's a separate tag x which determines the type of the "switched-to" configuration and therefore the required input type (the output type must match y).

This idea works if all the codegen is done at the site of the switch, and I agree that it would save the need to have different tags if you want to direct switch with different input types. It does rule out an implementation where search is performed by directly jumping execution to each handler, with the main logic at each handler site (at least if one wants to avoid additional dynamic checks/boxing on the shape of the "switched-to" payload), since the handler site won't know how many values to pass into the "switched-to" continuation. I don't know how much of a practical problem this is. The approach where all logic is on the handler is more "uniform" (because regular suspend still wants this), so it seems a shame to make it less viable.

[rossberg]

@tlively, I'm still a bit lost. Can you write out the typing rules for the handler side, and the reduction and/or desugaring defining execution?

[conrad-watt]

I realise that at the module level, @tlively's approach doesn't seem to save on the total number of declared tags, since you still need to declare separate tags for the actual continuation types.

@tlively, how would you feel if in the "handler-switched" design, the switch handler could take a list of tags (which must all have matching output type)? Then you don't need separate switch handler declarations for each choice and we're just talking about handfuls of bytes (with the explicit switch instruction actually requiring an additional index!).

Keeping the handler-switched approach preserves the ability for implementations to use the "logic-on-handler" compilation approach if they want (switch-site code still also works), and lets us spec switch handlers as syntactic sugar, and doesn't seem to have any runtime cost - just the requirement to explicitly list the tags you want to permit switching for on the switch handler (which can be weighed against the extra index needed in every switch if we want to quibble over bytes).

[rossberg]

@conrad-watt, doesn't the handler already take "a list of tags"? Or are you talking about the difference between (on $tag switch)* vs (on tag* switch)? The latter should save about one byte per extra tag, though it actually adds one for the singular case.

[conrad-watt]

@rossberg the latter - I'm trying to drill down into whether explicitly listing the tags on the handler side is actually any worse globally, since it seems to be the main thing @tlively's proposal aims to avoid.

[tlively]

Ah I think I understand - so the point is that in switch y x, y is the type of the "signal" used to find the matching handler, but only its result type matters, and there's a separate tag x which determines the type of the "switched-to" configuration and therefore the required input type (the output type must match y).

Almost. y is the tagidx used to find the handler, and you're right that only its result type matters, since its parameter type would characterize the values sent to the handler, but in the case of symmetric switching, there are no values sent to the handler. x is not a tagidx, but a typeidx for the continuation type of the "switched-to" continuation. That target continuation type determines the other input and output types for the switch instruction, just like in the bag-o-stacks switch instruction. (This is in fact the bag-o-stacks switch instruction with a tagidx added to identify a delimiter and with the typed-continuations continuation type syntax instead of the bag-o-stacks stack type syntax.)

I realise that at the module level, @tlively's approach doesn't seem to save on the total number of declared tags, since you still need to declare separate tags for the actual continuation types.

You only need one tag, but you do still need a separate continuation type for each type of continuation. These are not the same as tags.

@tlively, how would you feel if in the "handler-switched" design, the switch handler could take a list of tags (which must all have matching output type)? Then you don't need separate switch handler declarations for each choice and we're just talking about handfuls of bytes (with the explicit switch instruction actually requiring an additional index!).

I would strongly prefer not to have to have both a continuation type and a tag for every type of continuation involved in symmetric switching when we can get away with just having the continuation type, especially since tags are not structural and do not work like types w.r.t. composability.

@tlively, I'm still a bit lost. Can you write out the typing rules for the handler side, and the reduction and/or desugaring defining execution?

The handler side is a normal resume except that any of these special SYMMETRIC tags used in handlers must have parameter types that match the resume's result type.

  C |- resume x (tag y l)* : [t1* (ref null x)] -> [t2*]
  -- expand(C.TYPES[x]) = cont ft
  -- expand(C.TYPES[ft]) = func t1* -> t2*
  -- ;; constraints on label types l* omitted
  -- (C.TAGS[y].ATTR != SYMMETRIC \/ 
      (C.TAGS[y].TYPE = func t3* -> t4* /\ t3* <: t2*))

(edited to fix the constraint on the tag type)

I'm not going to write out fully precise reduction rules here because that would require some new administrative instruction(s), but the idea is that a continuation is captured up to the delimiter, then passed as the final parameter when resuming the target continuation, just like in any other symmetric switching design. The difference here is that there is no possible desugaring because the handler does not know the type of the other values that are being passed to the target continuation.

[conrad-watt]

You only need one tag, but you do still need a separate continuation type for each type of continuation. These are not the same as tags.

I would strongly prefer not to have to have both a continuation type and a tag for every type of continuation involved in symmetric switching when we can get away with just having the continuation type, especially since tags are not structural and do not work like types w.r.t. composability.

Ah, this was definitely a gap in my mental model. I think this leaves me ok with the idea of using a single tag to carry the necessary result type. The only thing I'd be a little concerned about with the general approach is the idea that an engine might want to do the "logic on handler" compilation strategy, but if at some point during the prototyping process we can get confirmation that this isn't necessary, that's just fine.

The one specific part of the design I'd still push on would be that I think a handler with a symmetric tag shouldn't have a label/regular suspend case. If you know in your compilation scheme that you're only going to use that handler for symmetric switches, you end up needing to still create a fake block with the right type signature that's never actually used. If you genuinely want to suspend instead of switching, it seems more realistic to just use a different tag rather than try and fit the type of the suspended continuation into the type of the symmetric tag.

Side-note: in this comment the result type of the resume is the input type of the symmetric tag, while in this comment the result type of the resume seems to be the output type of the symmetric tag. The input version makes more sense to me, because of the precedent with exception handling tags (in fact, if the label in the symmetric handler is dropped, I'd suggest requiring that the output type be empty, like with exceptions).

[tlively]

The one specific part of the design I'd still push on would be that I think a handler with a symmetric tag shouldn't have a label/regular suspend case.

Yes, that's fine with me! In the worst case you would have to have two tags with the same type if you wanted to switch and suspend interchangeably, but since the switch and suspend are already differentiated at both the switch/suspend point and the handler, that's not too burdensome.

Side-note: in this comment the result type of the resume is the input type of the symmetric tag, while in this comment the result type of the resume seems to be the output type of the symmetric tag.

Oops, that's a mistake in the second comment. The input version is correct. I've edited the comment to fix it.

in fact, if the label in the symmetric handler is dropped, I'd suggest requiring that the output type be empty, like with exceptions.

That's fine with me too, since the output type is literally not used for anything if these tags cannot be used for normal suspends.

[rossberg]

I'm with @conrad-watt that the need for a fake handler is odd. Moreover, if we use a special switch handler, then we can also remove the annotation on the tag itself, can't we? That would be a simplification.

I think there are more simplifications possible:

• Nothing seems to depend on rt being present in the typing of switch, so I think we can just drop it.
• The tag merely fixes the result type of the handler, so it would be more natural to require its parameters to be empty and use its result for the result.

With that in mind we can compare the two versions more directly. Resume as such would be the same for both:

resume $ct hdl* : t1* (ref null $ct) -> t2*
-- if $ct ~~ cont $ft
-- if $ft ~~ func t1* -> t2*
-- if (hdl : t2*)*

The handler-site version types as follows (omitting subtyping for simplicity):

suspend $e : t1* -> t2*
-- if tag $e : t1* -> t2*

on $e switch : t*
-- if tag $e : te1* (ref null? $ct1) -> te2*
-- if $ct1 ~~ cont $ft1
-- if $ft1 ~~ func te1* (ref null? $ct2) -> t*
-- if $ct2 ~~ cont $ft2
-- if $ft2 ~~ func te2* -> t*

The switch-site version types as follows:

C |- switch $e $ct1 : t1* (ref null $ct1) -> t2*
-- if tag $e : eps -> t*
-- if $ct1 ~~ cont $ft1
-- if $ft1 ~~ func t1* (ref null? $ct2) -> t*
-- if $ct2 ~~ cont $ft2
-- if $ft2 ~~ func t2* -> t*

on $e switch : t*
-- if tag $e : eps -> t*

What this shows is that, mostly, the side conditions move from handler to switch.

Obviously, the latter version is a bit more complicated, because it requires a new instruction besides suspend. It's also a bit weird that the tag never materialises a tagged value semantically, but is used essentially as a typed prompt only. The continuation and its arguments are passed to the handler and the target through a kind of side channel.

I think this could still be transformed into regular handlers, but only via a global transformation, since we need to expand each switch tag with multiple ones, one for each continuation type it's used with.

What bothers me about that, though, is that the handler conceptually has to forward values whose type and shape it doesn't know. In an implementation that would generally require a uniform value representation on the handler side (and the continuation's arguments), unless the switching code is always inlinable at the switch side, where the types are known. That strikes me as a severe constraint on implementations.

[conrad-watt]

What bothers me about that, though, is that the handler conceptually has to forward values whose type and shape it doesn't know. In an implementation that would generally require a uniform value representation on the handler side (and the continuation's arguments), unless the switching code is always inlinable at the switch side, where the types are known. That strikes me as a severe constraint on implementations.

I'm also a bit concerned about this, although I am somewhat drawn to the idea (in @tlively's version) that "child" stacks wanting to switch using some handler as a base can just coordinate between themselves on their continuation types instead of needing to install all their types as tags in the handler.

Do we have any precedent, either from EH, or from other language runtimes implementing continuations/coroutines/effects/exceptions regarding how common the inlining approach is?

[tlively]

• Nothing seems to depend on rt being present in the typing of switch, so I think we can just drop it.

When I was playing around with SpecTec, it errored out whenever I tried to make rt part of the preceding t*, so I got into the habit of keeping it explicit, but otherwise I agree.

• The tag merely fixes the result type of the handler, so it would be more natural to require its parameters to be empty and use its result for the result.

Originally I used the parameters because the tags could be used for normal suspends and resumes as well, so the types sent by the switch had to be in parameters just like they are in suspends, but now that we've agreed to keep tags for switching and suspending separate, either parameters or results would work. I agree that using the results is more intuitive.

I am somewhat drawn to the idea (in @tlively's version) that "child" stacks wanting to switch using some handler as a base can just coordinate between themselves on their continuation types instead of needing to install all their types as tags in the handler.

This property is very important for use cases where there is a single top-level handler that is part of the generic language runtime (e.g. perhaps part of a precompiled system library), but then source-level code gets lowered to arbitrary symmetric continuation types depending on what types are being passed around in the source. Requiring that system library to know all the types is less modular and would be a regression in modularity for this use case compared to Bag-o-Stacks, which does not have any handlers to coordinate on.

Do we have any precedent, either from EH, or from other language runtimes implementing continuations/coroutines/effects/exceptions regarding how common the inlining approach is?

Thread scheduling systems run the scheduler "inline" on the source thread in the implementation of yield to find the next thread to execute. In Bag-o-stacks, switching was "inline" by construction because there were no handlers, and at least V8 would have been happy to implement that. I would claim that the expected implementation of suspend and exceptions is "inline" in the same way because all the work is in finding the handler, and that's done before switching to the handler. All of these non-local control primitives do all the work to find the destination "inline," then execute as simple a jump as possible to actually get there. switch should work the same way, and expecting any code to be run at the handler only makes sense if you desugar it into two jumps, which no high-performance implementation would want to do.

[tlively]

I realized that if we’re distinguishing symmetric switches with both new handlers and a new switch instruction, then there’s no need to use a separate tag attribute. All the necessary type constraints at the resume can come from the handler rather than the tag.

[rossberg]

@tlively, yes, that was my question in my last comment, and why I omitted it from the rules.

[tlively]

Closing this as resolved. Thanks, everyone!