Chapter 16. Abstract Views and Viewtypes

Table of Contents
Simple Linear Objects
Memory Allocation and Deallocation
Example: Array-Based Circular Buffers
Locking and Unlocking
Linear Channels for Asynchronous IPC

I have so far given a presentation of views that solely focuses on at-views and the views built on top of at-views. This is largely due to at-views being the form of most widely used views in practice and also being the first form of views supported in ATS. However, other forms of views can be readily introduced into ATS abstractly. Even in a case where a view can be defined based on at-views (or other forms of views), one may still want to introduce it as an abstract view (accompanied with certain proof functions for performing view-changes). Often what the programmer really needs is to figure out conceptually whether abstractly defined views and proof functions for manipulating them actually make sense. This is a bit like arguing whether a function is computable: There is rarely a need, if at all, to actually encode the function as a Turing-machine to prove its being computable. IMHO, learning proper use of abstract views and abstract viewtypes is a necessary step for one to take in order to employ linear types effectively in practice to deal with resource-related programming issues.

Simple Linear Objects

Objects in the physical world are conspicuously linear: They cannot be created from nothing or simply go vanished by turning into nothing. Thus, it is only natural to assign linear types to values that represent physical objects. I choose the name simple linear object here to refer to a linear value representing an object of some sort that does not contain built-in mechanism for supporting inheritance.

Let us now take a look at a concrete example of simple linear object. The following code presents an interface for a timer (that is, stopwatch):

// absvtype timer_vtype vtypedef timer = timer_vtype // fun timer_new (): timer fun timer_free (x: timer): void fun timer_start (x: !timer): void fun timer_finish (x: !timer): void fun timer_pause (x: !timer): void fun timer_resume (x: !timer): void fun timer_get_ntick (x: !timer): uint fun timer_reset (x: !timer): void //

The state of a timer is given the record type timer_struct defined as follows:

// typedef timer_struct = @{ started= bool // the timer has started , running= bool // the timer is running // the tick number recorded when the timer , ntick_beg= uint // was turned on last time , ntick_acc= uint // the number of accumulated ticks } (* end of [timer_struct] *) //

The following linear datatype timer is declared for timers, and the abstract type timer_vtype is assumed to equal timer:

// datavtype timer = TIMER of (timer_struct) // assume timer_vtype = timer //

Various functions on timers can now be readily implemented. Let us first see the code for creating and freeing timers:

implement timer_new () = let // val timer = TIMER (_) val TIMER (x) = timer // val () = x.started := false val () = x.running := false val () = x.ntick_beg := 0u val () = x.ntick_acc := 0u // prval () = fold@ (timer) // in timer end // end of [timer_new] implement timer_free (timer) = let val ~TIMER _ = timer in (*nothing*) end // end of [timer_free]

The function for starting a timer can be implemented as follows:

implement timer_start (timer) = let val+@TIMER(x) = timer val () = x.started := true val () = x.running := true val () = x.ntick_beg := the_current_tick_get () val () = x.ntick_acc := 0u prval () = fold@ (timer) in // nothing end // end of [timer_start]

where the_current_tick_get is a function for reading the current time (represented as a number of ticks):

extern fun the_current_tick_get (): uint

A timer can be stopped or paused. The function for stopping a timer can be implemented as follows:

implement timer_finish (timer) = let val+@TIMER(x) = timer val () = x.started := false val () = if x.running then { val () = x.running := false val () = x.ntick_acc := x.ntick_acc + the_current_tick_get () - x.ntick_beg } (* end of [val] *) prval () = fold@ (timer) in // nothing end // end of [timer_finish]

A timer can be paused and then resumed. The following code implements the functions for pausing and resuming a timer:

implement timer_pause (timer) = let val+@TIMER(x) = timer val () = if x.running then { val () = x.running := false val () = x.ntick_acc := x.ntick_acc + the_current_tick_get () - x.ntick_beg } (* end of [val] *) prval () = fold@ (timer) in // nothing end // end of [timer_pause] implement timer_resume (timer) = let val+@TIMER(x) = timer val () = if x.started && ~(x.running) then { val () = x.running := true val () = x.ntick_beg := the_current_tick_get () } (* end of [if] *) // end of [val] prval () = fold@ (timer) in // nothing end // end of [timer_resume]

As can be expected, the amount of time between the point where a timer is paused and the point where the timer is resumed is not counted.

It is also possible to reset a timer by calling the function timer_reset:

implement timer_reset (timer) = let val+@TIMER(x) = timer val () = x.started := false val () = x.running := false val () = x.ntick_beg := 0u val () = x.ntick_acc := 0u prval () = fold@ (timer) in // nothing end // end of [timer_reset]

In order to read the time accumulated by a timer, the function timer_get_ntick can be called:

implement timer_get_ntick (timer) = let val+@TIMER(x) = timer var ntick: uint = x.ntick_acc val () = if x.running then ( ntick := ntick + the_current_tick_get () - x.ntick_beg ) (* end of [if] *) // end of [val] prval () = fold@ (timer) in ntick end // end of [timer_get_ntick]

A straightforward approach to implementing the_current_tick_get can be based directly on the function clock_gettime:

local staload "libc/SATS/time.sats" in (* in-of-local *) implement the_current_tick_get () = let var tv: timespec // uninitialized val err = clock_gettime (CLOCK_REALTIME, tv) val ((*void*)) = assertloc (err >= 0) prval ((*void*)) = opt_unsome{timespec}(tv) in $UNSAFE.cast2uint(tv.tv_sec) end // end of [the_current_tick_get] end // end of [local]

Note that the library flag -lrt may be needed in order to have link-time access to clock_gettime as the function is in librt.

Please find on-line the entirety of the code presented in this section plus some testing code.