Accidental capture in stack suspension

[eqrion]

I saw this topic come up several times in the CG in-person meeting but never saw it fleshed out.

With typed continuations, a suspending stack gives a control tag (which may be private to a module, or shared) that it should suspend to the nearest handler of on the stack. With fibers, a suspending stack must provide the ancestor fiberref to suspend to on the stack.

I heard concern that the typed continuations approach of suspending to nearest handler with a given control tag could lead to 'unwanted capture' (correct me if it was a different phrase, can't find any notes from the meeting).

Is it possible to get a concrete example of what this is and how it happens?

[fgmccabe]

In most plausible scenarios, the control tags will be declared once per language runtime, not once per usage. This is likely to lead to the situation where control tags are imported rather than declared locally.
In addition, accidental capture is a phenomenon that is associated with any dynamic scoping system. Exception handling suffers from the same issue.
For a quasi-concrete example, think about generating elements from a list of lists. The list generator will be a single function that is used 'twice' in this case: once for the list of lists, and again for each sub-list. When the generator yields an element, that yielded value must penetrate through to the original requester of the iteration; but unless you have specific tokens/careful programming, it may actually be caught by the inner generator. There are more details here but that is the general idea.

[eqrion]

I'm not sure I follow your example. Is it possible to write it using JS generator functions or some pseudo syntax?

[RossTate]

I wrote up a more detailed example for you in another thread.

[RossTate]

Sure. Good question. But let me give an example using just exceptions; the same issue arises for continuations and (other) effects.

Suppose you have a Java interface for sequences

interface Sequence<Element> {
    /* consumer is called for each element and throws an exception when done */
    void foreach(Consumer<Element> consumer);
}

The idea is that these sequences knowsbetter how to iterate through their elements than the consumer does, and so foreach gives the sequence control over the iteration process.

Here are two simple examples of such sequences:

class CountFrom implements Sequence<Integer> {
    private final int from;
    public CountFrom(int from) { this.from = from; }
    public void foreach(Consumer<Integer> consumer) {
        for (int i = from; true; i++)
            consumer.accept(i);
    }
}

class Empty implements Sequence<Integer> {
    public void foreach(Consumer<Integer> consumer) {}
}

Note that the loop in CountFrom can go on forever. But the expectation of the Sequence interface is that the consumer can throw an exception in order to bail out from the iteration process early. The following class is an example illustrating this pattern, using a (private) exception to only iterate through the first so many elements of the first sequence and then move on to the second sequence.

class AppendAfter<Element> implements Sequence<Element> {
    private final Sequence<Element> first, second;
    private final int amount;
    public AppendAfter(Sequence<Element> first, int amount, Sequence<Element> second) {
        this.first = first; this.amount = amount; this.second = second;
    }
    public void foreach(final Consumer<Element> consumer) {
        try {
            first.foreach(new Consumer<Element>() {
                private int count = amount;
                public void accept(Element element) {
                    if (count-- == 0)
                        throw new AppendAfterException();
                    consumer.accept(element);
                }
            });
        } catch (AppendAfterException e) {}
        second.foreach(consumer);
    }
    private static final class AppendAfterException extends RuntimeException {}
}

Now you can put these together to get some simple finite sequences. For example,

Sequence<Integer> simple = new AppendAfter(new CountFrom(0), 5, new Empty());
simple.foreach((Integer i) -> System.out.println(i));

will print 0 1 2 3 4 (each on its own line), just as you'd expect. (All these examples are working Java code.)

But when you try complex compositions, things go wrong. For example, you might expect

Sequence<Integer> ints = new AppendAfter(new AppendAfter(new CountFrom(0), 10, new CountFrom(10)), 5, new Empty());
ints.foreach((Integer i) -> System.out.println(i));

to print out 0 1 2 3 4, but in fact it prints out 0 1 2 3 4 10 11 12 13 14 ... (seemingly forever).

Why did that happen? Well, because we used dynamically scoped exceptions, our complex composition experienced an accidental capture. In particular, when the "outer" AppendAfter saw 5 elements had been enumerated, the consumer it gave to its first sequence threw an exception to break out of its loop, but unfortunately the "inner" AppendAfter caught that exception (mistaking it for the one that could be thrown the the consumer it gave to its first sequence), and so the inner AppendAfter moved to its second sequence while the outer AppendAfter was left in an invalid state.

Had we instead used lexically scoped exceptions—where the target destination is made explicit rather than dynamically searched for—such as in the following pseducode:

class AppendAfterFixed<Element> implements Sequence<Element> {
    private final Sequence<Element> first, second;
    private final int amount;
    public AppendAfterFixed(Sequence<Element> first, int amount, Sequence<Element> second) {
        this.first = first; this.amount = amount; this.second = second;
    }
    public void foreach(final Consumer<Element> consumer) {
        label: lexical_try {
            first.foreach(new Consumer<Element>() {
                private int count = amount;
                public void accept(Element element) {
                    if (count-- == 0)
                        lexical_throw label;
                    consumer.accept(element);
                }
            });
        } catch {}
        second.foreach(consumer);
    }
}

then our complex composition would have produced the expected output.

All this is to illustrate what accidental capture is and why dynamic scoping is not compositional. And note that dynamic scoping failed to compose even though I used a private nominal "event tag" (AppendAfterException). Adding effects to function types also doesn't fix the problem; this example is in fact typeable. The issue is that effect types for dynamically scoped effects only guarantees the effect is handled by someone; it does not guarantee that it is handled by the intended someone.

On the other hand, types for lexically scoped effects do guarantee effects are handled by the intended someone. This paper gives a language with effects and generics that can be given both dynamically scoped and lexically scoped semantics, and it proves that the lexically scoped semantics satisfies an extremely strong composability property (specifically relational parametricity) due to ensuring intended handling, and that the dynamically scoped semantics fails to satisfy this property due to accidental capture.

There's more to say on why to use lexically-scoped (i.e. explicit) semantics rather than dynamically scoped (i.e. searching and using some policy when multiple matches are present) semantics, but you just asked about accidental capture, and I'm guessing I've already given you more to ponder over than you were hoping for.

P.S; The above example was not contrived. For languages with generators, this is what happens behind the scenes when employing a valuable optimization to eliminate stack allocations in common usage patterns of generators, such as for each loops.

[eqrion]

Okay, thanks for this example.

If I understand it correctly, the relevant summary of what goes wrong for this proposal is:

1. AppendAfterFixed is aiming to be an abstract component that is arbitrarily composable
2. AppendAfterFixed.foreach will setup a handler for it's own 'control tag'
3. AppendAfterFixed.foreach will invoke an interface (which can be anything, including another instance of itself) and provide it a closure which attempts to suspend back to the handler from (2) using its 'control tag'
4. Choosing to compose as a: AppendAfterFixed(b: AppendAfterFixed) causes two handlers from step (2) to be set up, before the outer closure from step (3) is run. The outer closure runs and is erroneously captured by the inner one due to the unexpected stack layout.

My follow up question then is, does this happen with any of the critical use cases of stack-switching?

• Green threads
  • All examples of green threads I've seen rely on a top-level scheduler handler
  • Step (3) therefore sounds like attempting to call into a recursive scheduler handler, which sounds like a bug violating global assumptions.
  • It's also unclear why a scheduler would be invoked with a closure that would perform a yield to a different scheduler such as in step (3).
• Yield style generators
  • Invoking a generator function will setup a handler such as in step (2). I believe the control tag could be 1:1 with the generator function definition.
  • Yield can only happen in the called generator function, not in a closure passed to another function, so there's no chance for the yield to be captured by anything else.
  • If a generator invokes another generator, it must setup a handler for anything from the generator it's calling.
• Async/await
  • My assumption is this is the same as yield style generators.
• First class continuations
  • I know less about how this will be used.
  • Best guess is if the source language feature is nearly the same as the runtime feature, then any accidental capture is the fault of the source language feature.

Am I missing something?

[RossTate]

Choosing to compose as a: AppendAfterFixed(b: AppendAfterFixed) causes two handlers from step (2) to be set up, before the outer closure from step (3) is run. The outer closure runs and is erroneously captured by the inner one due to the unexpected stack layout.

The fixed version does not have accidental capture because it uses lexically scoped exceptions.

All examples of green threads I've seen rely on a top-level scheduler handler

In practice, there is no top level schedule handler. That is a device used to encode green threads in dynamic scope, and one that comes at a cost (e.g. an extra context switch on every thread switch). According to the language implementers we have spoken to the following is what actually happens: either the currently executing thread either has an obvious target (e.g. because it is sending a synchronous message to another thread) and directly switches to that target, or it is voluntarily yielding and runs the scheduler on the current green thread and then directly switches to the target returned by the scheduler.

Yield style generators

The paper gives an example of dynamic scoping causing accidental capture for yield-style generators. See Section 2.2.

Async/await and first-class continuations

In general, in any system with higher-order interactions between two components (such as WebAssembly, both within modules and across modules), dynamic scope causes composability issues due to accidental capture.

Am I missing something?

Dynamically scoped semantics can be encoded via lexically scoped semantics. This encoding is efficient in a manner that is already expressible in WebAssembly, and that encoding is how languages implement dynamically scoped features natively, since native environments only support lexically scoped semantics.

On the other hand, while lexically scoped semantics can be encoded via dynamically scoped semantics, it is inefficient as it generally requires more context switches and dynamically-scoped searches.

So why should we use dynamically scoped semantics when it is less efficient and has worse composability properties than lexically scoped semantics and when all language runtimes already know how to implement their features efficiently using lexically scoped semantics because that is what the hardware supports?

[titzer]

On the other hand, while lexically scoped semantics can be encoded via dynamically scoped semantics, it is inefficient as it generally requires more context switches and dynamically-scoped searches.

I'd like to see efficiency claims evaluated on implementations because in other proposals we've dithered too long on efficiency considerations that turned out to be mirages.

Concretely, if the typed continuations proposal gives rise to accidental capture or leads to a suboptimal encoding what is characterized here as lexically-scoped semantics, then that should manifest in concrete examples and concrete measurements.

[RossTate]

We have heard from multiple language teams that the encodings imposed by the typed continuations proposal are suboptimal. As an example, multiple language teams have reported that they found that moving from "scheduler at the top" to "scheduler in the green thread and then direct switch" resulted in appreciable performance improvements because it removes a context switch from every green-thread switch. More generally, the experience relayed is that removing context switches results in better performance. I believe it is undisputed that a lexically-scoped design involves, generally speaking, fewer context switches than the typed continuations proposal for a variety of features (and never involves more context switches). So, putting those two pieces together, it seems reasonable to deduce that the typed continuations proposal can at best match the performance of a lexically-scoped design and in various situations will be appreciably less efficient. If you have a scenario where you have reason to suspect the typed continuations proposal to work better, it would be useful to discuss it.

[slindley]

There still seems to be some confusion and misleading information in
this discussion. I'll attempt to partially address some (but by no
means all) of it here.

First, it should be stressed that the question of how to select a
handler when suspending is almost entirely orthogonal to the question
of to what degree continuations are typed. This was one of the points
of Andreas's talk about the design space at the recent CG meeting in
San Francisco. The typed continuations proposal in its basic form
suspends to the nearest handler with a matching event tag. However,
one of the extensions described in the proposal is to also support
suspending to a specific named handler (also with a matching event
tag). Both modes of selecting a handler (unnamed and named) are
useful.

Issues with "accidental capture" of effects (including exceptions) in
source languages are the subject of much recent and ongoing research
including my own. (You can roughly think of an effect as corresponding
to an event tag, though in some systems such as Koka, an effect in
fact corresponds to a collection of such tags.) The fundamental issue
is not really about dynamic scoping but rather the inability to
encapsulate effects. In our research my coauthors and I refer to the
problem as the effect pollution problem [3].

(It is true that if we only have a second-class notion of exception,
as in languages like Java, then that hinders effect
encapsulation. But, for example, in languages like SML and OCaml that
have generative exceptions it is straightforward to encapsulate
exceptions, and in particular to write code that behaves like Ross's
AppendAfterFixed.)

It is worth bearing in mind that though effect pollution can be a
problem in source languages, it is not entirely clear-cut to what
extent it is necessarily a problem for low-level target languages like
Wasm, in practice.

There are many solutions to the effect pollution problem. Here are a
few.

• There are various forms of so called "lexically-scoped handlers"
  (these are not all the same thing [2, 6, 9]). Often these are
  implemented using some form of global capability-passing or
  evidence-passing transformation along with named handlers.

• The first version of the Eff language [1] solved the effect
  pollution problem with effect instances. These allow each clause
  of a handler to be associated with not only a tag, but also an
  instance. To avoid clashes we can ensure that a fresh instance is
  associated with each handler.

• OCaml 5 supports generative effects (and generative exceptions) via
  local modules. This means that we can always generate a fresh tag
  that is guaranteed to be unique and so cannot possibly get handled
  by the wrong handler. OCaml 5 supports only unnamed handlers, both
  in the front-end and the back-end, and its performance is
  competitive with Rust and Go [5].

• Koka and Frank provide a masking operator that allows effects to be
  hidden in such away that clashes are avoided. (Incidentally, Koka's
  implementation also uses an evidence-passing implementation under
  the hood, but the source language primarily uses plain effect
  handlers, and they are not restricted to be "lexically scoped" - and
  the compilation strategy works fine in general, despite the mistaken
  claims of the ICFP 2020 Koka paper [6], which were rectified in the
  ICFP 2021 Koka paper [8].)

• The C++ effects library [4] supports both unnamed and named handlers
  (just like the typed continuations proposal and its extension).

• There is an experimental extension of Koka with named handlers in
  the source language [7].

It may be illuminating to look at the implementations of generators in
OCaml 5 and in the C++ effect library.

OCaml 5:

https://github.com/ocaml-multicore/effects-examples/blob/master/generator.ml

Lines 56-58 are the crucial ones. They ensure that the Next effect
is unique by placing it inside a local module.

C++ effects library [4]:

Generators are described in Section 2.6.

In neither case is any aspect of effects exposed to the user of the
implementation, and distinct generators are entirely independent. The
OCaml 5 implementation uses generative effects to ensure this; the C++
effects implementation uses a named handler.

References

[1]
Andrej Bauer, Matija Pretnar.
Programming with algebraic effects and handlers. JLAMP 2015.
https://www.sciencedirect.com/science/article/pii/S2352220814000194

[2]
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, Filip Siezckowski.
Binders by day, labels by night: effect instances via lexically scoped handlers. POPL 2019
https://dl.acm.org/doi/10.1145/3371116

[3]
Lukas Convent, Sam Lindley, Conor McBride, Craig Mclaughlin.
Doo bee doo bee doo. JFP 2020.
https://www.cambridge.org/core/journals/journal-of-functional-programming/article/doo-bee-doo-bee-doo/DEC5F8FDABF7DE3088270E07392320DD

[4]
Dan Ghica, Sam Lindley, Marcos Maroñas Bravo, Maciej Piróg.
High-level effect handlers in C++. OOPSLA 2022.
https://dl.acm.org/doi/abs/10.1145/3563445

[5]
KC Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer, Anil Madhavapeddy.
Retrofitting effect handlers onto OCaml. PLDI 2021.
https://arxiv.org/abs/2104.00250

[6]
Ningning Xie, Jonathan Brachthäuser, Daniel Hillerström, Philipp Schuster, Daan Leijen.
Effect handlers, evidently. ICFP 2020.
https://dl.acm.org/doi/10.1145/3408981

[7]
Ningning Xie, Youyou Cong, Kazuki Ikemori, Daan Leijen. OOPSLA 2022.
First-class names for effect handlers.
https://dl.acm.org/doi/10.1145/3563289

[8]
Ningning Xie and Daan Leijen.
Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C. ICFP 2021.
https://dl.acm.org/doi/abs/10.1145/3473576

[9]
Yizhou Zhang and Andrew Myers.
Abstraction-safe effect handlers via tunneling. POPL 2019.
https://dl.acm.org/doi/10.1145/3290318

[RossTate]

None of those solutions are present in the (unextended) typed continuations proposal. They are encodable in the typed continuations proposal, but the encodings necessarily involve additional context switches than what the source material requires. For example, one way to fix AppendAfter while using only dynamically scoped exceptions is the following lexical-to-dynamic encoding for exceptions:

class AppendAfterEncoded<Element> implements Sequence<Element> {
    private final Sequence<Element> first, second;
    private final int amount;
    public AppendAfterEncoded(Sequence<Element> first, int amount, Sequence<Element> second) {
        this.first = first; this.amount = amount; this.second = second;
    }
    public void foreach(final Consumer<Element> consumer) {
        final AppendAfterException identifier = new AppendAfterException();
        try {
            first.foreach(new Consumer<Element>() {
                private int count = amount;
                public void accept(Element element) {
                    if (count-- == 0)
                        throw identifier; // object closes over final "identifier" variable in context
                    consumer.accept(element);
                }
            });
        } catch (AppendAfterException e) {
             if (e != identifier)
                 throw e;
        }
        second.foreach(consumer);
    }
    private static final class AppendAfterException extends RuntimeException {}
}

But this encoding is worst-case quadratic with respect to the number of non-local control transfers AppendAfterFixed uses, as are many of the more straightforward encodings of the constructs you listed (which all generally would down to the same "allocate something beforehand and then run a user test at each capture site to figure out if the capture was accidental").

For many of the constructs, if you want to avoid this quadratic worst-case, you're essentially forced to implement your own dynamic scope (which is easy to do) and emulate lexically scoped direct switching. So why not just provide lexically scoped direct switching in the first place? It can support all of the constructs you listed without any additional context switches.

---

However,
one of the extensions described in the proposal is to also support
suspending to a specific named handler (also with a matching event
tag). Both modes of selecting a handler (unnamed and named) are
useful.

There are more modes than just these two. Bidirectional algebraic effects (such as rejections in promises) are another mode. But all of these modes can be implemented using only named handlers. This implementation is fairly easy (the application just implements dynamic scope on its own, e.g. by maintaining a linked-list data structure of stacks) and efficient (e.g. no more context switches than in the source program). On the other hand, named handlers and bidirectional unnamed handlers cannot be encoded using just unidirectional unnamed handlers without increasing the number of context switches.

So why should a wasm engine provide both named and unidirectional unnamed handlers when the application can straightforwardly implement the latter in terms of the former (and implement a bunch of optimizations on top of it! like tail-resumption optimization) or straightforwardly implement its own construct (such as the many you listed) in terms of the latter (but not necessarily the former)?

[dhil]

On the other hand, named handlers and bidirectional unnamed handlers cannot be encoded using just unidirectional unnamed handlers without increasing the number of context switches.

Uh-oh. You should be more careful about making such statements about expressiveness. Using the number of context switches as a measure is dubious, because it is possible to implement suspend and resume such that each requires exactly one context switch irrespective of the length of the active stack chain (i.e. nesting depth of handlers). I wrote such an implementation two years ago in C. As such, the "number of context switches" is a non-informative measure.

So why should a wasm engine provide both named and unidirectional unnamed handlers when the application can straightforwardly implement the latter in terms of the former (and implement a bunch
of optimizations on top of it! like tail-resumption optimization) or straightforwardly implement its own construct (such as the many you listed) in terms of the latter (but not necessarily the former)?

It might be "easy" if your backend is already set up for prompt-passing style. Otherwise, you essentially need to perform some variation of continuation-passing style on your intermediate representation in order to recover modularity, which consequently forces you into accepting new calling convention.

[RossTate]

Using the number of context switches as a measure is dubious, because it is possible to implement suspend and resume such that each requires exactly one context switch irrespective of the length of the active stack chain (i.e. nesting depth of handlers).

This seems to miss the point. That implementation strategy (which is what I have expected the typed-continuations proposal would use), enables you to suspend to the most immediate matching unnamed handler with a single context switch. But what I said was "named handlers ... cannot be encoded using just ... unnamed handlers without increasing the number of context switches". The issue is that, if the system only supports unnamed handlers (as in the typed-continuations proposal), then named handlers have to be approximated by unnamed handlers. As a consequence, when you want to suspend to a named handler, you can only suspend to the most immediate unnamed handler approximating that named handler. Then you have to run application code to determine if the named handler for that suspension point is the one you were looking for, or if it accidentally belongs to another named handler with the same approximation, in which case you have to suspend again. Thus, except when you're lucky, it generally takes multiple context switches with unnamed handlers to implement what would have been a single context switch with a named handler.

I also said the same issue for bidirectional algebraic effects. The issue here is that the handler of the effect can be inside another continuation. So first you have to switch to that continuation, and then you have to perform the dynamically scoped suspension. So two context switches when there could have been one.

Another example is direct switching used in implementations of green threads. You can implement this with dynamic scope via a suspend and a resume, but that requires two context switches to perform one direct switch. The typed-continuations proposal does describe a possible extension for this feature, but note that it uses named (i.e. lexically scoped) handlers. This is because it would be unsound to do so with just dynamic scoping (the unnamed handler is expecting some return value for the continuation it resumed, and there's no way to know at the site of the switch_to instruction what that type is in order to ensure it matches the return type of the continuation you're switching to).

It might be "easy" if your backend is already set up for prompt-passing style.

I know of four ways for an application to implement specifically dynamic scope. One of them is already fairly common in WebAssembly. None of them need you to perform CPS on your IR in order to recover modularity. (Some of them do require you to import something from a common "runtime" module, but so does the typed continuations proposal: the common effect tag used across your language's compiled modules.) If this is a concern, then it might be a worthwhile topic for a new Discussion.