OEP

170

Title

Two-way protocols

Summary

Provide a cleaner language binding for client-server relationships

Owner

Adam Sampson <ats@offog.org>

Status

Proposed

Date-Proposed

2008-02-25

Keywords

language channels mobiles client-server protocols

At the moment, client-server relationships between processes are implemented using channel bundles containing request and response channels, each of which has its own (usually variant) protocol. There is no higher-level way of describing the two-way protocol involved in a client-server conversation, and as a result the compiler cannot enforce the correct order of messages. Furthermore, the current approach requires quite a lot of "boilerplate" code for each client-server type.

It would be cleaner to add two-way protocols to the occam-pi language. For example, you could define a two-way protocol like this (based on the SJ syntax):

PROTOCOL AGENT
  CASE
    move!; VECTOR2 -> (ok? | suspend? -> suspended!; AGENT.INFO)
    look! -> view?; VIEW -> return.view!; VIEW
    quit!
:

or perhaps something like this, taking advantage of indentation (although I think the first CSP-ish form is clearer):

PROTOCOL AGENT
  CASE
    move!; VECTOR2
      CASE
        ok?
        suspend?
          suspended!; AGENT.INFO
    look!
      view?; VIEW
        return.view!; VIEW
    quit!
:

or, to mirror the communication syntax more closely:

PROTOCOL AGENT
  ! CASE
    move; VECTOR2
      ? CASE
        ok
        suspend
          ! suspended; AGENT.INFO
    look
      SEQ
        ? view; VIEW
        ! return.view; VIEW
    quit
:

To declare a channel that carries it:

CHAN AGENT agent:

Communication must always be initiated by the ! end of the channel, so in client-server terms, it's the client, which matches the existing syntax for channel bundles. The syntax for communicating over channel ends now just looks like regular channel communication:

PROC move (CHAN AGENT cli!, VAL VECTOR2 velocity)
  SEQ
    cli ! move; velocity
    cli ? CASE
      ok
        SKIP
      suspend
        SEQ
          cli ! suspended; state
          running := FALSE
:

Note that messages can pass in both directions across this channel. We can use session types to implement this safely using a single underlying occam-pi channel: the protocol spec gets compiled into a state machine, and the type of the channel end includes the state that it's currently in, so we always know (at both ends) what communication we're expecting next. The compiler can statically check that the protocol is followed.

This also makes it possible to hand off a channel end to another process in the middle of a conversation ("delegation" in session type terms). To make that possible, you'd need to be able to label states, and be able to abbreviate a channel end in a particular state --

CHAN 
AGENT[accepted]

, for example.

Labelled states would also be useful for specifying conversations that you could get into in multiple ways (for example, entering a location and moving within it in Occoids), and for recursion (which SJ has a special syntax for).

The examples so far have been with static channels, but we'd want to be able to move them around too, so we'd need mobile regular channels to make this useful -- see OEP/164 for that proposal.

OEP/170 (last edited 2008-02-27 16:49:49 by ats)