mod SOCKET is
protecting STRING .
including CONFIGURATION .
op socket : Nat -> Oid [ctor] .
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)] .
op socketManager : -> Oid [special (...)] .
endm
Currently only IPv4 TCP sockets are supported; other protocol families and socket types may be added in the future. The external object named by the constant socketManager is a factory for socket objects.
To create a client socket, you send socketManager a message
createClientTcpSocket(socketManager, ME, ADDRESS, PORT)
where ME is the name of the object the reply should be sent to, ADDRESS is the name of the server you want to connect to (say ``www.google.com''), and PORT is the port you want to connect to (say 80 for HTTP connections). You may also specify the name of the server as an IPv4 dotted address or as ``localhost'' for the same machine where the Maude system is running on.
The reply will be either
createdSocket(ME, socketManager, NEW-SOCKET-NAME)
or
socketError(ME, socketManager, REASON)
where NEW-SOCKET-NAME is the name of the newly created socket and REASON is the operating system's terse explanation of what went wrong.
You can then send data to the server with a message
send(SOCKET-NAME, ME, DATA)
which elicits either
sent(ME, SOCKET-NAME)
or
closedSocket(ME, SOCKET-NAME, REASON)
Notice that all errors on a client socket are handled by closing the socket.
Similarly, you can receive data from the server with a message
receive(SOCKET-NAME, ME)
which elicits either
received(ME, SOCKET-NAME, DATA)
or
closedSocket(ME, SOCKET-NAME, REASON)
When you are done with the socket, you can close it with a message
closeSocket(SOCKET-NAME, ME)
with reply
closedSocket(ME, SOCKET-NAME, "")
Once a socket has been closed, its name may be reused, so sending messages to a closed socket can cause confusion and should be avoided.
Notice that TCP does not preserve message boundaries, so sending "one"
and "two" might be received as "on" and "etwo".
Delimiting message boundaries is the responsibility of the next higher-level
protocol, such as HTTP. We will present an implementation of buffered sockets
in Section 8.4.2 which solves this problem.
The following modules implement an updated version of the five rule HTTP/1.0 client from the paper ``Towards Maude 2.0" [14] that is now executable. The first module defines some auxiliary operations on strings.
fmod STRING-OPS is
pr STRING .
var S : String .
op extractHostName : String -> String .
op extractPath : String -> String .
op extractHeader : String -> String .
op extractBody : String -> String .
eq extractHostName(S)
= if find(S, "/", 0) == notFound
then S
else substr(S, 0, find(S, "/", 0))
fi .
eq extractPath(S)
= if find(S, "/", 0) == notFound
then "/"
else substr(S, find(S, "/", 0), length(S))
fi .
eq extractHeader(S)
= substr(S, 0, find(S, "\r\n\r\n", 0) + 4) .
eq extractBody(S)
= substr(S, find(S, "\r\n\r\n", 0) + 4, length(S)) .
endfm
The second module requests one web page to a HTTP server.
mod HTTP/1.0-CLIENT is
pr STRING-OPS .
inc SOCKET .
sort State .
ops idle connecting sending receiving closing : -> State [ctor] .
op state:_ : State -> Attribute [ctor] .
op requester:_ : Oid -> Attribute [ctor] .
op url:_ : String -> Attribute [ctor] .
op stored:_ : String -> Attribute [ctor] .
op HttpClient : -> Cid .
op httpClient : -> Oid .
op dummy : -> Oid .
op getPage : Oid Oid String -> Msg [msg ctor] .
op gotPage : Oid Oid String String -> Msg [msg ctor] .
vars H R R' TS : Oid .
vars U S ST : String .
First, we try to connect to the server using port 80, updating the state and the requester attribute with the new server.
rl [getPage] :
getPage(H, R, U)
< H : HttpClient |
state: idle, requester: R', url: S, stored: "" >
=> < H : HttpClient |
state: connecting, requester: R, url: U, stored: "" >
createClientTcpSocket(socketManager, H,
extractHostName(U), 80) .
Once we are connected to the server (we have received a createdSocket message), we send a GET message (from the HTTP protocol) requesting the page. When the message is sent, we wait for a response.
rl [createdSocket] :
createdSocket(H, socketManager, TS)
< H : HttpClient |
state: connecting, requester: R, url: U, stored: "" >
=> < H : HttpClient |
state: sending, requester: R, url: U, stored: "" >
send(TS, H, "GET " + extractPath(U) + " HTTP/1.0\r\nHost: " +
extractHostName(U) + "\r\n\r\n") .
rl [sent] :
sent(H, TS)
< H : HttpClient |
state: sending, requester: R, url: U, stored: "" >
=> < H : HttpClient |
state: receiving, requester: R, url: U, stored: "" >
receive(TS, H) .
While the page is not complete, we receive data and append it to the string on the stored attribute. When the page is completed, the server closes the socket, and then we show the page information by means of the gotPage message.
rl [received] :
received(H, TS, S)
< H : HttpClient |
state: receiving, requester: R, url: U, stored: ST >
=> receive(TS, H)
< H : HttpClient | state: receiving,
requester: R, url: U, stored: (ST + S) > .
rl [closedSocket] :
closedSocket(H, TS, S)
< H : HttpClient |
state: receiving, requester: R, url: U, stored: ST >
=> gotPage(R, H, extractHeader(ST), extractBody(ST)) .
We use a special operator start to represent the initial configuration. It receives the server URL we want to connect to. Notice the occurrence of the portal <> in such initial configuration.
op start : String -> Configuration .
eq start(S)
= <>
getPage(httpClient, dummy, S)
< httpClient : HttpClient | state: idle, requester: dummy,
url: "", stored: "" > .
endm
Now we can get pages from servers, say ``www.google.com'', by using the following Maude command:
Maude> erew start("www.google.com") .
It is also possible to have optional bounds on the erewrite command, and then use the continuation commands to get more results, like, for example,
Maude> erew [1, 2] start("www.google.com") .
Maude> cont 1 .
To have communication between two Maude interpreter instances, one of them must take the server role and offer a service on a given port; generally ports below 1024 are protected. You cannot in general assume that a given port is available for use. To create a server socket, you send socketManager a message
createServerTcpSocket(socketManager, ME, PORT, BACKLOG)
where PORT is the port number and BACKLOG is the number of queue requests for connection that you will allow (5 seems to be a good choice). The response is either
createdSocket(ME, socketManager, SERVER-SOCKET-NAME)
or
socketError(ME, socketManager, REASON)
Here SERVER-SOCKET-NAME refers to a server socket. The only thing you can do with a server socket (other than close it) is to accept clients, by means of the following message:
acceptClient(SERVER-SOCKET-NAME, ME)
which elicits either
acceptedClient(ME, SERVER-SOCKET-NAME, ADDRESS, NEW-SOCKET-NAME)
or
socketError(ME, socketManager, REASON)
Here ADDRESS is the originating address of the client and NEW-SOCKET-NAME is the name of the socket you use to communicate with that client. This new socket behaves just like a client socket for sending and receiving. Note that an error in accepting a client does not close the server socket. You can always reuse the server socket to accept new clients until you explicitly close it.
The following modules illustrate a very naive two-way communication between two Maude interpreter instances. The issues of port availability and message boundaries are deliberately ignored for the sake of illustration (and thus if you are unlucky this example could fail).
The first module describes the behavior of the server.
mod FACTORIAL-SERVER is
inc SOCKET .
pr CONVERSION .
op _! : Nat -> NzNat .
eq 0 ! = 1 .
eq (s N) ! = (s N) * (N !) .
op Server : -> Cid .
op aServer : -> Oid .
vars O LISTENER CLIENT : Oid .
var A : AttributeSet .
var N : Nat .
vars IP DATA S : String .
Using the following rules, the server waits for clients. If one client is accepted, the server waits for messages from it. When the message arrives, the server converts the received data to a natural number, computes its factorial, converts it into a string, and finally sends this string to the client. Once the message is sent, the server closes the socket with the client.
rl [createdSocket] :
< O : Server | A > createdSocket(O, socketManager, LISTENER)
=> < O : Server | A > acceptClient(LISTENER, O) .
rl [acceptedClient] :
< O : Server | A > acceptedClient(O, LISTENER, IP, CLIENT)
=> < O : Server | A > receive(CLIENT, O)
acceptClient(LISTENER, O) .
rl [received] :
< O : Server | A > received(O, CLIENT, DATA)
=> < O : Server | A >
send(CLIENT, O, string(rat(DATA, 10)!, 10)) .
rl [sent] :
< O : Server | A > sent(O, CLIENT)
=> < O : Server | A > closeSocket(CLIENT, O) .
rl [closedSocket] :
< O : Server | A > closedSocket(O, CLIENT, S)
=> < O : Server | A > .
endm
The Maude command that initializes the server is as follows, where the configuration includes the portal <>.
Maude> erew <>
< aServer : Server | none >
createServerTcpSocket(socketManager, aServer, 8811, 5) .
The second module describes the behavior of the clients.
mod FACTORIAL-CLIENT is
inc SOCKET .
op Client : -> Cid .
op aClient : -> Oid .
vars O CLIENT : Oid .
var A : AttributeSet .
Using the following rules, the client connects to the server (clients must be created after the server), sends a message representing a number,8.3 and then waits for the response. When the response arrives, there are no blocking messages and rewriting ends.
rl [createdSocket] :
< O : Client | A > createdSocket(O, socketManager, CLIENT)
=> < O : Client | A > send(CLIENT, O, "6") .
rl [sent] :
< O : Client | A > sent(O, CLIENT)
=> < O : Client | A > receive(CLIENT, O) .
endm
The initial configuration for the client will be as follows, again with portal <>.
Maude> erew <>
< aClient : Client | none >
createClientTcpSocket(socketManager,
aClient, "localhost", 8811) .
Almost everything in the socket implementation is done in a nonblocking way; so, for example, if you try to open a connection to some webserver and that webserver takes 5 minutes to respond, other rewriting and transactions happen in the meanwhile as part of the same command erewrite. The one exception is DNS resolution, which is done as part of the createClientTcpSocket message handling and which cannot be nonblocking without special tricks.