Probably the single greatest motivation behind the development of ATS is the desire to make ATS a programming language that can be employed effectively to construct safe and reliable programs running in the kernels of operating systems. Instead of following seemingly natural approaches that often focus on carving out a "safe" subset of C and/or put wrappers around "unsafe" programming features in C, ATS relies on the paradigm of programming with theorem-proving to prevent resources such as memory from being misused or mismanaged, advocating an approach to safety that is both general and flexible. For example, a well-typed program constructed in ATS cannot cause buffer overrun at run-time even though pointer arithmetic is fully supported in ATS. More specifically, if a pointer is to be dereferenced, ATS requires that a proof be given attesting to the safety of the dereferencing operation. Proofs of this kind are constructed to demonstrate the validity of linear propositions, which are referred to as views in ATS, for classifying resources as well as capabilities.
Please find on-line the code presented for illustration in this chapter.
A view is a linear version of prop, where the word linear comes from linear logic, a resource-aware logic invented by Jean-Yves Girard. There is a built-in sort view for static terms representing views. Given a type T and a memory location L, a view of the form T@L can be formed to indicate a value of the type T being stored in the memory at the location L, where @ is a special infix operator. Views of this form are extremely common in practice, and they are often referred to as at-views. As an example, the following function templates ptr_get0 and ptr_set0, which reads and writes through a given pointer, are assigned types containing at-views:
// fun{a:t@ype} ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a) // fun{a:t@ype} ptr_set0 {l:addr} (pf: a? @ l | p: ptr l, x: a): (a @ l | void) //
Note that ptr is a type constructor that forms a type ptr(L) when applied to a static term L of the sort addr, and the only value of the type ptr(L) is the pointer that points to the location denoted by L.
Given a type T, the function ptr_get0<T> is assigned the following type:
which indicates that the function ptr_get0<T> returns a proof of the view T@L and a value of the type T when applied to a proof of the view T@L and a pointer of the type ptr(L) for some L. Intuitively speaking, a proof of the view T@L, which is a form of resource as T@L is linear, is consumed when it is passed to ptr_get0<T>, and another proof of the same view T@L is generated when ptr_get0<T> returns. Notice that a proof of the view T@L must be returned for otherwise subsequent accesses to the memory location L would have been precluded.Similarly, the function ptr_set0<T> is assigned the following type:
Note that T? is a type for values of size sizeof(T) that are assumed to be uninitialized. The function ptr_set0<T> returns a proof of the view T@L when applied to a proof of the view T?@L, a pointer of the type ptr(L) and a value of the type T. The use of the view T?@L indicates that the memory location at L is assumed to be uninitialized when ptr_set0<T> is called.
As an example, a function template swap0 is implemented as follows for swapping memory contents at two given locations:
fn{a:t@ype} swap0{l1,l2:addr} ( pf1: a @ l1, pf2: a @ l2 | p1: ptr (l1), p2: ptr (l2) ) : (a @ l1, a @ l2 | void) = let val (pf1 | x1) = ptr_get0<a> (pf1 | p1) val (pf2 | x2) = ptr_get0<a> (pf2 | p2) val (pf1 | ()) = ptr_set0<a> (pf1 | p1, x2) val (pf2 | ()) = ptr_set0<a> (pf2 | p2, x1) in (pf1, pf2 | ()) end // end of [swap0]
Compared to a corresponding implementation in C, the verbosity of this one in ATS is evident. In particular, the need for threading linear proofs through calls to functions that make use of resources can often result in a lot of administrative code to be written. I now present some special syntax to significantly alleviate the need for such administrative code.
The function templates ptr_get1 and ptr_set1 are given the following interfaces:
// fun{a:t@ype} ptr_get1 {l:addr} (pf: !a @ l >> a @ l | p: ptr l): a // fun{a:t@ype} ptr_set1 {l:addr} (pf: !a? @ l >> a @ l | p: ptr l, x: a): void //
fn{a:t@ype} swap1{l1,l2:addr} ( pf1: !a@l1, pf2: !a@l2 | p1: ptr l1, p2: ptr l2 ) : void = let val x = ptr_get1<a> (pf1 | p1) val () = ptr_set1<a> (pf1 | p1, ptr_get1<a> (pf2 | p2)) val () = ptr_set1<a> (pf2 | p2, x) in // nothing end // end of [swap1]
A further simplied implementation of swap1 is given as follows:
Given a pointer p of the type ptr(L) for some L, !p yields the value stored at the memory location L. The typechecker first searches for a proof of the view T@L for some T among all the currently available proofs when typechecking !p; if such a proof pf is found, then !p is essentially elaborated into ptr_get1(pf | p) and then typechecked. As !p is a left-value (which is to be explained later in detail), it can also be used to form an assignment like !p := v for some value v. The typechecker elaborates !p := v into ptr_set1(pf | p, v) for the sake of typechecking if a proof of the at-view T@L can be found for some type T among all the currently available proofs. Note that this implementation of swap1 makes no use of administrative code for handling linear proofs explicitly.