As we said before, TCP does not preserve message boundaries; to guarantee it we may use a filter class BufferedSocket, defined in the module BUFFERED-SOCKET, which is described here. We interact with buffered sockets in the same way we interact with sockets, with the only difference that all messages in the module SOCKET have been capitalized to avoid confusion. Thus, to create a client with a buffered socket, you send socketManager a message
CreateClientTcpSocket(socketManager, ME, ADDRESS, PORT)
instead of a message
createClientTcpSocket(socketManager, ME, ADDRESS, PORT).
All the messages have exactly the same declarations, the only difference being their initial capitalization:
op CreateClientTcpSocket : Oid Oid String Nat -> Msg
[ctor msg format (b o)] .
op CreateServerTcpSocket : Oid Oid Nat Nat -> Msg
[ctor msg format (b o)] .
op CreatedSocket : Oid Oid Oid -> Msg [ctor msg format (m o)] .
op AcceptClient : Oid Oid -> Msg [ctor msg format (b o)] .
op AcceptedClient : Oid Oid String Oid -> Msg
[ctor msg format (m o)] .
op Send : Oid Oid String -> Msg [ctor msg format (b o)] .
op Sent : Oid Oid -> Msg [ctor msg format (m o)] .
op Receive : Oid Oid -> Msg [ctor msg format (b o)] .
op Received : Oid Oid String -> Msg [ctor msg format (m o)] .
op CloseSocket : Oid Oid -> Msg [ctor msg format (b o)] .
op ClosedSocket : Oid Oid String -> Msg [ctor msg format (m o)] .
op SocketError : Oid Oid String -> Msg [ctor msg format (r o)] .
Thus, apart from this small difference, we interact with buffered sockets in exactly the same way we do with sockets, the boundary control being completely transparent to the user.
When a buffered socket is created, in addition to the socket object through which the information will be sent, a BufferedSocket object is also created on each side of the socket (one in each one of the configurations between which the communication is established). All messages sent through a buffered socket are manipulated before they are sent through the socket underneath. When a message is sent through a buffered socket, a mark is placed at the end of it; the BufferedSocket object at the other side of the socket stores all messages received on a buffer, in such a way that when a message is requested the marks placed indicate which part of the information received must be given as the next message.
An object of class BufferedSocket has two attributes: read, of sort String, which stores the messages read, and bState, which indicates whether the filter is idle or active.
op BufferedSocket : -> Cid [ctor] .
op read :_ : String -> Attribute [ctor gather(&)] .
op bState :_ : BState -> Attribute [ctor gather(&)] .
sort BState .
ops idle active : -> BState [ctor] .
The identifiers of the BufferedSocket objects are marked with a b operator, i.e., the buffers associated with a socket SOCKET have identifier b(SOCKET). Note that there is a BufferedSocket object on each side of the socket, that is, there are two objects with the same identifier, but in different configurations.
op b : Oid -> Oid [ctor] .
A buffered socket object understands capitalized versions of the messages a socket object understands. For most of them, it just converts them into the corresponding uncapitalized message. There are messages AcceptClient, CloseSocket, CreateServerTcpSocket, and CreateClientTcpSocket with the same arities as the corresponding socket messages, with the following rules.
vars SOCKET NEW-SOCKET SOCKET-MANAGER O : Oid .
vars ADDRESS IP IP' DATA S S' REASON : String .
var Atts : AttributeSet .
vars PORT BACKLOG N : Nat .
rl [createServerTcpSocket] :
CreateServerTcpSocket(SOCKET-MANAGER, O, PORT, BACKLOG)
=> createServerTcpSocket(SOCKET-MANAGER, O, PORT, BACKLOG) .
rl [acceptClient] :
AcceptClient(SOCKET, O)
=> acceptClient(SOCKET, O) .
rl [closeSocket] :
CloseSocket(b(SOCKET), SOCKET-MANAGER)
=> closeSocket(SOCKET, SOCKET-MANAGER) .
rl [createClientTcpSocket] :
CreateClientTcpSocket(SOCKET-MANAGER, O, ADDRESS, PORT)
=> createClientTcpSocket(SOCKET-MANAGER, O, ADDRESS, PORT) .
Note that in these cases the buffered-socket versions of the messages are just translated into the corresponding socket messages.
A BufferedSocket object can also convert an uncapitalized message into the capitalized one. The rule socketError shows this:
rl [socketError] :
socketError(O, SOCKET-MANAGER, REASON)
=> SocketError(O, SOCKET-MANAGER, REASON) .
BufferedSocket objects are created and destroyed when the corresponding sockets are. Thus, we have rules
rl [acceptedclient] :
acceptedClient(O, SOCKET, IP', NEW-SOCKET)
=> AcceptedClient(O, b(SOCKET), IP', b(NEW-SOCKET))
< b(NEW-SOCKET) : BufferedSocket |
bState : idle, read : "" > .
rl [createdSocket] :
createdSocket(O, SOCKET-MANAGER, SOCKET)
=> < b(SOCKET) : BufferedSocket | bState : idle, read : "" >
CreatedSocket(O, SOCKET-MANAGER, b(SOCKET)) .
rl [closedSocket] :
< b(SOCKET) : BufferedSocket | Atts >
closedSocket(SOCKET, SOCKET-MANAGER, DATA)
=> ClosedSocket(b(SOCKET), SOCKET-MANAGER, DATA) .
Once a connection has been established, and a BufferedSocket object has been created on each side, messages can be sent and received. When a Send message is received, the buffered socket sends a send message with the same data plus a mark8.4 to indicate the end of the message.
rl [send] :
< b(SOCKET) : BufferedSocket | bState : active, Atts >
Send(b(SOCKET), O, DATA)
=> < b(SOCKET) : BufferedSocket | bState : active, Atts >
send(SOCKET, O, DATA + "#") .
rl [sent] :
< b(SOCKET) : BufferedSocket | bState : active, Atts >
sent(O, SOCKET)
=> < b(SOCKET) : BufferedSocket | bState : active, Atts >
Sent(O, b(SOCKET)) .
The key is then in the reception of messages. A BufferedSocket object is always listening to the socket. It sends a receive message at start up and puts all the received messages in its buffer. Notice that a buffered socket goes from idle to active in the buffer-start-up rule. A Receive message is then handled if there is a complete message in the buffer, that is, if there is a mark on it, and results in the reception of the first message in the buffer, which is removed from it.
rl [buffer-start-up] :
< b(SOCKET) : BufferedSocket | bState : idle, Atts >
=> < b(SOCKET) : BufferedSocket | bState : active, Atts >
receive(SOCKET, b(SOCKET)) .
rl [received] :
< b(SOCKET) : BufferedSocket |
bState : active, read : S, Atts >
received(b(SOCKET), O, DATA)
=> < b(SOCKET) : BufferedSocket |
bState : active, read : (S + DATA), Atts >
receive(SOCKET, b(SOCKET)) .
crl [Received] :
< b(SOCKET) : BufferedSocket |
bState : active, read : S, Atts >
Receive(b(SOCKET), O)
=> < b(SOCKET) : BufferedSocket |
bState : active, read : S', Atts >
Received(O, b(SOCKET), DATA)
if N := find(S, "#", 0)
/\ DATA := substr(S, 0, N)
/\ S' := substr(S, N + 1, length(S)) .
The BUFFERED-SOCKET module is used in the specification of Mobile Maude, a mobile agent language based on Maude, which is discussed in detail in [16, Chapter 16].