Re: [Haskell-cafe] Suggestion for Network.Socket in regards to PortNumber

On Mon, Jun 22, 2009 at 7:27 PM, Tim Sheard
My idea is to use types to ensure that any sequence of operations adheres to a path on a finite state automata. For example if we wanted to implement the following automata (This needs to read in a fixed width font)
Here's the reply Oleg gave me when I asked about using monadic regions to enforce similar constraints (published with Oleg's permission): Oleg writes:
First of all, protocols of using API functions are essentially session types, right? Thus various implementations of session types could be taken advantage of (including the one presented by Jesse Tov on Haskell 2008 Symposium). Aliasing is responsible for a lot of the complexity: if the variable 's' is bound to a value of the type socket and we execute "do s' <- bindS s" so to bind the socket, the old variable s is still available and could be used. But it should not be used because bindS "consumed" the unbound socket and produced the new one. To properly describe these resource restrictions (a resource can be consumed and after that it is not available any more), we need linear, affine or various other kinds of substructural logics and type systems. It seems they all can be emulated in Haskell, but with some hackery (see for example Sec 6 of our monadic regions paper). Parameterized monads are necessary.
The lightweight monadic regions paper relied on a simple session protocol: open -> (read+write)* -> close. That protocol can be ensured without parameterized monads: the only aliasing to mind is the accessibility of the file handle after the closing operation. We can get rid of `close' (make it implicit ar region's exit) and use rank-2 types to prevent file handles from leaking out. There is some dynamic overhead, in the function open. However, the most frequent operation, reading and writing from the handle, involves no overhead and its correctness ensured statically.
That design can be extended to sockets. For example:
data Socket sort = Socket Int
data UnconnectedSocket data ConnectedSocket s
connect :: RMonadIO (m s) => SocketProto -> SAddress -> m s (Socket (ConnectedSocket s))
sendto :: RMonadIO (m s) => (Socket (ConnectedSocket s)) -> Buffer -> m s (ReturnCode)
-- polymorphic in the socket sort send :: MonadIO m => Socket sort -> Buffer -> m ReturnCode
In this design, the operation of creating a socket and connecting it are bundled together -- which is very common and is the case for System V, I think (where it is called openActive, I think). If you for some reason want to keep 'socket' and 'connect' separate, then 'connect' has to check at run-time that the socket in question is not connected yet. Still, the most common operations like send and write should be overhead-free.
Cheers, Johan

On Jun 24, 2009, at 05:11 , Johan Tibell wrote:
Oleg writes:
In this design, the operation of creating a socket and connecting it are bundled together -- which is very common and is the case for System V, I think (where it is called openActive, I think). If you for
I don't believe that is specced by SVID or successors. TLI/XTI may have had something similar to it but nobody wants to go there. :)
some reason want to keep 'socket' and 'connect' separate, then
One reason to do so is that for connectionless (UDP) sockets, the BSD socket protocol *allows* connect(); this allows you to use send() instead of sendto() and is an optimization for the case where you are communicating with a single remote service. (That said, the only program/service I can think of where this is guaranteed is tftp. There's no point in optimizing cases where it might be true on a case- by-case basis, such as DNS when only a single nameserver has been specified.) A more common case is that servers accept() instead of connect(). listen() switches the socket to this state. (NB! bind() is *not* involved here; a client can bind(), although it's unusual, and a server may register with a naming service instead of bind()ing to a well known port — see Sun RPC for example.) Still another state change is invoked by shutdown(), which can make read/recv and/or write/send illegal operations. A socket which has been shutdown() for both send and receive can be close()d or select()ed; the latter lets you wait for the other end to disconnect, or to catch late errors. The BSD socket protocol is explicitly driven by a state machine, btw, but it's a fairly complex one. Also, it's generally described in terms of the kernel's view, which includes states you normally can't distinguish in a user program (for example, a socket in TIME_WAIT keeps its port unavailable unless you use SO_REUSEADDR, but is otherwise indistinguishable from a socket which has been close()d and reaped). -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

On Wed, Jun 24, 2009 at 8:16 PM, Brandon S. Allbery KF8NH < allbery@ece.cmu.edu> wrote:
The BSD socket protocol is explicitly driven by a state machine, btw, but it's a fairly complex one. Also, it's generally described in terms of the kernel's view, which includes states you normally can't distinguish in a user program (for example, a socket in TIME_WAIT keeps its port unavailable unless you use SO_REUSEADDR, but is otherwise indistinguishable from a socket which has been close()d and reaped).
I've been looking for a state diagram for this state machine for e.g. Linux but my google-fu has failed me so far. Do you have a reference? -- Johan

A search in google images for sockets state diagram comes up with some
relatively good ones
http://images.google.com/images?hl=en&um=1&sa=3&q=sockets+state+diagram&btnG=Search+images
Most of them are just the TCP connection state logic, but I'm sure I'd find
others there if I looked closer.
- Job
On Wed, Jun 24, 2009 at 3:11 PM, Johan Tibell
On Wed, Jun 24, 2009 at 8:16 PM, Brandon S. Allbery KF8NH < allbery@ece.cmu.edu> wrote:
The BSD socket protocol is explicitly driven by a state machine, btw, but it's a fairly complex one. Also, it's generally described in terms of the kernel's view, which includes states you normally can't distinguish in a user program (for example, a socket in TIME_WAIT keeps its port unavailable unless you use SO_REUSEADDR, but is otherwise indistinguishable from a socket which has been close()d and reaped).
I've been looking for a state diagram for this state machine for e.g. Linux but my google-fu has failed me so far. Do you have a reference?
-- Johan
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Wed, Jun 24, 2009 at 9:43 PM, Job Vranish
A search in google images for sockets state diagram comes up with some relatively good ones
http://images.google.com/images?hl=en&um=1&sa=3&q=sockets+state+diagram&btnG=Search+images Most of them are just the TCP connection state logic, but I'm sure I'd find others there if I looked closer.
I tried this search and did look closer but I only find TCP state diagrams and other non-related diagrams. :( -- Johan

On Jun 24, 2009, at 16:04 , Johan Tibell wrote:
On Wed, Jun 24, 2009 at 9:43 PM, Job Vranish
wrote: A search in google images for sockets state diagram comes up with some relatively good ones http://images.google.com/images?hl=en&um=1&sa=3&q=sockets+state+diagram&btnG=Search+images Most of them are just the TCP connection state logic, but I'm sure I'd find others there if I looked closer. I tried this search and did look closer but I only find TCP state diagrams and other non-related diagrams. :(
This is what happens when I write while my sinuses are trying to convince me that I am drunk :/ The more accurate version of what I said is "the BSD socket protocol is a direct reflection of the TCP state diagram; UDP and other socket types are hacked on top of it and can be a poor fit". Studying the TCP state diagram should make it clear why sockets work as they do, but all the rules go out the window if you're not doing TCP. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH
participants (3)
-
Brandon S. Allbery KF8NH
-
Job Vranish
-
Johan Tibell