Sunday, February 15, 2009

JSON protocols (part 1)

For a long time I have been interested in describing protocols. In 2002 I published a contract system called UBF for defining protocols. This scheme was never widely adopted - perhaps it was just to strange...

I have revised UBF and recast it in a form which I call JSON Protocols - since JSON is widely implemented, this method of described protocols might be more acceptable.

What's the problem?

Client and server interaction should be regulated by some kind of contract that is independent of both the client and server. If the client-server interaction fails, then it should be evident by examining the contract which of the parts in the system has failed. Is the problem in the client or the server?


To simplify our problem we will assume that the client and server interact by exchanging JSON messages and we will add a form of contact that will allow us to check that the sequence of messages is correct.

The File Server Contract

We'll start with a simple example and build a formal description of a file server. I'll use the familiar notion of a finite state machine to describe the operations of the server.

The behaviour of the server is completely specified by a set of
4-tuples of the form:

State x RequestMessage -> ResponseMessage x StateOut

We'll start our specification of the file server somewhere in the middle of a session. We'll assume that users must be authenticated, but we'll show how they are authenticated later.

Let's assume the server is in the state ready - meaning it is ready to accept a request. We can start by defining two state transitions:

ready x getFile -> file x ready;
ready x getFile -> noFile x stop;

This means that if our machine is in the state ready and receives a getFile message it will respond by either sending a file message and transitioning to the ready state or it will respond with a noFile message and transition to the stop state.

Here getFile and file are messages and ready and stop are states.

Attached to the message is some data structure that accompanies the messages.
We can defined these data structures as follows:

data[getFile] = {fileName:string};
data[file] = {fileName:string, fileData:string};

Having defined the data we turn to the wire protocol - what data is actually sent between the client and the server? To answer this we will give a JSON example.

Suppose we want to fetch a file called "index.txt", assume also that the content of the file is "abc" then our contract says that the following JSON terms must be exchanged:

Request =
{msg:"getFile", data:{fileName:"index.txt"}}


Response =
{msg:"file",
data:{fileName:"index.txt", fileData:"abc"},
state:"ready"}
Note that exactly this interchange must take place. If either of the messages is incorrectly typed the contract checker can detect the error and determine whether the client or server has violated the contract.
There is a simple relation between the format of the message that is actually exchanged on the wire and the, algebraic specification of the messages.

[note - I have taken liberty with JSON notation here and omitted the quote marks preceding the tags in the object name, strictly I should have written {"msg":"file" etc., but I have written msg:"file"]

What happens if a file doesn't exist? We had a rule for this:

ready x getFile -> eNoFile x stop;

The reply message eNoFile has no associated data, so no data description is necessary.

As an example, suppose we request the file "badfile" which does not exist. This is what we would see "on the wire".

Request = {msg:"getFile", data:{fileName:"badfile"}}
Response = {msg:"eNoFile", state:"stop"}

Observe that the eNoFile message has no associated data.

Why do we send the state back in the response message?

This is to avoid the situation where the server performs a silent state change that cannot be observed by the client. Suppose we have two rules:

a x s1 -> c x s2
a x s1 -> c x s3

When we send an a message we always receive a c message, but we cannot tell if the server changed to state s2 or s3. To make things clearer we always include the new state in the reply.

Now that we've seen what happens in the middle of a session, we can include details of the login and authentication phase.

login x start -> challenge x wait;
response x wait -> ok x ready;
response x wait -> badpassword x stop;

data[login] = {name:string};
data[challenge] = {salt:string};
data[response] = {md5:string};

Once we are ready we might want to list files:

ready x listFiles -> files x ready;
ready x logout -> stop;

data[files] = [{filename:string}];

This completely (and formally specifies the behaviour of a file sever)

Adding time

We can easily add time to our specification:

read x getFile -> file x read within 2 seconds;

This means that we must respond within 2 seconds.

What else?

We need some meta-information, the version number and name of the protocol, and an introspection mechanism.

Notation

I've been a bit sloppy with notation here and used a notation that I hope is 'self-evident'. The state machine syntax is trivial:

StateIn x MessageIn -> MessageOut x StateOut;

The data notation is less obvious:

data[XXX] = {tag1: type1, tag2: type2 ...}

denotes a JSON message of the form:

{"msg":"XXX", data:{"tag1":Data1, "tag2": Data2, ...}}

Where Data1 is of type type1 and Data2 is of type type2. Observe I have only
used the type "string" in my examples, but this is easily extended to JSON primitive types, enumerations and sequences of types.

I also used the notation [X] (in the definiton data[files] =
[{filename:string}]. [X] means an array (or sequence) of type X.

Contract Checking

Now what we have our state machines and message we can easily write a contract checker.

Given the state of the finite machine and then next message we can easily check if the client and server are correctly responding to protocol messages as required by the specification. Each message has a data type specification can easily be checked.

Comments on this are welcomed.

In Part 2 I will post Erlang bindings for the protocol specification and code for a contract checker.

Other implementers might like to implement bindings and contract checkers for their favorite languages. having done this we could start writing multi-language applications based on formal and checkable contracts.




12 comments:

Vincent Murphy said...

Joe-

I am an admirer of your work and don't mean to be 'smart', in fact I may be missing something, but isn't this a re-invention of HTTP?

Ready and Stop states are handled by TCP, getFile is HTTP GET, File is 200, noFile is 404, 201 is Updated.

In particular, including protocol information (getFile) as part of the message can be seen to be conflating the application protocol and the document payload. We RESTafarians have spent a good few years now trying to discourage that. :)

Harake said...

The response from the getFile request is fileData:"abc". This seems like a very naive way of looking at it... I mean how would you send a 1GB file for example? If you would chunk it up, how would you handle events from the server? Or rather how would you handle chunks?

Or is it suppose to handle request-response type of protocols only?

/Mazen

Anonymous said...

@Harake, First it is example :)

Second you can chunk data introducing addtionall temporary states (like "moredataready" ), and messages getMore. Just idea.

Luke Sutton said...

I think you guys are missing the point. This is a hypothetical design, performance or duplication of existing standards is irrelevant.

Martin S said...

Hello Joe,

first and foremost I like your formal approach to protocols.

I like your approach to describing a protocol. I am a fan of your data notation
data[XXX] = {tag1: type1, tag2: type2 ...}

which leads to describing a protocol in json terms. That is, we can think of a server that self-publishes its protocol / capabilites encoded in json (similarly to e.g. protobuffs).

I don't think we need to explicitly add the state of the server in the response. Imho a server's state must always be a function of the "chain of commands" that a client send him, that is the protocol must be deterministic. What you describe with

> a x s1 -> c x s2
> a x s1 -> c x s3

is non-determinism (imho) and should be considered a protocol bug.

Steve Davis said...

@Vincent - HTTP is a stateless protocol, so it doesn't make sense to declare non-existent state. Also HTTP is a text-based protocol and DOES include all "protocol information" in the message GET, HEAD, POST, etc not to mention all those HTTP Headers. TCP stop and ready are for packet exchange right? ...so not really anything to do with the data payload. A long way of saying, I don't see the REST argument applies here?

On another note - it's slightly odd to me is that JSON is essentially a text-based protocol also but then implicitly includes the idea of a "string" as part of the text.

I'm looking forward to part 2, and the implementation of contract checking. But I"m not yet convinced that JSON would be superior or even equal to UBF.

Joe Armstrong said...

@Harake

getFile x ready -> bigFile x sending;

sending x '$empty' -> chunk x sending;
sending x '$empty' -> done x ready;

data[chunk] = {part:integer, val:string}

'$empty' is the empty message - ie in response to no message you spontaneously emit a message and change state.

LeHoff said...

@Joe: I have looked into UBF and I think the major issue for an Erlanger like me was that the distribution was merely a directory with a bunch of files in it. That kind of distribution only appeals to Innovators (http://en.wikipedia.org/wiki/File:Technology-Adoption-Lifecycle.png) and possibly some of the "Early Adopters".

@Martin S: I second your comments about the way to describe a protocol, but I beg to differ on the inclusion of the state in the replies. I had my issues with that inclusion in the first place, but after reading the documents on UBF I surrendered. The inclusion of the next state elegantly captures a protocol between two entities and helps you ensure that the implementation on both sides are correct by giving you something to check. The introduced non-determinism is not a problem in my view since it allows you to give some internal state from the clients, e.g., if the file is there or not for the getFile example. If some of the protocols I am dealing with on my day time job were specified like Joe suggests my life would be a lot easier... hmmm, on the other hand I could be out of a job... let's leave it at that!

Steve Davis said...

btw surely...

Request =
{msg:"getFile", data:{fileName:"index.txt"}}

should be...

Request =
{"msg":"getFile", "data":{"fileName":"index.txt"}}

...and so on?

BR /Steve

musk said...

Why are you dropping the UBF specs and going for this JSON? I think the UBF spec looks pretty good and seems to be a nice consistent way of writing out a protocol. Maybe if you updated the page some more and provided more language bindings for the contract checker it would get more adoption. Having to work with SOAP and WSDL at work I really think we need a good alternative that is less verbose and more concise.
BTW have you considered adding security features into the protocol language? Something along the lines of message signing. Or do you think this is something which should not be handled at the protocol layer?

Anonymous said...

my gut reaction to seeing any description of a wire protocol that represents a number as a string of digits is to stop reading. if that reaction is common among people in our field of study that would help explain why your ideas regarding protocols are not well-received.

Have you considered other encodings for numbers? This is a context where I would consider sacrificing some degree of human readability.

M-MZ said...

Everybody loves to design protocols don't they. :)

Personally I like the ideas expressed in the original UBF document.

What I also think can also be a problem, apart from the "strange" UBF is the use of, more or less, static types in de definition of the protocol. Types can sometimes be a hurdle too.

It would be nice if the protocol definition could be dynamically typed, and the protocol checker could work with that.