Bluish Coder

As an exercise in learning more about ATS I worked on porting the preforking echo server I wrote in Pure. I wanted to get a feel for how higher order functions worked so I followed the same structure as the Pure program.

The code I ended up with is in preforking1.dats. There is also a pretty-printed version produced by 'atsopt'. I posted some questions about my attempt on the ATS mailing list and got a reply clearing some things up and with the example reworked. That reworked example is in preforking2.dats (pretty-printed version)

The Pure code uses 'fdopen' to convert the socket file descriptor to a stdio 'FILE*'. ATS doesn't have fdopen as part of the standard library so I added this with the ability to include inline C code.

The sockets code makes use of ATS features to reduce the chance that sockets are used incorrectly by performing compile time typechecking. The code in 'make_server_socket' looks like this:

fun make_server_socket (port: int) : [fd:int] (socket_v(fd,listen) | int fd) = let
  val (pf_sock_s | sockfd) = socket_family_type_exn (AF_INET, SOCK_STREAM);
  var servaddr: sockaddr_in_struct_t;
  val servport = in_port_nbo_of_int (port);
  val in4addr = in_addr_nbo_of_hbo (INADDR_ANY);
  val () = sockaddr_ipv4_init (servaddr, AF_INET, in4addr, servport);
  val () = bind_ipv4_exn (pf_sock_s | sockfd, servaddr);
  val () = listen_exn (pf_sock_s | sockfd, 10);
in
  (pf_sock_s | sockfd)
end;

The socket functions are defined such that performing operations out of order causes a compile error. Removing the 'listen_exn' line and compiling results in this error (edited for brevity):

preforking1.dats: 2072(line=63, offs=3) -- 2092(line=63, offs=23): 
error(3): mismatch of static terms (tyleq):
  The needed term is: S2Eapp(S2Ecst(socket_v); S2EVar(146), S2Eapp(S2Ecst(listen); ))
  The actual term is: S2Eapp(S2Ecst(socket_v); S2EVar(145), S2Eapp(S2Ecst(bind); ))

This error occurs on the line that returns the result:

(pf_sock_s | sockfd)

The error occurs because the return value of 'make_server_socket' is defined as:

[fd:int] (socket_v(fd,listen) | int fd)

The part of the definition to the left of the pipe character (the '|') is a view that is threaded through calls to the socket functions. The 'listen' part says the socket must be in a state whereby 'listen_exn' was called on it. The function definitions for 'bind_ipv4_exn' and 'listen_exn' are:

fun bind_ipv4_exn {fd:int} (
    pf_sock: !socket_v (fd, init) >> socket_v (fd, bind)
  | fd: int fd, servaddr: &sockaddr_in_struct_t
  ) : void

fun listen_exn {fd:int} (
    pf_sock: !socket_v (fd, bind) >> socket_v (fd, listen)
  | fd: int fd, backlog: Pos
  ) : void

The bind_ipv4_exn definition takes as an argument a socket file descriptor in the 'init' state and leaves it in the 'bind' state. The 'listen_exn' function takes a socket in the 'bind' state and leaves it in the 'listen' state. So by not calling 'listen_exn' we've left the socket in the 'bind' state and that does not match the return value of 'make_server_socket'.

This is all checked at compile time. Everything to the left of the pipe character in a type (the '|') is compile time state and is absent at runtime. So the compiled result of the program knows nothing about the state the socket is in.

For more on this read the ATS tutorial topics on dataviews and dataviewtypes.

Another interesting feature is that the socket code ensures at compile time that the socket has been closed. Removing the following line results in a compile time error:

val () = socket_close_exn(pf_sock_s | sockfd);

The error is:

preforking1.dats: 2118(line=67, offs=21) -- 2861(line=81, offs=4): error(3):
the linear dynamic variable [pf_sock_s] needs to be consumed but it is 
preserved with the type 
[S2Eapp(S2Ecst(socket_v); S2EVar(151), S2Eapp(S2Ecst(listen); ))] instead.

You can see in the definitions of the socket functions whether the pf_sock linear variable is expected to be consumed or not. This is indicated by the exclamation mark (the '!') before the type. Compare the definition of 'listen_exn' with that of 'socket_close_exn':

fun listen_exn {fd:int} (
    pf_sock: !socket_v (fd, bind) >> socket_v (fd, listen)
  | fd: int fd, backlog: Pos
  ) : void

fun socket_close_exn {fd:int} {s:status}
   (pf_sock: socket_v (fd, s) | fd: int fd): void

Notice that 'pf_sock' in 'listen_exn' is '!socket_v' whereas in 'socket_close_exn' it is 'socket_v'. The latter says that the linear variable is consumed and cannot be used after this function is called. It is a compile error to use it after it is consumed. It is also a compile error to not consume the linear variable. I showed the error resulting from not closing the socket, the following is the result of using the socket after closing it:

implement main () = let
  val (pf_sock_s | sockfd) = make_server_socket (5000);
  val () = socket_close_exn(pf_sock_s | sockfd);
  val children = array0_make_arraysize($arrsz{pid_t} (fork_child(pf_sock_s | sockfd, child),
                                                     fork_child(pf_sock_s | sockfd, child)));
  ...

preforking1.dats: 2292(line=70, offs=66) -- 2301(line=70, offs=75): error(3): 
  there is no type for the dynamic variable [pf_sock_s].

As the linear dynamic variable 'pf_sock_s' has been consumed by the 'socket_close_exn' call it is no longer available to the code following it.

The ATS Cairo Tutorial has more examples of using the type system to check errors when calling C code.

The 'child' function has an 'assert_err' call in it to check the result of 'input_line' was a valid line and not an error. It then outputs the line:

val line = input_line(file);
val () = assert_errmsg(stropt_is_some line, #LOCATION);
val () = output_line(file, stropt_unsome(line));

If that assert is removed then a compile error results:

preforking1.dats: 1491(line=48, offs=30) -- 1504(line=48, offs=43): 
error(3): unsolved constraint: 
  C3STRprop(none; S2Eapp(S2Ecst(>=); S2EVar(139), S2Eint(0)))

Not the friendliest error message but the line it points too and the offsets show it as being the 'stropt_unsome(line)' part of the 'output_line' call. The following prelude definitions are relevant here:

fun input_line (fil: FILEref): Stropt
fun output_line (fil: FILEref, line: string): void

castfn stropt_some {n:nat} (str: string n):<> stropt n
castfn stropt_unsome {n:nat} (stropt: stropt n):<> string n
fun stropt_is_none {i:int} (stropt: stropt i):<> bool (i < 0)
fun stropt_is_some {i:int} (stropt: stropt i):<> bool (i >= 0)

'input_line' returns a 'Stropt' but 'output_line' requires a 'string'. 'stropt_unsome' takes a 'stropt' of length 'n' where 'n' is a natural number (positive integer greater than one) and returns a 'string' of the same length.

The result returned from 'input_line' can have a length of zero which doesn't match the type of stropt_unsome which requires a length of one or more. This results in the compile time error when the assertion is removed. The compiler is telling the programmer that they haven't catered for the possible error result of a zero length string returned from 'input_line'.

By adding the assertion there is now a check for the case of the length being zero resultinging in the assertion failure. The compiler now knows that any use of the string after that line must have a length of greater than zero. So the type check to the call of 'stropt_unsome' passes.

The original code I wrote created closures and used some input functions to read from the socket that used heap allocations that results in the garbage collector needing to be linked into the program. In the reworked example posted to the mailing list the code was changed to not require garbage collection to be used. One feature used in that example is allocating closures on the stack instead of the heap. This is done with '@lam':

var !p_clo = @lam
    (pf: !V | pid: &pid_t): void =<clo> let
    val _pid = $effmask_all (waitpid(pid, status, WNONE))
  in
    // nothing
  end 
val () = array_ptr_foreach_clo<pid_t> {V} (view@ status | !p_children, !p_clo, NCHILD)

The 'var !p_clo = @lam' syntax means that the closure is stack allocated and the memory will be reclaimed when the function exits. The 'array_ptr_foreach_clo' call following it then calls this closure on each item in the array of process id's. It's also possible to heap allocate closures and manually free them - linear types ensure the call to free the memory is not forgotten by the programmer. Getting the type annotations for closures is unfortunately tricky and the syntax is a bit painful.

The ATS tutorial has a section on allocation in stack frames and functions vs closures.