Skip to content

Getting Started

A Token Server Program in Erlang

Let us consider a token server program consisting of a single process that handles client requests for obtaining integer identifier tokens. The server blocks and waits for requests sent as asynchronous messages. These messages are addressed to the server using its PID, and deposited in the server mailbox that buffers multiple client requests. The token server unblocks upon reading a message from its mailbox. In our client-server protocol, messages contain the command 0, signifying a new token request, and the client PID to whom the corresponding server reply should be addressed.

Our token server program is implemented as the Erlang module token_server that can be found under examples/erlang/src.

1
2
3
4
5
6
7
8
9
start(N) ->
  spawn(?MODULE, loop, [N]).

loop(OwnTok, NextTok) ->
  receive
    {Clt, 0} ->
      Clt ! NextTok,
      loop(OwnTok, NextTok + 1) % Increment token.
  end.

token_server:loop/1 encapsulates the token server logic that is spawned by some other launcher process (e.g. the Erlang shell) that invokes token_server:start/1 for some integer argument Tok. This argument Tok is the private server token that should never be leaked.

The spawned server consumes a message request from its mailbox via the receive expression on lines 5-9, and pattern matches against the new token request operation 0.

Every request fulfilled by the server results in a corresponding reply that it sends to the PID of the client instantiated in variable Clt, line 6. The server uses the parameter NextTok of loop/2 to track the current token number; OwnTok contains the private token of the token server itself. After handling a request 0, the server executes loop/2 to recommence the process loop and service the next client request, incrementing the next token value accordingly (line 8). Note that our server is designed not to terminate.

Safety properties

There are a number of properties we would like the server execution to observe. For example, the server loop does not control the initial value of Tok that an invocation to token_server:start/1 provides. We could, therefore, require that:

(P1)    Failure does not occur when the server is stated with its identifier token.

Similarly, we would expect that

(P2)    The server starts with its correct identifier token of 1,

and that

(P3)    The token 1 is not leaked by the server in reply to a client request.

both hold. These properties are data-dependent, which makes them hard to ascertain using static techniques such as type systems.

The properties mentioned thus far phrase the correctness requirement as a guarantee that the program must always provide. Such properties are called safety properties, since they stipulate that “for any sort of behaviour that the program can do, nothing bad ever happens.” As a consequence of this condition, showing that a program violates a safety property entails finding just one instance of a program execution that exhibits bad behaviour. Producing this evidence is enough of a proof that the program under scrutiny is not safe with respect to the property in question.

The next section explains how these properties can be expressed in a logic that precisely and unambiguously establishes the behaviour program executions must comply with.