Chapter 13. Introduction to Views and Viewtypes

Table of Contents
Views for Memory Access through Pointers
Viewtypes as a Combination of Views and Types
Left-Values and Call-by-Reference
Stack-Allocated Variables
Heap-Allocated Linear Closure-Functions

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.

Views for Memory Access through Pointers

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:

{l:addr} (T @ l | ptr (l)) -> (T @ l | T)

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:

{l:addr} (T? @ l | ptr (l), T) -> (T @ l | void)

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 //

Clearly, for each type T, the function ptr_get1<T> is assigned the following type:

{l:addr} (!T @ l >> T @ l | ptr(l)) -> T

Given a linear proof pf of the view T@L for some L and a pointer p of the type ptr(L), the function call ptr_get1<T>(pf, p) is expected to return a value of the type T. However, the proof pf is not consumed. Instead, it is still a proof of the view T@L after the function call returns. Similarly, the function ptr_set1<T> is assigned the following type:

{l:addr} (!T? @ l >> T @ l | ptr(l), T) -> void

Given a linear proof pf of the view T?@L for some L, a pointer p of the type ptr(L) and a value v of the type T, the function call ptr_set1<T>(pf, p, v) is expected to return the void value while changing the view of pf from T?@L to T@L. In general, assume that f is given a type of the following form for some views V1 and V2:

(...,!V1 >> V2, ...) -> ...

Then a function call f(..., pf, ...) on some proof variable pf of the view V1 is to change the view of pf into V2 upon its return. In the case where V1 and V2 are the same, !V1 >> V2 can simply be written as !V1. As an example, a function template swap1 for swapping the contents at two given memory locations is implemented as follows:

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]

Clearly, this implementation is considerably cleaner when compared to the above implementation of swap0.

A further simplied implementation of swap1 is given as follows:

fn{a:t@ype} swap1{l1,l2:addr} ( pf1: !a@l1, pf2: !a@l2 | p1: ptr (l1), p2: ptr (l2) ) : void = let val tmp = !p1 in !p1 := !p2; !p2 := tmp end // end of [swap1]

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.