Improving channel types in Steel

A more generic interface to channels

The current channel example from the SteelCore paper hints at how we might structure the verification of message-passing programs.

However, it has a number of obvious limitations so far.

• The current example only supports simplex, synchronous channels.

  The paper sketches how we might make then duplex and asynchronous. I don't want to say too much more about that here: making them asynchronous is pretty easy. Duplex with 2-party sessions is more interesting, but also not that hard.

• Multi-party sessions: Beyond 2 parties, writing specifations to orchestrate message-passing interactions among multiple parties is much more interesting and open ended. It would be interesting to read, say, https://www.doc.ic.ac.uk/~yoshida/multiparty/multiparty.pdf and to also talk to folks like Karthik and Cedric who have worked quite a lot on this topic before, including for cryptographically secure multi-party sessions.

• Higher order channels: Exchanging slprops and channels over channels. This is the part I want to focus on for this note.

Higher order channels

Consider a simple scenario for mixing message-passing concurrency with shared state. In this setting, one might like to exchange references to mutable memory over a channel. For example, participant allocates a reference, uses it for a while, and then sends the reference across a channel to another participant together with some slprop assertion about that reference, e.g., a fractional permission to that reference.

As another example, consider sending a channel over a channel, enabling dynamic topologies of communication in the style of the pi calculus. With our current API, channels are just value types, so they can already be sent over other channels. However, a channel is only useful when accompanied by an slprop permission authorizing its use according to a given protocol.

The current channel API does not support these scenarios---in particular, it's not yet possible to transfer an slprop across a channel.

For reference, here's the current interface to the channel API (partial):

val send (#p:prot) (c:chan p) (#next:prot{more next}) (x:msg_t next)
  : SteelT unit (sender c next) (fun _ -> sender c (step next x))


val recv (#p:prot) (#next:prot{more next}) (c:chan p)
  : SteelT (msg_t next) (receiver c next) (fun x -> receiver c (step next x))

Note that one the send side, the sender has to prove that the channel is currently in the sender c next state, allowing them to send a x:msg_t next. However, the precondition slprop does not expect any property about x, the actual value being sent over. Likewise, on the recv side, the receiver obtains a well-typed value x:msg_t next but the provided slprop says nothing about x itself, aside from using it to transition the state machine.

I would instead like an interface such as the following:

val send (#p:prot) (c:chan p) (#next:prot{more next}) (x:msg_t next)
  : SteelT unit (sender c next `star` slprop_of next x) (fun _ -> sender c (step next x))


val recv (#p:prot) (#next:prot{more next}) (c:chan p)
  : SteelT (msg_t next) (receiver c next) (fun x -> receiver c (step next x) `star` slprop_of next x)

The main addition here is that send expects the sender to yield an slprop_of next x to the channel, so that the channel can transfer this slprop to the receiver when delivering it the message.

How to achieve this interface is the question:

• A first attempt would be to enhance the type of protocols prot so that at each Msg action we represent not only the type of the next message, but also an slprop associated with it, i.e., something like this:

type slprot : Type -> Type =
| Return  : #a:Type -> v:a -> slprot a
| Msg     : a:Type -> p:(a -> slprop) -> #b:Type -> k:(a -> slprot b) -> slprot b
...

Note the addition of the p: a -> slprop field in the Msg case. However, while this may be a convenient means of specification, it is incompatible with our current implementation strategy. Putting an slprop into Msg raises the universe of slprot too high, making it impossible to store a slprot in (ghost) state.

So, what could we do instead? Some initial thoughts:

One of the strong points of the current channel implementation is that it provides a verified implementation of all protocols expressible in the prot type once and for all. Doing this requires manifesting the predicates sender c next etc. in terms of some instrumented ghost state.

• Go meta: If we are to give up on the once-and-for-all style, we could allow the user to specify protocols with embedded slprops (something like slprot) and then to metaprogram implementations of the channel API specialized to the use of a given slprot. This might allow us to avoid storing these slprots in the heap.

• Go generic: Another approach could be to retain the once-and-for-all style, but to limit the slprops storable within an slprot to be from some family of slprops that are denotable in a sufficent small universe of codes. For example:

   type slprot (#c:Type0) [| d:slcode c |] : Type -> Type =
   | Return  : #a:Type -> v:a -> slprot d a
   | Msg     : a:Type -> p:(a -> c) -> #b:Type -> k:(a -> slprot d b) -> slprot d b
   ...
  

  The type of slprots is parameterized by a typeclass of slcodes, a type c paired with its denotation as_slprop : c -> slprop of codes c to slprops.

  This should make the universe of slprop d b small enough to continue with our current implementation strategy at the expense of carring around this typeclass (which may not be so bad), and also limiting the expressiveness of slprot to use slprops that are sufficiently small---however even that may not be too bad, since each protocol can chose its own class of slcodes, suited for its needs (we do not need a universal language of codes for all slprops).