Bluish Coder

Implementing a stack with proofs in ATS

This post works through an example of a stack datatype, adding ATS features as we go along to help prove the implementation is correct. The example starts with a simplified stack of integers. I then add some dependent types to improve checking of the implementation and follow this with dataprop usage for more extensive compile time checking.

I use datatype when defining the stack type. This requires the ATS garbage collector but keeps the code a bit simpler for those not used to reading ATS annotations. The code here is based on examples in the ATS distribution in the doc/EXAMPLE/SPEC/stack directory but simplified for ease of explanation. This post documents the process I went through to understand that example better.

The example code can be found in this github gist:

git clone git://gist.github.com/3826469.git

Stack

The code for this is in the gist as stack1.dats.

The definition of the first stack implementation is:

datatype stack =
  | stack_nil
  | stack_cons of (int, stack)

fun stack_new (): stack
fun stack_is_empty (s: stack): bool
fun stack_top (s: stack): int
fun stack_pop (s: &stack): void
fun stack_push (s: &stack, x: int): void

The stack is represented as a list with the top of the stack being the head of the list. The stack is created with stack_new and the remaining functions receive a reference to the stack (which is what the "&" means) so that they can modify it when pushing and popping. The implementation is:

implement stack_new () = stack_nil ()
implement stack_is_empty (s) =
  case+ s of
  | stack_nil () => true
  | stack_cons _ => false

implement stack_push (s, x) = (s := stack_cons (x, s))
implement stack_top (s) =
  case+ s of
  | stack_nil () => (assertloc (false); 0)
  | stack_cons (x,_) => x

implement stack_pop (s) =
  case+ s of
  | stack_nil () => assertloc (false)
  | stack_cons (_, xs) => s := xs

An assertion is thrown if an attempt is made to get the top of an empty stack.

Checking emptiness

The code for this is in the gist as stack2.dats.

Certain stack operations shouldn't work on an empty stack. This can be seen in the implementation of stack_top and stack_pop where it asserts at runtime if the stack is empty. One way of having the property checked at compile time is to add a boolean type index to the stack type that indicates if it is an empty stack or a non-empty stack:

datatype stack (bool) =
  | stack_nil (true)
  | {b:bool} stack_cons (false) of (int, stack b)

fun stack_new (): stack true
fun stack_is_empty {b:bool} (s: stack b): bool b
fun stack_top {b:bool} (s: stack false): int
fun stack_pop (s: &stack false >> stack b): #[b:bool] void
fun stack_push {b:bool} (s: &stack b >> stack false, x: int): void

In this definition stack_nil has the type index set to true to indicate at the type level that it is an empty stack. stack_cons has the type index set to false as a cons is a non-empty stack. A stack_cons can be applied to a empty or non-empty stack as the second argument to the constructor so the definition allows an unconstrained bool there.

The function definitions are changed to encode knowledge of the effect they have on the stack. stack_new always returns an empty stack. stack_top and stack_pop can only work on non-empty stacks. The boolean result of stack_is_empty returns a result which depends on the type of the stack it is given as an argument. This allows the type checker to reason about stack emptiness state when stack_is_empty is called.

The definition of stack_pop uses >> to change the type after calling so that the emptiness of the stack is no longer known. The #[b:bool] syntax identifies b as an existantial variable that can be referenced in the arguments. So we say here the emptiness state of the input stack is now unknown after calling.

stack_push is similar but we say there that the emptiness state is unknown when called but known after calling - it will be a non-empty stack.

With this static checking in place the implementation of stack_top and stack_pop no longer needs the assertion:

implement stack_top (s) = let
  val+ stack_cons (x,_) = s
in
  x
end

implement stack_pop (s) = let
  val+ stack_cons (_, xs) = s
in
  s := xs
end

val+ does an exhaustive match. It fails at compile time if any other possible pattern match is valid. Calling code must ensure that a non-empty stack is passed to these functions.

implement main () = {
  var s1 = stack_new ()
  val a = stack_is_empty (s1)
  val () = stack_push (s1, 10)
  val b = stack_is_empty (s1)
  val c = stack_top (s1)
  val () = stack_pop (s1)
  val d = stack_is_empty (s1)
}

This code contains no assertion checks but still type checks. This is because the type checker can follow the flow of the value of the emptiness state of the stack from stack_new, which is always empty, through to the end of the function thanks to our additional type declarations on the stack functions. Checks are needed in the case of code like the following where the initial stack state is unknown:

fun mustcheck {b:bool} (s: stack b): void = {
  val () = assertloc (not (stack_is_empty (s)))
  val c = stack_top (s)
}

Without the assertloc this code won't compile as stack_top can't tell statically whether the stack is empty or not. Note that if the function were to push onto the stack then the assertloc isn't needed as the declaration for stack_push indicates the stack can't be empty:

fun nocheck {b:bool} (s: &stack b >> stack false): void = {
  val () = stack_push (s, 42)
  val c = stack_top (s)
}

This example can be improved further by using an integer type index representing the number of items on the stack instead of using a bool. The push and pop operations can increment and decrement this index. This would give the type checker more information on pop operations as it could infer when pop results in an empty stack rather than the unknown result the current example results in. I leave this as an exercise for the reader as our next iteration provides this and more by taking a slightly different approach.

Checking a stack really is a stack

The code for this is in the gist as stack3.dats.

For this iteration of the stack code we'll be changing the approach a bit. Previously we verified our usage of stack was correct in certain cases. In this approach we'll verify that the implementation of stack matches the specification of being a stack. To do this we'll first model a list in the 'static' type system of ATS (the type system of type indexes and done using datasort) and then define some dataprop relations that specify what each stack operation means in terms of this static list:

datasort ilist =
  | inil
  | icons of (int, ilist) 

The following dataprop constructs look very similar to the datatype construct used in the ATS dynamic type system. The resulting prop is used to encode a relation that can be used as a proof in functions. We define props EMPTY, IS_EMPTY, TOP, PUSH and POP for each of the standard stack operations.

EMPTY is an empty stack. It has one constructor, also called EMPTY that has a list as an argument that must be inil, the constructor for the empty ilist sort.

dataprop EMPTY (ilist) =
  | EMPTY (inil)

IS_EMPTY has two constructors, one for the case when the list is empty and one for when it is not. The prop is indexed by the ilist and a boolean. It encodes the relation that the given ilist is empty if the boolean is true. The IS_EMPTY_true constructor shows that a inil list is empty. The IS_EMPTY_false constructor shows that a icons is not empty.

dataprop IS_EMPTY (ilist, bool) =
  | IS_EMPTY_true (inil, true) 
  | {x:int} {xs:ilist} IS_EMPTY_false (icons (x,xs), false)

The TOP prop encodes the relation that the given ilist has the given value at the top of the stack. The TOP constructor does this by pattern matching the icons and using the head of the icons as the value.

dataprop TOP (ilist, int) = 
  | {x:int} {xs:ilist} TOP (icons (x,xs), x)

The PUSH prop has three index arguments. it encodes the relation that the first list, when having the 2nd argument pushed onto it, results in the third list. The PUSH constructor shows how this is done.

dataprop PUSH (ilist, int, ilist) = 
  | {x:int} {xs,ys:ilist} PUSH (xs, x, icons (x, xs))

The POP prop has two index arguments, both are lists. It encodes the relation that the first list, when pop is called on it, will result in the second list. The POP constructor implementation shows this.

dataprop POP (ilist, ilist) =
  | {x:int} {xs:ilist} POP (icons (x,xs), xs)

These dataprop definitions form the basic specification for a stack. Instead of implementing the specification as functions they are encoded as prop types so they can be used in proofs of an actual implementation to test that the implementation conforms to the specification. It's important though to do some checks that the specification itself is correct. These checks can be done as proof functions in ATS. Proof functions are checked during compilation then erased at code generation time so they have no run time overhead.

The following proof function asserts that when a push of a value x on a stack xs results in a stack ys, the top of the ys will be the x that was pushed:

prfun stack_push_check {x:int} {xs,ys:ilist} .<>. (pf: PUSH (xs, x, ys)):<> TOP (ys, x) = let
  prval PUSH () = pf
in
  TOP ()
end

Note that the implementation of the proof function is trivial. The assignment in the first implementation line will set the universal variables in the PUSH constructor from the values in the type of pf. The return of TOP () then matches the appropriate values based on the return type of the proof function. It basically checks that (psuedo code):

val ys = icons (x, xs)   // PUSH
val icons (x', xs') = ys // TOP
x' == x && xs' = xs

The .<>. syntax in the proof function means the function is non-recursive and terminates. The :<> syntax means the proof function is pure (has no side effects). These are requirements for functions involving proofs.

The following proof function asserts that popping a value off the stack resulting from a push operation results in the same stack as the original:

prfun stack_pop_check {x:int} {xs,ys:ilist} .<>. (pf: PUSH (xs, x, ys)):<> POP (ys, xs) = let
  prval PUSH () = pf
in
  POP ()
end

This proof function asserts that is_empty on an empty list is true:

prfun stack_empty_check {xs:ilist} .<>. (pf: EMPTY xs):<> IS_EMPTY (xs, true) = let
  prval EMPTY () = pf
in
  IS_EMPTY_true ()
end

With these definitions in a file you can run the ATS type checker to confirm that the specifications passes the checks using the -tc command line option:

$ atscc -tc stack3.dats  
The file [stack3.dats] is successfully typechecked!

Implementing a stack checked against the specification

The code for this is in the gist as stack4.dats.

Given the specification for the stack operations in the previous section we can now write a stack implementation where proofs are used to ensure the implementation matches the spec. The first step is to define the stack datatype indexed by the ilist sort:

datatype stack (ilist) =
  | stack_nil (inil)
  | {x:int} {xs:ilist} stack_cons (icons (x,xs)) of (int x, stack xs)

The functions that implement the stack operations take and return the proof objects defined by the dataprop definitions for the stack operations. Proof arguments in ATS functions are seperated from normal function arguments by a pipe,|, symbol. All those arguments to the left of the | are proof arguments:

fun stack_new (): [xs:ilist] (EMPTY xs | stack xs)
fun stack_is_empty {xs:ilist} (s: stack xs): [b:bool] (IS_EMPTY (xs, b) | bool b)
fun stack_top {xs:ilist} (pf: IS_EMPTY (xs, false) | s: stack xs): [x:int] (TOP (xs, x) | int x)
fun stack_pop {x:int} {xs:ilist} (pf: IS_EMPTY (xs, false) | s: &stack xs >> stack ys)
                                   : #[ys:ilist] (POP (xs, ys) | void)
fun stack_push {x:int} {xs:ilist} (s: &stack xs >> stack ys, x: int x)
                                   : #[ys:ilist] (PUSH (xs, x, ys) | void)

The stack_top and stack_pop functions require the caller to provide a proof that the stack is not empty. All the operations return a proof that is used to ensure the implementation of the function is correct (as defined by the relations we wrote previously).

implement stack_new () = (EMPTY () | stack_nil ())
implement stack_is_empty (s) =
  case+ s of
  | stack_nil () => (IS_EMPTY_true | true)
  | stack_cons _ => (IS_EMPTY_false | false)

implement stack_push {x} {xs} (s, x) = (PUSH () | (s := stack_cons (x, s)))
implement stack_top (pf | s) = let
  prval IS_EMPTY_false () = pf
  val+ stack_cons (x,_) = s
in
  (TOP () | x)
end

implement stack_pop (pf | s) = let
  prval IS_EMPTY_false () = pf
  val+ stack_cons (_, xs) = s
in
  (POP () | s := xs)
end

The main changes compared to the previous implementations we've done of stack is to handle the proof arguments. The handling is mostly trivial in that we assign the argument to the expected type (eg. IS_EMPTY_false if we expect the stack to be empty) and we use the constructors for returning the proofs for the various operations. The actual checking that the implementation is correct is done by the ATS proof system using the types and variables defined in the dataprop statements in a similar manner to the proof check functions discussed earlier. The proofs are erased at code generation time and the resulting C code is exactly as if it was written without the proofs - with the knowledge that the code is correct as it was checked at compile time.

The additional proof code does impose a syntactical burden to the user of the stack code. For example:

fun mustcheck {xs:ilist} (s: stack xs): void = {
  val (pf | e) = stack_is_empty (s)
  val () = assertloc (not e)
  val (_ | c) = stack_top (pf | s)
}

In this check we need to pass the proof from the stack_is_empty call to the stack_top call. Even though we don't need the proof result of the stack_top call we still need to match it against the wildcard _ symbol to ignore it. For the nocheck example shown previously:

fun nocheck {xs:ilist} (s: &stack xs >> stack ys): #[ys:ilist] void = {
  val (pf | ()) = stack_push (s, 42)
  prval PUSH () = pf
  val (_ | c) = stack_top (IS_EMPTY_false () | s)
}

We need to do a proof assignment of the stack_push proof result for the code to correctly infer that the stack is not empty and the IS_EMPTY_false proof we construct is correct. The main function showing basic stack usage becomes:

implement main () = {
  val (_ | s) = stack_new ()
  var s1 = s
  val (_ | a) = stack_is_empty (s1)
  val (pf | ()) = stack_push (s1, 10)
  prval PUSH () = pf
  val (_ | b) = stack_is_empty (s1)
  val (_ | c) = stack_top (IS_EMPTY_false () | s1)
  val (pf | ()) = stack_pop (IS_EMPTY_false () | s1)
  prval POP () = pf
  val (_ | d) = stack_is_empty (s1)
}

We can ignore many of the proofs here so they are pattern matched with the wildcard symbol _. The use of prval PUSH () = pf is needed to allow the stack_top and stack_pop calls to to be successfully checked. The equivalent for POP would be needed if we used stack_top or stack_pop after that call.

The benefit of the additional proof code is that we can be assured that the stack implementation matches our stack specification. The implementation is verified to be correct and our usage is verified to be correct. Any changes to the implementation will fail to compile if they don't match the specification (popping too many elements off the stack for example). We can write alternate stack implementations that use the same stack proofs to verify that those implementations are correct. The ATS distribution includes an implementation based on lists and arrays in the doc/EXAMPLE/SPEC/stack directory.

Non-integer stacks

The code for this is in the gist as stack5.dats.

The implementation shown previously is simplified in that it is a stack of integers. The nicely matches the ilist sort which is a list of integers. Handling verification of a stack that contains a non-integer type requires a workaround. We keep the ilist sort and proofs but introduce a new abstract type that maps our actual stack element type to an int sort. In the following example we create a stack of double values. The abstract type that is the placeholder for the real element type is:

abst@ype E (t@ype,int) = double
castfn encode (x: double):<> [x:int] E (double, x)
castfn decode {i:int} (x: E (double, i)):<> double

Included are two cast functions to convert from the placeholder value to our real value and back. The abstract type is set to be the same size as our element type so the compiler can treat it exactly as if it was a double. The stack datatype and functions are written to use the abstract type instead of the real type:

datatype stack (ilist) =
  | stack_nil (inil)
  | {x:int} {xs:ilist} stack_cons (icons (x,xs)) of (E (double, x), stack xs)

fun stack_top {xs:ilist} (pf: IS_EMPTY (xs, false) | s: stack xs)
                           : [x:int] (TOP (xs, x) | E (double, x))
fun stack_push {x:int} {xs:ilist} (s: &stack xs >> stack ys, x: E (double, x))
                           : #[ys:ilist] (PUSH (xs, x, ys) | void)

I only show the functions that have changed here. The changes are minor but the caller will need to use encode and decode when calling and retrieving values:

val (pf | ()) = stack_push (s1, encode 10.0)
val (_ | c) = stack_top (IS_EMPTY_false () | s1)  
val () = printf("%f\n", @(decode c))

The generated C code is as efficient as the original stack however. The compiler knows the exact size of the placeholder type as we assign it in the abst@ype definition. The cast functions are no-ops at generation time.

This approach can be made generic by adding the element type as an index to the stack type and making the stack functions template functions. I leave that as an exercise for the reader but the doc/EXAMPLE/SPEC/stack example shipped with ATS shows the way.

Conclusion

This approach to proof checking has some syntactical overhead when writing and reading code. One could imagine an IDE (or emacs mode) that allowed the user to hide or display proofs as required to help reduce the overhead. Once familiar with proof code it may not be so noticeable, much like how parenthesis in Lisp disappear to the experienced developer.

More information and examples on proof checking in ATS are available at:

• Theorem-Proving in ATS
• Programming with Theorem-Proving
• Combining Programming with Theorem-Proving (PDF Paper)

Safer handling of C memory in ATS

In previous ATS posts I've written about how ATS can make using C functions safer by detecting violations of the C API's requirements at compile time. This post is a walkthrough of a simple example which involves a C api that copies data from a buffer of memory to one allocated by the caller. I'll start with an initial attempt with no safety beyond a C version and work through different options.

The API I'm using for the example is a base64 encoder from the stringencoders library. The C definition of the function is:

size_t modp_b64_encode(char* dest, const char* str, size_t len);

Given a string, str, this will store the base64 encoded value of len bytes of that string into dest. dest must be large enough to hold the result. The documentation for modp_b64_encode states:

• dest should be allocated by the caller to contain at least ((len+2)/3*4+1) bytes. This will contain the null-terminated b64 encoded result.
• str contains the bytes
• len contains the number of bytes in str
• returns length of the destination string plus the ending null byte. i.e. the result will be equal to strlen(dest) + 1.

A first attempt

A first attempt at wrapping this in ATS is:

extern fun modp_b64_encode (dest: !strptr1, str: string, len: size_t): size_t = "mac#modp_b64_encode"

dest is defined to be a linear non-null string. The ! means that the C function does not free the string and does not store it so we are responsible for allocating the memory and freeing it. The following function uses this API to convert a string into a base64 encoded string:

extern fun string_to_base64 (s: string): strptr1

implement string_to_base64 (s) = let
  val s_len = string_length (s)                           // 1
  val d_len = size1_of_size ((s_len + 2) / 3 * 4)         // 2
  val (pfgc, pf_bytes | p_bytes) = malloc_gc (d_len + 1)  // 3
  val () = bytes_strbuf_trans (pf_bytes | p_bytes, d_len) // 4
  val dest = strptr_of_strbuf @(pfgc, pf_bytes | p_bytes) // 5
  val len = modp_b64_encode (dest, s, s_len)              // 6
in
  dest                                                    // 7
end

A line by line description of what this functions does follows:

1. Get the length of the input string as s_len
2. Compute the length of the destination string as d_len. This does not include the null terminator.
3. Allocate d_len number of bytes plus one for the null terminator. This returns three things. pfgc is a proof variable that is used to ensure we free the memory later. pf_bytes is a proof that we have d_len+1 bytes allocated at a specific memory address. We need to provide this proof to other functions when we pass the pointer to the memory around so that the compiler can check we are using the memory correctly. p_bytes is the raw pointer to the memory. We can't do much with this without the proof pf_bytes saying what the pointer points too.
4. We have a proof that says we have a raw array of bytes. What we want to say is that this memory is actually a pointer to a null terminated string. In ATS this is called a strbuf. The function bytes_strbuf_trans converts the proof pf_bytes from "byte array of length n" to "null terminated string of length n-1, with null terminator at n".
5. Now that we have a proof saying our pointer is a string buffer we can convert that to a strptr1. The function strptr_of_strbuf does this conversion. It consumes the pfgc and pf_bytes and returns the strptr1.
6. Here we call our FFI function.
7. Returns the resulting strptr1

string_to_base64 is called with code like:

implement main () = let
  val s = string_to_base64 "hello_world"
in
  begin
    print s;
    print_newline ();
    strptr_free s
  end
end

Although this version of the FFI usage doesn't gain much safety over using it from C, there is some. I originally had the following and the code wouldn't type check:

  val d_len = size1_of_size ((s_len + 2) / 3 * 4 + 1)     // 2
  val (pfgc, pf_bytes | p_bytes) = malloc_gc d_len        // 3
  val () = bytes_strbuf_trans (pf_bytes | p_bytes, d_len) // 4

In line 2 I include the extra byte for the null terminator. But line 4 uses this same length when converting the byte array proof into a proof of having a string buffer. What line 4 now says is we have a string buffer of length d_len with a null terminator at d_len+1. The proof pf_bytes states we only have a buffer of length d_len so fails to type check. The ability for ATS to typecheck lengths of arrays and knowing about requiring null terminators in string buffers saved the code from an off by one error here.

A version of this code is available in github gist 3522299. This can be cloned and used to work through the following examples trying out different approachs.

$ git clone git://gist.github.com/3522299.git example
$ cd example
$ make
$ ./base64

Typecheck the source buffer

One issue with this version of the wrapper is that we can pass an invalid length of the source string:

val len = modp_b64_encode (dest, s, 1000)

Since s is less than length 1000 this will access memory out of bounds. This can be fixed by using dependent types to declare that the given length must match that of the source string length:

extern fun modp_b64_encode {n:nat} (dest: !strptr1,
                                    str: string n, 
                                    len: size_t n): size_t = "mac#modp_b64_encode"

We declare that a sort n exists that is a natural number. The str argument is a string of length n and the length passed is that same length. This is now a type error:

val s = string1_of_string "hello"
val len = modp_b64_encode (dest, s, 1000)

Unfortunately so is this:

val s = string1_of_string "hello"
val len = modp_b64_encode (dest, s, 2)

Ideally we want to be able to pass in a length of less than the total string length so we can base64 encode a subset of the source string. The following FFI declaration does this:

extern fun modp_b64_encode {n:nat} (dest: !strptr1,
                                    str: string n, 
                                    len: sizeLte n): size_t = "mac#modp_b64_encode"

sizeLte is a prelude type definition that's defined as:

typedef sizeLte (n: int) = [i:int | 0 <= i; i <= n] size_t (i)

It is a size_t where the value is between 0 and n inclusive. Our string_to_base64 function is very similar to what it was before but uses string1 functions on the string. string1 is a dependently typed string which includes the length in the type:

extern fun string_to_base64 {n:nat} (s: string n): strptr1

implement string_to_base64 (s) = let
  val s_len = string1_length (s)
  val d_len = (s_len + 2) / 3 * 4
  val (pfgc, pf_bytes | p_bytes) = malloc_gc (d_len + 1)
  val () = bytes_strbuf_trans (pf_bytes | p_bytes, d_len)
  val dest = strptr_of_strbuf @(pfgc, pf_bytes | p_bytes)
  val len = modp_b64_encode (dest, s, s_len)
in
  dest
end

Typecheck the destination buffer

The definition for modp_b64_encode defines the destination as being a linear string. This has no length defined at the type level so it's possible to pass a linear string that is too small and result in out of bounds memory access. this version of the FFI definition changes the type to a strbuf.

As explained previously an strbuf is a string buffer that is null terminated, It has two type level arguments:

abst@ype strbuf (bsz: int, len: int)

The first, bsz is the length of the entire buffer. The second, len is the length of the string. So bsz should be greater than len to account for the null terminator.

The new version of the modp_b64_encode functions is quite a bit more complex so I'll go through it line by line:

extern fun modp_b64_encode                                              
             {l:agz}                                                   // 1
             {n,bsz:nat | bsz >= (n + 2) / 3 * 4 + 1}                  // 2
             (pf_dest: !b0ytes bsz @ l >> strbuf (bsz, rlen - 1) @ l | // 3
              dest: ptr l,                                             // 4
              str: string n,                                           
              len: sizeLte n                                           
            ): #[rlen:nat | rlen >= 1;rlen <= bsz] size_t rlen         // 5
            = "mac#modp_b64_encode"

Put simply, this function definition takes a pointer to a byte array enforced to be the correct size and after calling enforces that the pointer is now a pointer to a null terminated string with the correct length. In detail:

1. This line declares a dependent type variable l of sort agz. Sort agz is an address greater than zero. In otherwords it's a non-null pointer address. It's used to allow the definition to reason about the memory address of the destination buffer.
2. Declare dependent type variables n and bsz of sort nat. Sort nat is an integer greater than or equal to zero. bsz is additionally constrained to be greator or equal to (n+2)/3*4+1. This is used to ensure that the destination buffer is at least the correct size as defined by the documentation for modp_b64_encode. In this way we can enforce the constraint at the type level.
3. All function arguments to the left of the | symbol in ATS are proof arguments. This line defines pf_dest which on input should be a proof that an array of bytes of length bsz is held at memory address l (b0ytes is a typedef for an array of uninitialized bytes). The ! states that this function does not consume the proof. The >> means that after the function is called the type of the proof changes to the type on the right hand side of the >>. In this case it's a string buffer at memory address l of total length bsz, but the actual string is of length rlen-1 (the result length as described next).
4. The dest variable is now a simple pointer type pointing to memory address l. The proof pf_dest describes what this pointer actually points to.
5. We define a result dependent type rlen for the return value. This is the length of the returned base64 encoded string plus one for the null terminator. We constrain this to be less than or equal to bsz since it's not possible for it to be longer than the destination buffer. We also constrain it to be greater than or equal to one since a result of an empty string will return length one. The # allows us to refer to this result dependent type in the function arguments which we do for pf_dest to enforce the constraint that the string buffer length is that of the result length less one.

Our function to call this is a bit simpler:

extern fun string_to_base64 {n:nat} (s: string n): strptr1

implement string_to_base64 (s) = let
  val s_len = string1_length (s)
  val d_len = (s_len + 2) / 3 * 4 + 1
  val (pfgc, pf_bytes | p_bytes) = malloc_gc d_len
  val len = modp_b64_encode (pf_bytes | p_bytes, s, s_len)
in
  strptr_of_strbuf @(pfgc, pf_bytes | p_bytes)
end

We no longer need to do the manual conversion to a strbuf as the definition of modp_b64_encode changes the type of the proof for us.

Handle errors

So far the definitions of modp_64_encode have avoided the error result. If the length returned is -1 there was an error. In our last definition of the function we changed the type of the proof to a strbuf after calling. What we actually need to do is only change the type if the function succeeded. On failure we must leave the proof the same as when the function was called. This will result in forcing the caller to check the result for success so they can unpack the proof into the correct type. Here's the new, even more complex, definition:

dataview encode_v (int, int, addr) =
  | {l:agz} {bsz:nat} {rlen:int | rlen > 0; rlen <= bsz }
      encode_v_succ (bsz, rlen, l) of strbuf (bsz, rlen - 1) @ l 
  | {l:agz} {bsz:nat} {rlen:int | rlen <= 0 } 
      encode_v_fail (bsz, rlen, l) of b0ytes bsz @ l

extern fun modp_b64_encode 
             {l:agz}
             {n,bsz:nat | bsz >= (n + 2) / 3 * 4 + 1}
             (pf_dest: !b0ytes bsz @ l >> encode_v (bsz, rlen, l) |  // 1
              dest: ptr l,
              str: string n, 
              len: sizeLte n
             ): #[rlen:int | rlen <= bsz] size_t rlen 
             = "mac#modp_b64_encode"

First we define a view called encode_v to encode the result that the destination buffer becomes. A dataview is like a datatype but is for proofs. It is erased after type checking is done. The view encode_v is dependently typed over the size of the buffer bsz, the length of the result, rlen, and the memory address, l.

The first view constructor, encode_v_succ, is for when the result length is greater than zero. In that case the view contains a strbuf. This is the equivalent of the case in our previous iteration where we only handled success.

The second view constructor, encode_v_fail, is for the failure case. If the result length is less than or equal to zero then the view contains the original array of bytes.

In the line marked 1 above, we've changed the type the proof becomes to that of our view. Notice that the result length is one of the dependent types of the view. Now when calling modp_b64_encode we must check the return type so we can unpack the view to get the correct proof. Here is the new calling code:

extern fun string_to_base64 {n:nat} (s: string n): strptr0

implement string_to_base64 (s) = let
  val s_len = string1_length (s)
  val d_len = (s_len + 2) / 3 * 4 + 1
  val (pfgc, pf_bytes | p_bytes) = malloc_gc d_len
  val len = modp_b64_encode (pf_bytes | p_bytes, s, s_len) 
in
  if len > 0 then let
      prval encode_v_succ pf = pf_bytes                     // 1
    in
      strptr_of_strbuf @(pfgc, pf | p_bytes)
    end
  else let  
      prval encode_v_fail pf = pf_bytes                    // 2
      val () = free_gc (pfgc, pf | p_bytes)
    in
      strptr_null ()
    end
end

The code is similar to the previous iteration until after the modp_b64_encode call. Once that call is made the proof pf_bytes is now an encode_v. This means we can no longer use the pointer p_bytes as no proof explaining what exactly it is pointing to is in scope.

We need to unpack the proof by pattern matching against the view. To do this we branch on a conditional based on the value of the length returned by modp_b64_encode. If this length is greater than zero we know pf_bytes is a encode_v_succ. We pattern match on it in the line marked 1 to extract our proof that p_bytes is an strbuf and can then turn that into a strptr and return it.

If the length is not greater than zero we know that pf_bytes must be an encode_v_fail. We pattern match on this in the line marked 2, extracting the proof that it is the original array of bytes we allocated. This is free'd in the following line and we return a null strptr. The type of string_to_base64 has changed to allow returning a null pointer.

We know the types of the encode_v proof based on the result length because this is encoded in the definition of encode_v. In that dataview definition we state what the valid values rlen is for each case. If our condition checks for the wrong value we get a type error on the pattern matching line. If we fail to handle the success or the failure case we get type errors for not consuming proofs correctly (eg. for not freeing the allocated memory on failure).

Conclusion

The result of our iterations ends up providing the following safety guarantees at compile time:

• We don't exceed the memory bounds of the source buffer
• We don't exceed the memory bounds of the destination buffer
• The destination buffer is at least the minimium size required by the function documentation
• We can't treat the destination buffer as a string if the function fails
• We can't treat the destination buffer as an array of bytes if the function succeeds
• Off by one errors due to null terminator handling are removed
• Checking to see if the function call failed is enforced

The complexity of the resulting definition is increased but someone familiar with ATS can read it and know what the function expects. The need to also read function documentation and find out things like the minimum size of the destination buffer is reduced.

When the ATS compiler compiles this code to C code the proof checking is removed. The resulting C code looks very much like handcoded C without runtime checks. Something like the following is generated:

char* string_to_base64(const char* s) {
  int s_len = strlen (s);
  int d_len = (s_len + 2) / 3 * 4 + 1;
  void* p_bytes = malloc (d_len)
  int len = modp_b64_encode (p_bytes, s, s_len);
  if (len > 0) 
    return (char*)p_bytes;
  else {
    free(p_bytes);
    return 0;
  }
}

H.264/AAC/MP3 decoding support for Firefox for Android

My last post on H.264/AAC/MP3 support for B2G briefly talked about Android. A couple of bugs landed recently on mozilla-central to provide support for playback of these formats on some Android devices:

• Bug 759945 - Stagefright decoding using software decoders
• Bug 782508 - Stagefright decoding using hardware decoders

Support for using these formats can be turned on or off using the preference media.plugins.enabled. It is turned on by default on nightly builds.

This is an early stage in the implementation and you should expect bugs and performance issues. Please test and raise bugs for anything you come across. I suspect that there will be issues with certain devices with the hardware decoding support. We need to find these and find fixes or workarounds for them.

Support is restricted to ICS and Jellybean devices with Gingerbread in development. The following devices have worked for me:

• Galaxy Note running ICS
• Nexus S running ICS
• Nexus S running Jellybean
• HTC One X (International) running ICS

The following bugs are known issues on specific devices:

• Bug 784329 - No video playback on Galaxy Nexus.
• Bug 783830 - Playback on Samsung Galaxy S3 intercepted by AwesomePlayer.

My mozilla-central git clone is stopping

For quite a while I've been maintaining a git mirror of the mercurial mozilla-central repository. My mirror has the history from the mercurial repository but they both lack the original CVS history as this was not converted when the change was made to use mercurial.

Recently a new git mirror containing the project history, including CVS, has become available in the mozilla-central github account. Now that this is available I will no longer be maintaining my own git mirror. The two repositories use different commit id's so are incompatible. I'll be deleting my repository in a few days to prevent confusion - already I've received a few emails asking why I have mine going when an official repository is available and I'd prefer to avoid people accidentally using it and getting confused when it's not compatible with the main one.

It's great to see a more official git mirror finally become available and thanks to those that have supported my efforts in the past.

Lightweight Tasks Library for ATS

I've been using libevent a fair bit recently from my systems developed in the ATS programming language. The resulting code is callback oriented and this programming style can result in difficult to follow code. Recently I ported a python programming using the twisted asynchronous network library to ATS and the callbacks were getting hard to manage. An example of the callback style is this sample libevent program which downloads and prints an HTML web page.

To help make this code easier to manage I wrote a lightweight task scheduler for ATS. It's available in github as ats-task. The implementation uses the ucontext stack switching API. To use the library from ATS it should be cloned as task in the $ATSHOME/contrib/ directory:

$ cd $ATSHOME/contrib
$ git clone git://github.com/doublec/ats-task task
$ cd task
$ make

The first step in using the library is to create a task scheduler and install this as the global scheduler:

var sch = scheduler_new ()
val () = set_global_scheduler (sch)

Once this is done tasks can be spawned. task_spawn takes a stack size and a linear closure (cloptr1) that is run when the task is scheduled:

val () = task_spawn (16384, lam () => {
                        val () = print ("hello\n")
                        val () = task_yield ()
                        val () = print ("world\n")
                     })

Tasks can yield using 'task_yield' which results in switching to the next task waiting to run, and scheduling itself to run again later.

The task scheduler needs to be activated with:

val () = run_global_scheduler ()

The scheduler exits when no more tasks are queued. The global scheduler must be unset and free'd:

val () = unset_global_scheduler (sch)
val () = scheduler_free (sch)

A compile error results if the scheduler is not unset or free'd.

To integrate with the libevent event loop I create a task that handles the event processing. It loops, processing any queued events if there are any. If no tasks are currently active it blocks when processing the event loop to prevent unneccesary polling:

fun event_loop_task {l:agz} (base: event_base l, events_queued: bool): void = let
  val () = task_yield ()
in
  (* If no events are queued and if no tasks are also queued we can exit *)
  if event_base_got_exit (base) > 0 || (not events_queued && task_queue_count () = 0) then {
    prval () = unref_base (base)
  }

  (* We're the only active task left, safe to block *)
  else if task_queue_count () = 0 then event_loop_task (base, event_base_loop (base, EVLOOP_ONCE) = 0)

  (* Other tasks are waiting, we can't block *)
  else event_loop_task (base, event_base_loop (base, EVLOOP_NONBLOCK) = 0)
end

This task is spawned and runs for as long as libevent is needed. When a libevent callback is registered, instead of implementing functionality in the callback the code instead spawns a task, or schedules threads in some other manner, so that it happens during the thread scheduler loop. An example is registering a function to run on an HTTP callback:

fun rpc_callback (req: evhttp_request1, proxy: !merge_mine_proxy): void = {
   val () = task_spawn_lin (16384, llam () => {
              val () = merge_mine_proxy_handle_getwork (pxy, req)
            })
 }
 val r = evhttp_set_cb {merge_mine_proxy} (http, "/", rpc_callback, proxy) 

task_spawn_lin is a variant of task_spawn that takes a lincloptr1 function type so it can close over linear objects and views. Now when the callback is called from libevent it spawns the task and immediately exits. The task will be run when it is scheduled during the task scheduler loop.

When making HTTP requests from libevent a callback is run when the result of the HTTP request is available. To integrate that with the task library we want to suspend a task when we make the HTTP request and resume it when the callback is run. The function global_scheduler_halt suspends the current running task and returns it. This can be rescheduled within a callback using global_scheduler_queue_task. global_scheduler_resume should be called to mark the point at which the task will start running when it is resumed. Sample code for this is:

fun download (url: string): http_result1 = let
  val tsk = global_scheduler_halt ()
  var result: http_result1
  prval (pff, pf) = __borrow (view@ result) where {
                      extern prfun __borrow {l:addr} (r: !http_result1? @ l >> (http_result1 @ l))
                                      : (http_result1 @ l -<lin,prf> void, http_result1? @ l)
                    }
  val () = http_request (url, llam (r) => {
                                val () = global_scheduler_queue_task (tsk)
                                val () = result := r
                                prval () = pff (pf)
                              })
  val () = global_scheduler_resume ()
in
  result
end

The callback for the download is passed to the http_request function. That callback receives a linear object containing the result of the HTTP request. In the code here we create a variable on the stack, result of type http_result1, to store the result. The __borrow proof function obtains a second view to this stack variable so it can be accessed from within the linear closure passed to http_request. In that closure it stores the result in the stack variable and consumes the proof. This is safe because task stacks are allocated on the heap so we can safely access result from within the closure as we have removed the tsk from the scheduler before that code is run and the stack cannot go away before then. __borrow returns a proof function and a view to the stack variable. That proof function consumes the returned view thus ensuring the proof must be consumed and not leaving any dangling data around.

The call to global_scheduler_resume is where computation will resume for the task when it is queued after the callback is called. The end result is allowing code like this to be written:

fn do_main (): void = {
  fn print_result (r: http_result1): void = 
    case+ r of 
    | ~http_result_string s => (print_strptr (s); print_newline (); strptr_free (s))
    | ~http_result_error code => printf("Code: %d", @(code))

  val () = print_result (download ("http://www.ats-lang.org/"))
  val () = print_result (download ("http://www.bluishcoder.co.nz/"))
}

This code processes the results of the download without exposing callbacks to the programmer. No garbage collector is used and linear types ensures that everything is correctly released and no memory leaked - otherwise the code doesn't compile.

I'm still tinkering with the API for the task library. In particular the use of a global scheduler and how the halt/queue/resume code looks. I wanted to have first class schedulers to allow creating a scheduler on each native CPU thread to allow tasks to belong to a CPU. I'm not sure if the current approach is right for that yet though. I'd like to add task communication using channels and similar constructs.

The python program I converted to ATS is now running on a bitcoin merge mining pool handling the back end merge mining requests. It has successfully handled up to 200 requests per second, each of which spawns a number of other HTTP requests to other back end services. The CPU load on the machine dropped from 80% with the python program to less than 10% with the ATS rewritten program and runs using much less memory.

For the curious, the pool uses Ur/Web for the front end web and payments interfaces and ATS for the back end pool share submission, processing and merge mining. One day I'll write a blog post detailing the progression of the pool development. It's gone from Mozart/Oz, Ur/Web and now a combination of Ur/Web and ATS. Eventually it'll be completely ATS. It's my project of choice for testing language runtimes for scalability issues. Maybe Rust or Idris will be the next languages to try it with.