Interaction between session-typed communication and effects is broken

[dhil]

It is possible to break Links by using a combination of session-typed communication, multi-shot continuations, and exceptions. The gist is that with multi-shot continuations is possible subvert the linear type system by duplicating a linear channel. The program below illustrates two problems:

• Session fidelity is broken in the presence of multi-shot continuations. It is possible to deadlock session-typed concurrency.
• Type-safety is broken in the presence of multi-shot continuations and exceptions, giving rise to the slogan "Well-typed Links program can go wrong!"

# Breaking Links
# D. Hillerström, S. Lindley, and L. White

# Breaking session fidelity.
# Invoke the resumption twice to inadvertently perform two receives
# over a session-typed channel !Int.end.
fun deadlock() {
  var ch = fork(fun(ch) {
     var ch = send(42, ch);
     ignore(ch)
  });

  handle({
    # Nondeterministic choice.
    ignore(do Flip);
    var (i, ch) = receive(ch);
    println("Int: " ^^ intToString(i));
    ignore(ch)
  }) {
    case Return(_) -> ()
    case Flip(resume) ->
      resume(true); resume(false)
  }
}

# Breaking type safety.
# Inadvertently send two integers over a session-typed channel
# !Int.!String.end by using multi-shot continuations and exceptions.
fun unsound() {
  var ch = fork(fun(ch) {
     var (i, ch) = receive(ch);
     var (s, ch) = receive(ch);
     println("Int: " ^^ intToString(i));
     println("String: " ^^ s);
     ignore(ch)
  });

  handle({
    # Nondeterministic choice.
    var msg = if (do Flip) 42 else 84;
    var ch = send(msg, ch);
    # Throws an exception
    ignore(do Fail);
    var ch = send("foo", ch);
    ignore(ch)
  }) {
    case Return(_) -> ()
    case Fail(_) -> ()
    case Flip(resume) ->
      resume(true); resume(false)
  }
}

It is an open research question how to reconcile linear resources and first-class control effects. Thus it is hardly surprising that our implementation is broken.

[SimonJF]

This makes me very sad, but well-spotted. The fact that it's an open research question makes it slightly better, but it's still a shame.

At a high level, I suppose what we'd want to do is mark a resumption as linear if any invocation of its associated operation appears in a linear context.

A conservative fix would be to ensure that operations can only be invoked in an unrestricted context. This would break session exceptions; the translation relies on cancelling the endpoints in a continuation.

[dhil]

This makes me very sad [...]

Don't be. These two bugs are great news; there is research to done!

At a high level, I suppose what we'd want to do is mark a resumption as linear if any invocation of its associated operation appears in a linear context.

I am inclined to believe that operations should be annotated as to whether they admit an affine, linear, or unrestricted interpretation.

[SimonJF]

I am inclined to believe that operations should be annotated as to whether they admit an affine, linear, or unrestricted interpretation.

A (checked) annotation certainly sounds like a sensible solution.