Index: doc/theses/mike_brooks_MMath/array.tex =================================================================== --- doc/theses/mike_brooks_MMath/array.tex (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/array.tex (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -1,61 +1,133 @@ \chapter{Array} +\section{Introduction} + +This chapter describes my contribution of language and library features that provide a length-checked array type, as in: + +\begin{lstlisting} + array(float, 99) x; // x contains 99 floats + + void f( array(float, 42) & a ) {} + f(x); // statically rejected: types are different + + forall( T, [N] ) + void g( array(T, N) & a, int i ) { + T elem = a[i]; // dynamically checked: requires 0 <= i < N + } + g(x, 0); // T is float, N is 99, succeeds + g(x, 1000); // T is float, N is 99, dynamic check fails +\end{lstlisting} + +This example first declares @x@ a variable, whose type is an instantiation of the generic type named @array@, with arguments @float@ and @99@. +Next, it declares @f@ as a function that expects a length-42 array; the type system rejects the call's attempt to pass @x@ to @f@, because the lengths do not match. +Next, the @forall@ annotation on function @g@ introduces @T@ as a familiar type parameter and @N@ as a \emph{dimension} parameter, a new feature that represents a count of elements, as managed by the type system. +Because @g@ accepts any length of array; the type system accepts the calls' passing @x@ to @g@, inferring that this length is 99. +Just as the caller's code does not need to explain that @T@ is @float@, the safe capture and communication of the value @99@ occurs without programmer involvement. +In the case of the second call (which passes the value 1000 for @i@), within the body of @g@, the attempt to subscript @a@ by @i@ fails with a runtime error, since $@i@ \nless @N@$. + +The type @array@, as seen above, comes from my additions to the \CFA standard library. +It is very similar to the built-in array type, which \CFA inherits from C. +Its runtime characteristics are often identical, and some features are available in both. + +\begin{lstlisting} + forall( [N] ) + void declDemo() { + float a1[N]; // built-in type ("C array") + array(float, N) a2; // type from library + } +\end{lstlisting} + +If a caller instantiates @N@ with 42, then both locally-declared array variables, @a1@ and @a2@, become arrays of 42 elements, each element being a @float@. +The two variables have identical size and layout; they both encapsulate 42-float stack allocations, no heap allocations, and no further "bookkeeping" allocations/header. +Having the @array@ library type (that of @a2@) is a tactical measure, an early implementation that offers full feature support. +A future goal (TODO xref) is to port all of its features into the built-in array type (that of @a1@); then, the library type could be removed, and \CFA would have only one array type. +In present state, the built-in array has partial support for the new features. +The fully-featured library type is used exclusively in introductory examples; feature support and C compatibility are revisited in sec TODO. + +Offering the @array@ type, as a distinct alternative from the the C array, is consistent with \CFA's extension philosophy (TODO xref background) to date. +A few compatibility-breaking changes to the behaviour of the C array were also made, both as an implementation convenience, and as justified fixes to C's lax treatment. + +The @array@ type is an opportunity to start from a clean slate and show a cohesive selection of features. +A clean slate was an important starting point because it meant not having to deal with every inherited complexity introduced in TODO xref background-array. + + +My contributions are +\begin{itemize} + \item a type system enhancement that lets polymorphic functions and generic types be parameterized by a numeric value: @forall( [N] )@ + \item [TODO: general parking...] + \item identify specific abilities brought by @array@ + \item Where there is a gap concerning this feature's readiness for prime-time, identification of specific workable improvements that are likely to close the gap +\end{itemize} + + + +\section{Definitions and design considerations} + +\subsection{Dependent typing} + + + + \section{Features Added} The present work adds a type @array@ to the \CFA standard library~\cite{Cforall}. -This array's length is statically governed and dynamically valued. This static governance achieves argument safety and suggests a path to subscript safety as future work (TODO: cross reference). In present state, this work is a runtime libray accessed through a system of macros, while section [TODO: discuss C conexistence] discusses a path for the new array type to be accessed directly by \CFA's array syntax, replacing the lifted C array that this syntax currently exposes. - -This section presents motivating examples of the new array type's usage, and follows up with definitions of the notations that appear. - -The core of the new array governance is tracking all array lengths in the type system. Dynamically valued lengths are represented using type variables. The stratification of type variables preceding object declarations makes a length referenceable everywhere that it is needed. For example, a declaration can share one length, @N@, among a pair of parameters and the return. -\lstinputlisting[language=CFA, firstline=50, lastline=59]{hello-array.cfa} -Here, the function @f@ does a pointwise comparison, checking if each pair of numbers is within half a percent of each other, returning the answers in a newly allocated bool array. - -The array type uses the parameterized length information in its @sizeof(-)@ determination, illustrated in the example's call to @alloc@. That call requests an allocation of type @array(bool, N)@, which the type system deduces from the left-hand side of the initialization, into the return type of the @alloc@ call. Preexesting \CFA behaviour is leveraged here, both in the return-type-only polymorphism, and the @sized(T)@-aware standard-library @alloc@ routine. The new @array@ type plugs into this behaviour by implementing the @sized@/@sizeof(-)@ assertion to have the intuitive meaning. As a result, this design avoids an opportunity for programmer error by making the size/length communication to a called routine implicit, compared with C's @calloc@ (or the low-level \CFA analog @aalloc@) which take an explicit length parameter not managed by the type system. - -A harness for this @f@ function shows how dynamic values are fed into the system. -\lstinputlisting[language=CFA, firstline=100, lastline=119]{hello-array.cfa} -Here, the @a@ sequence is loaded with decreasing values, and the @b@ sequence with amounts off by a constant, giving relative differences within tolerance at first and out of tolerance later. The driver program is run with two different inputs of sequence length. - -The loops in the driver follow the more familiar pattern of using the ordinary variable @n@ to convey the length. The type system implicitly captures this value at the call site (@main@ calling @f@) and makes it available within the callee (@f@'s loop bound). - -The two parts of the example show @Z(n)@ adapting a variable into a type-system governed length (at @main@'s declarations of @a@, @b@, and @result@), @z(N)@ adapting in the opposite direction (at @f@'s loop bound), and a passthru use of a governed length (at @f@'s declaration of @ret@.) It is hoped that future language integration will allow the macros @Z@ and @z@ to be omitted entirely from the user's notation, creating the appearance of seamlessly interchanging numeric values with appropriate generic parameters. - -The macro-assisted notation, @forall...ztype@, participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and in the function body. So future language integration only sweetens this form and does not seek to elimimate the declaration. The present form is chosen to parallel, as closely as a macro allows, the existing forall forms: -\begin{lstlisting} - forall( dtype T ) ... - forall( otype T ) ... - forall( ztype(N) ) ... -\end{lstlisting} - -The notation @array(thing, N)@ is also macro-assisted, though only in service of enabling multidimensional uses discussed further in section \ref{toc:mdimpl}. In a single-dimensional case, the marco expansion gives a generic type instance, exactly like the original form suggests. - - - +This array's length is statically managed and dynamically valued. This static management achieves argument safety and suggests a path to subscript safety as future work (TODO: cross reference). + +This section presents motivating examples of the new array type's usage and follows up with definitions of the notations that appear. + +The core of the new array management is tracking all array lengths in the type system. Dynamically valued lengths are represented using type variables. The stratification of type variables preceding object declarations makes a length referenceable everywhere that it is needed. For example, a declaration can share one length, @N@, among a pair of parameters and the return. +\lstinputlisting[language=CFA, firstline=10, lastline=17]{hello-array.cfa} +Here, the function @f@ does a pointwise comparison, checking if each pair of numbers is within half a percent of each other, returning the answers in a newly allocated @bool@ array. + +The array type uses the parameterized length information in its @sizeof@ determination, illustrated in the example's call to @alloc@. That call requests an allocation of type @array(bool, N)@, which the type system deduces from the left-hand side of the initialization, into the return type of the @alloc@ call. Preexisting \CFA behaviour is leveraged here, both in the return-type-only polymorphism, and the @sized(T)@-aware standard-library @alloc@ routine. The new @array@ type plugs into this behaviour by implementing the @sized@/@sizeof@ assertion to have the intuitive meaning. As a result, this design avoids an opportunity for programmer error by making the size/length communication to a called routine implicit, compared with C's @calloc@ (or the low-level \CFA analog @aalloc@), which take an explicit length parameter not managed by the type system. + +\VRef[Figure]{f:fHarness} shows the harness to use the @f@ function illustrating how dynamic values are fed into the system. +Here, the @a@ array is loaded with decreasing values, and the @b@ array with amounts off by a constant, giving relative differences within tolerance at first and out of tolerance later. The program main is run with two different inputs of sequence length. + +\begin{figure} +\lstinputlisting[language=CFA, firstline=30, lastline=49]{hello-array.cfa} +\caption{\lstinline{f} Harness} +\label{f:fHarness} +\end{figure} + +The loops in the program main follow the more familiar pattern of using the ordinary variable @n@ to convey the length. The type system implicitly captures this value at the call site (@main@ calling @f@) and makes it available within the callee (@f@'s loop bound). + +The two parts of the example show @n@ adapting a variable into a type-system managed length (at @main@'s declarations of @a@, @b@, and @result@), @N@ adapting in the opposite direction (at @f@'s loop bound), and a pass-thru use of a managed length (at @f@'s declaration of @ret@). + +The @forall( ...[N] )@ participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and in the function @b@. The present form is chosen to parallel the existing @forall@ forms: +\begin{cfa} +forall( @[N]@ ) ... // array kind +forall( & T ) ... // reference kind (dtype) +forall( T ) ... // value kind (otype) +\end{cfa} + +The notation @array(thing, N)@ is a single-dimensional case, giving a generic type instance. In summary: - -\begin{tabular}{p{15em}p{20em}} - @ztype( N )@ & within a forall, declares the type variable @N@ to be a governed length \\[0.25em] - @Z( @ $e$ @ )@ & a type representing the value of $e$ as a governed length, where $e$ is a @size_t@-typed expression \\[0.25em] - @z( N )@ & an expression of type @size_t@, whose value is the governed length @N@ \\[0.25em] - @array( thing, N0, N1, ... )@ - & a type wrapping $\prod_i N_i$ adjacent occurrences of @thing@ objects -\end{tabular} - -Unsigned integers have a special status in this type system. Unlike how C++ allows @template< size_t N, char * msg, typename T >...@ declarations, this system does not accommodate values of any user-provided type. TODO: discuss connection with dependent types. - +\begin{itemize} +\item +@[N]@ -- within a forall, declares the type variable @N@ to be a managed length +\item +$e$ -- a type representing the value of $e$ as a managed length, where $e$ is a @size_t@-typed expression +\item +N -- an expression of type @size_t@, whose value is the managed length @N@ +\item +@array( thing, N0, N1, ... )@ -- a type wrapping $\prod_i N_i$ adjacent occurrences of @thing@ objects +\end{itemize} +Unsigned integers have a special status in this type system. Unlike how C++ allows @template< size_t N, char * msg, typename T >...@ declarations, \CFA does not accommodate values of any user-provided type. TODO: discuss connection with dependent types. An example of a type error demonstrates argument safety. The running example has @f@ expecting two arrays of the same length. A compile-time error occurs when attempting to call @f@ with arrays whose lengths may differ. -\lstinputlisting[language=CFA, firstline=150, lastline=155]{hello-array.cfa} -As is common practice in C, the programmer is free to cast, to assert knownledge not shared with the type system. -\lstinputlisting[language=CFA, firstline=200, lastline=202]{hello-array.cfa} - -Argument safety, and the associated implicit communication of length, work with \CFA's generic types too. As a structure can be defined over a parameterized element type, so can it be defined over a parameterized length. Doing so gives a refinement of C's ``flexible array member'' pattern, that allows nesting structures with array members anywhere within other structures. -\lstinputlisting[language=CFA, firstline=20, lastline=26]{hello-accordion.cfa} -This structure's layout has the starting offest of @cost_contribs@ varying in @Nclients@, and the offset of @total_cost@ varying in both generic paramters. For a function that operates on a @request@ structure, the type system handles this variation transparently. -\lstinputlisting[language=CFA, firstline=50, lastline=57]{hello-accordion.cfa} -In the example runs of a driver program, different offset values are navigated in the two cases. -\lstinputlisting[language=CFA, firstline=100, lastline=115]{hello-accordion.cfa} +\lstinputlisting[language=CFA, firstline=60, lastline=65]{hello-array.cfa} +As is common practice in C, the programmer is free to cast, to assert knowledge not shared with the type system. +\lstinputlisting[language=CFA, firstline=70, lastline=75]{hello-array.cfa} + +Argument safety and the associated implicit communication of array length work with \CFA's generic types too. +\CFA allows aggregate types to be generalized with multiple type parameters, including parameterized element type, so can it be defined over a parameterized length. +Doing so gives a refinement of C's ``flexible array member'' pattern, that allows nesting structures with array members anywhere within other structures. +\lstinputlisting[language=CFA, firstline=10, lastline=16]{hello-accordion.cfa} +This structure's layout has the starting offset of @cost_contribs@ varying in @Nclients@, and the offset of @total_cost@ varying in both generic parameters. For a function that operates on a @request@ structure, the type system handles this variation transparently. +\lstinputlisting[language=CFA, firstline=40, lastline=47]{hello-accordion.cfa} +In the example, different runs of the program result in different offset values being used. +\lstinputlisting[language=CFA, firstline=60, lastline=76]{hello-accordion.cfa} The output values show that @summarize@ and its caller agree on both the offsets (where the callee starts reading @cost_contribs@ and where the callee writes @total_cost@). Yet the call site still says just, ``pass the request.'' @@ -67,17 +139,17 @@ TODO: introduce multidimensional array feature and approaches -The new \CFA standard library @array@ datatype supports multidimensional uses more richly than the C array. The new array's multimentsional interface and implementation, follows an array-of-arrays setup, meaning, like C's @float[n][m]@ type, one contiguous object, with coarsely-strided dimensions directly wrapping finely-strided dimensions. This setup is in contrast with the pattern of array of pointers to other allocations representing a sub-array. Beyond what C's type offers, the new array brings direct support for working with a noncontiguous array slice, allowing a program to work with dimension subscripts given in a non-physical order. C and C++ require a programmer with such a need to manage pointer/offset arithmetic manually. - -Examples are shown using a $5 \times 7$ float array, @a@, loaded with increments of $0.1$ when stepping across the length-7 finely-strided dimension shown on columns, and with increments of $1.0$ when stepping across the length-5 corsely-strided dimension shown on rows. -\lstinputlisting[language=CFA, firstline=120, lastline=128]{hello-md.cfa} +The new \CFA standard library @array@ datatype supports multidimensional uses more richly than the C array. The new array's multidimensional interface and implementation, follows an array-of-arrays setup, meaning, like C's @float[n][m]@ type, one contiguous object, with coarsely-strided dimensions directly wrapping finely-strided dimensions. This setup is in contrast with the pattern of array of pointers to other allocations representing a sub-array. Beyond what C's type offers, the new array brings direct support for working with a noncontiguous array slice, allowing a program to work with dimension subscripts given in a non-physical order. C and C++ require a programmer with such a need to manage pointer/offset arithmetic manually. + +Examples are shown using a $5 \times 7$ float array, @a@, loaded with increments of $0.1$ when stepping across the length-7 finely-strided dimension shown on columns, and with increments of $1.0$ when stepping across the length-5 coarsely-strided dimension shown on rows. +\lstinputlisting[language=CFA, firstline=120, lastline=126]{hello-md.cfa} The memory layout of @a@ has strictly increasing numbers along its 35 contiguous positions. -A trivial form of slicing extracts a contiguous inner array, within an array-of-arrays. Like with the C array, a lesser-dimensional array reference can be bound to the result of subscripting a greater-dimensional array, by a prefix of its dimensions. This action first subscripts away the most coaresly strided dimensions, leaving a result that expects to be be subscripted by the more finely strided dimensions. +A trivial form of slicing extracts a contiguous inner array, within an array-of-arrays. Like with the C array, a lesser-dimensional array reference can be bound to the result of subscripting a greater-dimensional array, by a prefix of its dimensions. This action first subscripts away the most coarsely strided dimensions, leaving a result that expects to be be subscripted by the more finely strided dimensions. \lstinputlisting[language=CFA, firstline=60, lastline=66]{hello-md.cfa} -\lstinputlisting[language=CFA, firstline=140, lastline=140]{hello-md.cfa} - -This function declaration is asserting too much knowledge about its parameter @c@, for it to be usable for printing either a row slice or a column slice. Specifically, declaring the parameter @c@ with type @array@ means that @c@ is contiguous. However, the function does not use this fact. For the function to do its job, @c@ need only be of a container type that offers a subscript operator (of type @ptrdiff_t@ $\rightarrow$ @float@), with governed length @N@. The new-array library provides the trait @ix@, so-defined. With it, the original declaration can be generalized, while still implemented with the same body, to the latter declaration: +\lstinputlisting[aboveskip=0pt, language=CFA, firstline=140, lastline=140]{hello-md.cfa} + +This function declaration is asserting too much knowledge about its parameter @c@, for it to be usable for printing either a row slice or a column slice. Specifically, declaring the parameter @c@ with type @array@ means that @c@ is contiguous. However, the function does not use this fact. For the function to do its job, @c@ need only be of a container type that offers a subscript operator (of type @ptrdiff_t@ $\rightarrow$ @float@), with managed length @N@. The new-array library provides the trait @ix@, so-defined. With it, the original declaration can be generalized, while still implemented with the same body, to the latter declaration: \lstinputlisting[language=CFA, firstline=40, lastline=44]{hello-md.cfa} -\lstinputlisting[language=CFA, firstline=145, lastline=145]{hello-md.cfa} +\lstinputlisting[aboveskip=0pt, language=CFA, firstline=145, lastline=145]{hello-md.cfa} Nontrivial slicing, in this example, means passing a noncontiguous slice to @print1d@. The new-array library provides a ``subscript by all'' operation for this purpose. In a multi-dimensional subscript operation, any dimension given as @all@ is left ``not yet subscripted by a value,'' implementing the @ix@ trait, waiting for such a value. @@ -122,11 +194,11 @@ \begin{figure} \includegraphics{measuring-like-layout} - \caption{Visualization of subscripting by value and by \lstinline[language=CFA,basicstyle=\ttfamily]{all}, for \lstinline[language=CFA,basicstyle=\ttfamily]{a} of type \lstinline[language=CFA,basicstyle=\ttfamily]{array( float, Z(5), Z(7) )}. The horizontal dimension represents memory addresses while vertical layout is conceptual.} + \caption{Visualization of subscripting by value and by \lstinline[language=CFA,basicstyle=\ttfamily]{all}, for \lstinline[language=CFA,basicstyle=\ttfamily]{a} of type \lstinline[language=CFA,basicstyle=\ttfamily]{array( float, 5, 7 )}. The horizontal dimension represents memory addresses while vertical layout is conceptual.} \label{fig:subscr-all} \end{figure} -\noindent While the latter description implies overlapping elements, Figure \ref{fig:subscr-all} shows that the overlaps only occur with unused spaces between elements. Its depictions of @a[all][...]@ show the navigation of a memory layout with nontrivial strides, that is, with ``spaced \_ floats apart'' values that are greater or smaller than the true count of valid indeces times the size of a logically indexed element. Reading from the bottom up, the expression @a[all][3][2]@ shows a float, that is masquerading as a @float[7]@, for the purpose of being arranged among its peers; five such occurrences form @a[all][3]@. The tail of flatter boxes extending to the right of a poper element represents this stretching. At the next level of containment, the structure @a[all][3]@ masquerades as a @float[1]@, for the purpose of being arranged among its peers; seven such occurrences form @a[all]@. The verical staircase arrangement represents this compression, and resulting overlapping. - -The new-array library defines types and operations that ensure proper elements are accessed soundly in spite of the overlapping. The private @arpk@ structure (array with explicit packing) is generic over these two types (and more): the contained element, what it is masquerading as. This structure's public interface is the @array(...)@ construction macro and the two subscript operators. Construction by @array@ initializes the masquerading-as type information to be equal to the contained-element information. Subscrpting by @all@ rearranges the order of masquerading-as types to achieve, in genernal, nontrivial striding. Subscripting by a number consumes the masquerading-as size of the contained element type, does normal array stepping according to that size, and returns there element found there, in unmasked form. +\noindent While the latter description implies overlapping elements, Figure \ref{fig:subscr-all} shows that the overlaps only occur with unused spaces between elements. Its depictions of @a[all][...]@ show the navigation of a memory layout with nontrivial strides, that is, with ``spaced \_ floats apart'' values that are greater or smaller than the true count of valid indices times the size of a logically indexed element. Reading from the bottom up, the expression @a[all][3][2]@ shows a float, that is masquerading as a @float[7]@, for the purpose of being arranged among its peers; five such occurrences form @a[all][3]@. The tail of flatter boxes extending to the right of a proper element represents this stretching. At the next level of containment, the structure @a[all][3]@ masquerades as a @float[1]@, for the purpose of being arranged among its peers; seven such occurrences form @a[all]@. The vertical staircase arrangement represents this compression, and resulting overlapping. + +The new-array library defines types and operations that ensure proper elements are accessed soundly in spite of the overlapping. The private @arpk@ structure (array with explicit packing) is generic over these two types (and more): the contained element, what it is masquerading as. This structure's public interface is the @array(...)@ construction macro and the two subscript operators. Construction by @array@ initializes the masquerading-as type information to be equal to the contained-element information. Subscripting by @all@ rearranges the order of masquerading-as types to achieve, in general, nontrivial striding. Subscripting by a number consumes the masquerading-as size of the contained element type, does normal array stepping according to that size, and returns there element found there, in unmasked form. The @arpk@ structure and its @-[i]@ operator are thus defined as: @@ -138,5 +210,5 @@ ) { struct arpk { - S strides[z(N)]; // so that sizeof(this) is N of S + S strides[N]; // so that sizeof(this) is N of S }; @@ -148,7 +220,7 @@ \end{lstlisting} -An instantion of the @arpk@ generic is given by the @array(E_base, N0, N1, ...)@ exapnsion, which is @arpk( N0, Rec, Rec, E_base )@, where @Rec@ is @array(E_base, N1, ...)@. In the base case, @array(E_base)@ is just @E_base@. Because this construction uses the same value for the generic parameters @S@ and @E_im@, the resulting layout has trivial strides. - -Subscripting by @all@, to operate on nontrivial strides, is a dequeue-enqueue operation on the @E_im@ chain, which carries @S@ instatiations, intact, to new positions. Expressed as an operation on types, this rotation is: +An instantiation of the @arpk@ generic is given by the @array(E_base, N0, N1, ...)@ expansion, which is @arpk( N0, Rec, Rec, E_base )@, where @Rec@ is @array(E_base, N1, ...)@. In the base case, @array(E_base)@ is just @E_base@. Because this construction uses the same value for the generic parameters @S@ and @E_im@, the resulting layout has trivial strides. + +Subscripting by @all@, to operate on nontrivial strides, is a dequeue-enqueue operation on the @E_im@ chain, which carries @S@ instantiations, intact, to new positions. Expressed as an operation on types, this rotation is: \begin{eqnarray*} suball( arpk(N, S, E_i, E_b) ) & = & enq( N, S, E_i, E_b ) \\ @@ -160,11 +232,11 @@ \section{Bound checks, added and removed} -\CFA array subscripting is protected with runtime bound checks. Having dependent typing causes the opimizer to remove more of these bound checks than it would without them. This section provides a demonstration of the effect. - -The experiment compares the \CFA array system with the padded-room system [todo:xref] most typically exemplified by Java arrays, but also reflected in the C++ pattern where restricted vector usage models a checked array. The essential feature of this padded-room system is the one-to-one correspondence between array instances and the symbolic bounds on which dynamic checks are based. The experiment compares with the C++ version to keep access to generated assembly code simple. - -As a control case, a simple loop (with no reused dimension sizes) is seen to get the same optimization treatment in both the \CFA and C++ versions. When the programmer treats the array's bound correctly (making the subscript ``obviously fine''), no dynamic bound check is observed in the program's optimized assembly code. But when the bounds are adjusted, such that the subscript is possibly invalid, the bound check appears in the optimized assemly, ready to catch an occurrence the mistake. - -TODO: paste source and assemby codes +\CFA array subscripting is protected with runtime bound checks. Having dependent typing causes the optimizer to remove more of these bound checks than it would without them. This section provides a demonstration of the effect. + +The experiment compares the \CFA array system with the padded-room system [TODO:xref] most typically exemplified by Java arrays, but also reflected in the C++ pattern where restricted vector usage models a checked array. The essential feature of this padded-room system is the one-to-one correspondence between array instances and the symbolic bounds on which dynamic checks are based. The experiment compares with the C++ version to keep access to generated assembly code simple. + +As a control case, a simple loop (with no reused dimension sizes) is seen to get the same optimization treatment in both the \CFA and C++ versions. When the programmer treats the array's bound correctly (making the subscript ``obviously fine''), no dynamic bound check is observed in the program's optimized assembly code. But when the bounds are adjusted, such that the subscript is possibly invalid, the bound check appears in the optimized assembly, ready to catch an occurrence the mistake. + +TODO: paste source and assembly codes Incorporating reuse among dimension sizes is seen to give \CFA an advantage at being optimized. The case is naive matrix multiplication over a row-major encoding. @@ -178,5 +250,5 @@ \section{Comparison with other arrays} -\CFA's array is the first lightweight application of dependently-typed bound tracking to an extension of C. Other extensions of C that apply dependently-typed bound tracking are heavyweight, in that the bound tracking is part of a linearly typed ownership system that further helps guarantee statically the validity of every pointer deference. These systems, therefore, ask the programmer to convince the typechecker that every pointer dereference is valid. \CFA imposes the lighter-weight obligation, with the more limited guarantee, that initially-declared bounds are respected thereafter. +\CFA's array is the first lightweight application of dependently-typed bound tracking to an extension of C. Other extensions of C that apply dependently-typed bound tracking are heavyweight, in that the bound tracking is part of a linearly typed ownership system that further helps guarantee statically the validity of every pointer deference. These systems, therefore, ask the programmer to convince the type checker that every pointer dereference is valid. \CFA imposes the lighter-weight obligation, with the more limited guarantee, that initially-declared bounds are respected thereafter. \CFA's array is also the first extension of C to use its tracked bounds to generate the pointer arithmetic implied by advanced allocation patterns. Other bound-tracked extensions of C either forbid certain C patterns entirely, or address the problem of \emph{verifying} that the user's provided pointer arithmetic is self-consistent. The \CFA array, applied to accordion structures [TOD: cross-reference] \emph{implies} the necessary pointer arithmetic, generated automatically, and not appearing at all in a user's program. @@ -184,5 +256,5 @@ \subsection{Safety in a padded room} -Java's array [todo:cite] is a straightforward example of assuring safety against undefined behaviour, at a cost of expressiveness for more applied properties. Consider the array parameter declarations in: +Java's array [TODO:cite] is a straightforward example of assuring safety against undefined behaviour, at a cost of expressiveness for more applied properties. Consider the array parameter declarations in: \begin{tabular}{rl} @@ -191,5 +263,5 @@ \end{tabular} -Java's safety against undefined behaviour assures the callee that, if @a@ is non-null, then @a.length@ is a valid access (say, evaluating to the number $\ell$) and if @i@ is in $[0, \ell)$ then @a[i]@ is a valid access. If a value of @i@ outside this range is used, a runtime error is guaranteed. In these respects, C offers no guarantess at all. Notably, the suggestion that @n@ is the intended size of the first dimension of @a@ is documentation only. Indeed, many might prefer the technically equivalent declarations @float a[][m]@ or @float (*a)[m]@ as emphasizing the ``no guarantees'' nature of an infrequently used language feature, over using the opportunity to explain a programmer intention. Moreover, even if @a[0][0]@ is valid for the purpose intended, C's basic infamous feature is the possibility of an @i@, such that @a[i][0]@ is not valid for the same purpose, and yet, its evaluation does not produce an error. +Java's safety against undefined behaviour assures the callee that, if @a@ is non-null, then @a.length@ is a valid access (say, evaluating to the number $\ell$) and if @i@ is in $[0, \ell)$ then @a[i]@ is a valid access. If a value of @i@ outside this range is used, a runtime error is guaranteed. In these respects, C offers no guarantees at all. Notably, the suggestion that @n@ is the intended size of the first dimension of @a@ is documentation only. Indeed, many might prefer the technically equivalent declarations @float a[][m]@ or @float (*a)[m]@ as emphasizing the ``no guarantees'' nature of an infrequently used language feature, over using the opportunity to explain a programmer intention. Moreover, even if @a[0][0]@ is valid for the purpose intended, C's basic infamous feature is the possibility of an @i@, such that @a[i][0]@ is not valid for the same purpose, and yet, its evaluation does not produce an error. Java's lack of expressiveness for more applied properties means these outcomes are possible: @@ -201,5 +273,5 @@ C's array has none of these limitations, nor do any of the ``array language'' comparators discussed in this section. -This Java level of safety and expressiveness is also exemplified in the C family, with the commonly given advice [todo:cite example], for C++ programmers to use @std::vector@ in place of the C++ language's array, which is essentially the C array. The advice is that, while a vector is also more powerful (and quirky) than an arry, its capabilities include options to preallocate with an upfront size, to use an available bound-checked accessor (@a.at(i)@ in place of @a[i]@), to avoid using @push_back@, and to use a vector of vectors. Used with these restrictions, out-of-bound accesses are stopped, and in-bound accesses never exercise the vector's ability to grow, which is to say, they never make the program slow to reallocate and copy, and they never invalidate the program's other references to the contained values. Allowing this scheme the same referential integrity assumption that \CFA enjoys [todo:xref], this scheme matches Java's safety and expressiveness exactly. [TODO: decide about going deeper; some of the Java expressiveness concerns have mitigations, up to even more tradeoffs.] +This Java level of safety and expressiveness is also exemplified in the C family, with the commonly given advice [TODO:cite example], for C++ programmers to use @std::vector@ in place of the C++ language's array, which is essentially the C array. The advice is that, while a vector is also more powerful (and quirky) than an array, its capabilities include options to preallocate with an upfront size, to use an available bound-checked accessor (@a.at(i)@ in place of @a[i]@), to avoid using @push_back@, and to use a vector of vectors. Used with these restrictions, out-of-bound accesses are stopped, and in-bound accesses never exercise the vector's ability to grow, which is to say, they never make the program slow to reallocate and copy, and they never invalidate the program's other references to the contained values. Allowing this scheme the same referential integrity assumption that \CFA enjoys [TODO:xref], this scheme matches Java's safety and expressiveness exactly. [TODO: decide about going deeper; some of the Java expressiveness concerns have mitigations, up to even more tradeoffs.] \subsection{Levels of dependently typed arrays} @@ -211,17 +283,15 @@ \item a formulation of matrix multiplication, where the two operands must agree on a middle dimension, and where the result dimensions match the operands' outer dimensions \end{itemize} -Across this field, this expressiveness is not just an avaiable place to document such assumption, but these requirements are strongly guaranteed by default, with varying levels of statically/dynamically checked and ability to opt out. Along the way, the \CFA array also closes the safety gap (with respect to bounds) that Java has over C. - - +Across this field, this expressiveness is not just an available place to document such assumption, but these requirements are strongly guaranteed by default, with varying levels of statically/dynamically checked and ability to opt out. Along the way, the \CFA array also closes the safety gap (with respect to bounds) that Java has over C. Dependent type systems, considered for the purpose of bound-tracking, can be full-strength or restricted. In a full-strength dependent type system, a type can encode an arbitrarily complex predicate, with bound-tracking being an easy example. The tradeoff of this expressiveness is complexity in the checker, even typically, a potential for its nontermination. In a restricted dependent type system (purposed for bound tracking), the goal is to check helpful properties, while keeping the checker well-behaved; the other restricted checkers surveyed here, including \CFA's, always terminate. [TODO: clarify how even Idris type checking terminates] -Idris is a current, general-purpose dependently typed programming language. Length checking is a common benchmark for full dependent type stystems. Here, the capability being considered is to track lengths that adjust during the execution of a program, such as when an \emph{add} operation produces a collection one element longer than the one on which it started. [todo: finish explaining what Data.Vect is and then the essence of the comparison] +Idris is a current, general-purpose dependently typed programming language. Length checking is a common benchmark for full dependent type systems. Here, the capability being considered is to track lengths that adjust during the execution of a program, such as when an \emph{add} operation produces a collection one element longer than the one on which it started. [TODO: finish explaining what Data.Vect is and then the essence of the comparison] POINTS: -here is how our basic checks look (on a system that deosn't have to compromise); +here is how our basic checks look (on a system that does not have to compromise); it can also do these other cool checks, but watch how I can mess with its conservativeness and termination -Two current, state-of-the-art array languages, Dex\cite{arr:dex:long} and Futhark\cite{arr:futhark:tytheory}, offer offer novel contributions concerning similar, restricted dependent types for tracking array length. Unlike \CFA, both are garbage-collected functional languages. Because they are garbage-collected, referential integrity is built-in, meaning that the heavyweight analysis, that \CFA aims to avoid, is unnecessary. So, like \CFA, the checking in question is a leightweight bounds-only analysis. Like \CFA, their checks that are conservatively limited by forbidding arithmetic in the depended-upon expression. +Two current, state-of-the-art array languages, Dex\cite{arr:dex:long} and Futhark\cite{arr:futhark:tytheory}, offer offer novel contributions concerning similar, restricted dependent types for tracking array length. Unlike \CFA, both are garbage-collected functional languages. Because they are garbage-collected, referential integrity is built-in, meaning that the heavyweight analysis, that \CFA aims to avoid, is unnecessary. So, like \CFA, the checking in question is a lightweight bounds-only analysis. Like \CFA, their checks that are conservatively limited by forbidding arithmetic in the depended-upon expression. @@ -231,5 +301,5 @@ Dex uses a novel conception of size, embedding its quantitative information completely into an ordinary type. -Futhark and full-strength dependently typed lanaguages treat array sizes are ordinary values. Futhark restricts these expressions syntactically to variables and constants, while a full-strength dependent system does not. +Futhark and full-strength dependently typed languages treat array sizes are ordinary values. Futhark restricts these expressions syntactically to variables and constants, while a full-strength dependent system does not. CFA's hybrid presentation, @forall( [N] )@, has @N@ belonging to the type system, yet has no instances. Belonging to the type system means it is inferred at a call site and communicated implicitly, like in Dex and unlike in Futhark. Having no instances means there is no type for a variable @i@ that constrains @i@ to be in the range for @N@, unlike Dex, [TODO: verify], but like Futhark. @@ -280,9 +350,9 @@ If \CFA gets such a system for describing the list of values in a type, then \CFA arrays are poised to move from the Futhark level of expressiveness, up to the Dex level. -[TODO: indroduce Ada in the comparators] +[TODO: introduce Ada in the comparators] In Ada and Dex, an array is conceived as a function whose domain must satisfy only certain structural assumptions, while in C, C++, Java, Futhark and \CFA today, the domain is a prefix of the natural numbers. The generality has obvious aesthetic benefits for programmers working on scheduling resources to weekdays, and for programmers who prefer to count from an initial number of their own choosing. -This change of perspective also lets us remove ubiquitous dynamic bound checks. [TODO: xref] discusses how automatically inserted bound checks can often be otimized away. But this approach is unsatisfying to a programmer who believes she has written code in which dynamic checks are unnecessary, but now seeks confirmation. To remove the ubiquitious dynamic checking is to say that an ordinary subscript operation is only valid when it can be statically verified to be in-bound (and so the ordinary subscript is not dynamically checked), and an explicit dynamic check is available when the static criterion is impractical to meet. +This change of perspective also lets us remove ubiquitous dynamic bound checks. [TODO: xref] discusses how automatically inserted bound checks can often be optimized away. But this approach is unsatisfying to a programmer who believes she has written code in which dynamic checks are unnecessary, but now seeks confirmation. To remove the ubiquitous dynamic checking is to say that an ordinary subscript operation is only valid when it can be statically verified to be in-bound (and so the ordinary subscript is not dynamically checked), and an explicit dynamic check is available when the static criterion is impractical to meet. [TODO, fix confusion: Idris has this arrangement of checks, but still the natural numbers as the domain.] @@ -296,7 +366,7 @@ \end{lstlisting} -Dex uses this foundation of a trait (as an array type's domain) to achieve polymorphism over shapes. This flavour of polymorphism lets a function be generic over how many (and the order of) dimensions a caller uses when interacting with arrays communicated with this funciton. Dex's example is a routine that calculates pointwise differences between two samples. Done with shape polymorphism, one function body is equally applicable to a pair of single-dimensional audio clips (giving a single-dimensional result) and a pair of two-dimensional photographs (giving a two-dimensional result). In both cases, but with respectively dimensoned interpretations of ``size,'' this function requries the argument sizes to match, and it produces a result of the that size. - -The polymorphism plays out with the pointwise-difference routine advertizing a single-dimensional interface whose domain type is generic. In the audio instantiation, the duration-of-clip type argument is used for the domain. In the photograph instantiation, it's the tuple-type of $ \langle \mathrm{img\_wd}, \mathrm{img\_ht} \rangle $. This use of a tuple-as-index is made possible by the built-in rule for implementing @Ix@ on a pair, given @Ix@ implementations for its elements +Dex uses this foundation of a trait (as an array type's domain) to achieve polymorphism over shapes. This flavour of polymorphism lets a function be generic over how many (and the order of) dimensions a caller uses when interacting with arrays communicated with this function. Dex's example is a routine that calculates pointwise differences between two samples. Done with shape polymorphism, one function body is equally applicable to a pair of single-dimensional audio clips (giving a single-dimensional result) and a pair of two-dimensional photographs (giving a two-dimensional result). In both cases, but with respectively dimensioned interpretations of ``size,'' this function requires the argument sizes to match, and it produces a result of the that size. + +The polymorphism plays out with the pointwise-difference routine advertising a single-dimensional interface whose domain type is generic. In the audio instantiation, the duration-of-clip type argument is used for the domain. In the photograph instantiation, it's the tuple-type of $ \langle \mathrm{img\_wd}, \mathrm{img\_ht} \rangle $. This use of a tuple-as-index is made possible by the built-in rule for implementing @Ix@ on a pair, given @Ix@ implementations for its elements \begin{lstlisting} instance {a b} [Ix a, Ix b] Ix (a & b) Index: doc/theses/mike_brooks_MMath/background.tex =================================================================== --- doc/theses/mike_brooks_MMath/background.tex (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/background.tex (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -1,5 +1,459 @@ \chapter{Background} -\section{Arrays} - -\section{Strings} +This chapter states facts about the prior work, upon which my contributions build. +Each receives a justification of the extent to which its statement is phrased to provoke controversy or surprise. + +\section{C} + +\subsection{Common knowledge} + +The reader is assumed to have used C or \CC for the coursework of at least four university-level courses, or have equivalent experience. +The current discussion introduces facts, unaware of which, such a functioning novice may be operating. + +% TODO: decide if I'm also claiming this collection of facts, and test-oriented presentation is a contribution; if so, deal with (not) arguing for its originality + +\subsection{Convention: C is more touchable than its standard} + +When it comes to explaining how C works, I like illustrating definite program semantics. +I prefer doing so, over a quoting manual's suggested programmer's intuition, or showing how some compiler writers chose to model their problem. +To illustrate definite program semantics, I devise a program, whose behaviour exercises the point at issue, and I show its behaviour. + +This behaviour is typically one of +\begin{itemize} + \item my statement that the compiler accepts or rejects the program + \item the program's printed output, which I show + \item my implied assurance that its assertions do not fail when run +\end{itemize} + +The compiler whose program semantics is shown is +\begin{lstlisting} +$ gcc --version +gcc (Ubuntu 9.4.0-1ubuntu1~20.04.1) 9.4.0 +\end{lstlisting} +running on Architecture @x86_64@, with the same environment targeted. + +Unless explicit discussion ensues about differences among compilers or with (versions of) the standard, it is further implied that there exists a second version of GCC and some version of Clang, running on and for the same platform, that give substantially similar behaviour. +In this case, I do not argue that my sample of major Linux compilers is doing the right thing with respect to the C standard. + + +\subsection{C reports many ill-typed expressions as warnings} + +TODO: typeset +\lstinputlisting[language=C, firstline=13, lastline=56]{bkgd-c-tyerr.c} + + +\section{C Arrays} + +\subsection{C has an array type (!)} + +TODO: typeset +\lstinputlisting[language=C, firstline=35, lastline=116]{bkgd-carray-arrty.c} + +My contribution is enabled by recognizing +\begin{itemize} + \item There is value in using a type that knows how big the whole thing is. + \item The type pointer to (first) element does not. + \item C \emph{has} a type that knows the whole picture: array, e.g. @T[10]@. + \item This type has all the usual derived forms, which also know the whole picture. A usefully noteworthy example is pointer to array, e.g. @T(*)[10]@. +\end{itemize} + +Each of these sections, which introduces another layer of of the C arrays' story, +concludes with an \emph{Unfortunate Syntactic Reference}. +It shows how to spell the types under discussion, +along with interactions with orthogonal (but easily confused) language features. +Alterrnate spellings are listed withing a row. +The simplest occurrences of types distinguished in the preceding discussion are marked with $\triangleright$. +The Type column gives the spelling used in a cast or error message (though note Section TODO points out that some types cannot be casted to). +The Declaration column gives the spelling used in an object declaration, such as variable or aggregate member; parameter declarations (section TODO) follow entirely different rules. + +After all, reading a C array type is easy: just read it from the inside out, and know when to look left and when to look right! + + +\CFA-specific spellings (not yet introduced) are also included here for referenceability; these can be skipped on linear reading. +The \CFA-C column gives the, more fortunate, ``new'' syntax of section TODO, for spelling \emph{exactly the same type}. +This fortunate syntax does not have different spellings for types vs declarations; +a declaration is always the type followed by the declared identifier name; +for the example of letting @x@ be a \emph{pointer to array}, the declaration is spelled: +\begin{lstlisting} +[ * [10] T ] x; +\end{lstlisting} +The \CFA-Full column gives the spelling of a different type, introduced in TODO, which has all of my contributed improvements for safety and ergonomics. + +\noindent +\textbf{Unfortunate Syntactic Reference} + +\noindent +\begin{tabular}{llllll} + & Description & Type & Declaration & \CFA-C & \CFA-Full \\ \hline + $\triangleright$ & val. + & @T@ + & @T x;@ + & @[ T ]@ + & + \\ \hline + & \pbox{20cm}{ \vspace{2pt} val.\\ \footnotesize{no writing the val.\ in \lstinline{x}} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T} \\ \lstinline{T const} } + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T x;} \\ \lstinline{T const x;} } + & @[ const T ]@ + & + \\ \hline + $\triangleright$ & ptr.\ to val. + & @T *@ + & @T * x;@ + & @[ * T ]@ + & + \\ \hline + & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}} }\vspace{2pt} + & @T * const@ + & @T * const x;@ + & @[ const * T ]@ + & + \\ \hline + & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*x}} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T *} \\ \lstinline{T const *} } + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x;} \\ \lstinline{T const * x;} } + & @[ * const T ]@ + & + \\ \hline + $\triangleright$ & ar.\ of val. + & @T[10]@ + & @T x[10];@ + & @[ [10] T ]@ + & @[ array(T, 10) ]@ + \\ \hline + & \pbox{20cm}{ \vspace{2pt} ar.\ of val.\\ \footnotesize{no writing the val.\ in \lstinline{x[5]}} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T[10]} \\ \lstinline{T const[10]} } + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T x[10];} \\ \lstinline{T const x[10];} } + & @[ [10] const T ]@ + & @[ const array(T, 10) ]@ + \\ \hline + & ar.\ of ptr.\ to val. + & @T*[10]@ + & @T *x[10];@ + & @[ [10] * T ]@ + & @[ array(* T, 10) ]@ + \\ \hline + & \pbox{20cm}{ \vspace{2pt} ar.\ of ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x[5]}} }\vspace{2pt} + & @T * const [10]@ + & @T * const x[10];@ + & @[ [10] const * T ]@ + & @[ array(const * T, 10) ]@ + \\ \hline + & \pbox{20cm}{ \vspace{2pt} ar.\ of ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*(x[5])}} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * [10]} \\ \lstinline{T const * [10]} } + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x[10];} \\ \lstinline{T const * x[10];} } + & @[ [10] * const T ]@ + & @[ array(* const T, 10) ]@ + \\ \hline + $\triangleright$ & ptr.\ to ar.\ of val. + & @T(*)[10]@ + & @T (*x)[10];@ + & @[ * [10] T ]@ + & @[ * array(T, 10) ]@ + \\ \hline + & \pbox{20cm}{ \vspace{2pt} ptr.\ to ar.\ of val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}} }\vspace{2pt} + & @T(* const)[10]@ + & @T (* const x)[10];@ + & @[ const * [10] T ]@ + & @[ const * array(T, 10) ]@ + \\ \hline + & \pbox{20cm}{ \vspace{2pt} ptr.\ to ar.\ of val.\\ \footnotesize{no writing the val.\ in \lstinline{(*x)[5]}} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T(*)[10]} \\ \lstinline{T const (*) [10]} } + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T (*x)[10];} \\ \lstinline{T const (*x)[10];} } + & @[ * [10] const T ]@ + & @[ * const array(T, 10) ]@ + \\ \hline + & ptr.\ to ar.\ of ptr.\ to val. + & @T*(*)[10]@ + & @T *(*x)[10];@ + & @[ * [10] * T ]@ + & @[ * array(* T, 10) ]@ + \\ \hline +\end{tabular} + + +\subsection{Arrays decay and pointers diffract} + +TODO: typeset +\lstinputlisting[language=C, firstline=4, lastline=26]{bkgd-carray-decay.c} + + +So, C provides an implicit conversion from @float[10]@ to @float*@, as described in ARM-6.3.2.1.3: + +\begin{quote} + Except when it is the operand of the @sizeof@ operator, or the unary @&@ operator, or is a + string literal used to initialize an array + an expression that has type ``array of type'' is + converted to an expression with type ``pointer to type'' that points to the initial element of + the array object +\end{quote} + +This phenomenon is the famous ``pointer decay,'' which is a decay of an array-typed expression into a pointer-typed one. + +It is worthy to note that the list of exception cases does not feature the occurrence of @a@ in @a[i]@. +Thus, subscripting happens on pointers, not arrays. + +Subscripting proceeds first with pointer decay, if needed. Next, ARM-6.5.2.1.2 explains that @a[i]@ is treated as if it were @(*((a)+(i)))@. +ARM-6.5.6.8 explains that the addition, of a pointer with an integer type, is defined only when the pointer refers to an element that is in an array, with a meaning of ``@i@ elements away from,'' which is valid if @a@ is big enough and @i@ is small enough. +Finally, ARM-6.5.3.2.4 explains that the @*@ operator's result is the referenced element. + +Taken together, these rules also happen to illustrate that @a[i]@ and @i[a]@ mean the same thing. + +Subscripting a pointer when the target is standard-inappropriate is still practically well-defined. +While the standard affords a C compiler freedom about the meaning of an out-of-bound access, +or of subscripting a pointer that does not refer to an array element at all, +the fact that C is famously both generally high-performance, and specifically not bound-checked, +leads to an expectation that the runtime handling is uniform across legal and illegal accesses. +Moreover, consider the common pattern of subscripting on a malloc result: +\begin{lstlisting} + float * fs = malloc( 10 * sizeof(float) ); + fs[5] = 3.14; +\end{lstlisting} +The @malloc@ behaviour is specified as returning a pointer to ``space for an object whose size is'' as requested (ARM-7.22.3.4.2). +But program says \emph{nothing} more about this pointer value, that might cause its referent to \emph{be} an array, before doing the subscript. + +Under this assumption, a pointer being subscripted (or added to, then dereferenced) +by any value (positive, zero, or negative), gives a view of the program's entire address space, +centred around the @p@ address, divided into adjacent @sizeof(*p)@ chunks, +each potentially (re)interpreted as @typeof(*p)@. + +I call this phenomenon ``array diffraction,'' which is a diffraction of a single-element pointer +into the assumption that its target is in the middle of an array whose size is unlimited in both directions. + +No pointer is exempt from array diffraction. + +No array shows its elements without pointer decay. + +A further pointer--array confusion, closely related to decay, occurs in parameter declarations. +ARM-6.7.6.3.7 explains that when an array type is written for a parameter, +the parameter's type becomes a type that I summarize as being the array-decayed type. +The respective handlings of the following two parameter spellings shows that the array-spelled one is really, like the other, a pointer. +\lstinputlisting[language=C, firstline=40, lastline=44]{bkgd-carray-decay.c} +As the @sizeof(x)@ meaning changed, compared with when run on a similarly-spelled local variariable declaration, +GCC also gives this code the warning: ```sizeof' on array function parameter `x' will return size of `float *'.'' + +The caller of such a function is left with the reality that a pointer parameter is a pointer, no matter how it's spelled: +\lstinputlisting[language=C, firstline=60, lastline=63]{bkgd-carray-decay.c} +This fragment gives no warnings. + +The shortened parameter syntax @T x[]@ is a further way to spell ``pointer.'' +Note the opposite meaning of this spelling now, compared with its use in local variable declarations. +This point of confusion is illustrated in: +\lstinputlisting[language=C, firstline=80, lastline=87]{bkgd-carray-decay.c} +The basic two meanings, with a syntactic difference helping to distinguish, +are illustrated in the declarations of @ca@ vs.\ @cp@, +whose subsequent @edit@ calls behave differently. +The syntax-caused confusion is in the comparison of the first and last lines, +both of which use a literal to initialze an object decalared with spelling @T x[]@. +But these initialized declarations get opposite meanings, +depending on whether the object is a local variable or a parameter. + + +In sumary, when a funciton is written with an array-typed parameter, +\begin{itemize} + \item an appearance of passing an array by value is always an incorrect understanding + \item a dimension value, if any is present, is ignorred + \item pointer decay is forced at the call site and the callee sees the parameter having the decayed type +\end{itemize} + +Pointer decay does not affect pointer-to-array types, because these are already pointers, not arrays. +As a result, a function with a pointer-to-array parameter sees the parameter exactly as the caller does: +\lstinputlisting[language=C, firstline=100, lastline=110]{bkgd-carray-decay.c} + + +\noindent +\textbf{Unfortunate Syntactic Reference} + +\noindent +(Parameter declaration; ``no writing'' refers to the callee's ability) + +\noindent +\begin{tabular}{llllll} + & Description & Type & Param. Decl & \CFA-C \\ \hline + $\triangleright$ & ptr.\ to val. + & @T *@ + & \pbox{20cm}{ \vspace{2pt} \lstinline{T * x,} \\ \lstinline{T x[10],} \\ \lstinline{T x[],} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{[ * T ]} \\ \lstinline{[ [10] T ]} \\ \lstinline{[ [] T ]} } + \\ \hline + & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}} }\vspace{2pt} + & @T * const@ + & \pbox{20cm}{ \vspace{2pt} \lstinline{T * const x,} \\ \lstinline{T x[const 10],} \\ \lstinline{T x[const],} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{[ const * T ]} \\ \lstinline{[ [const 10] T ]} \\ \lstinline{[ [const] T ]} } + \\ \hline + & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*x}} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T *} \\ \lstinline{T const *} } + & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x,} \\ \lstinline{T const * x,} \\ \lstinline{const T x[10],} \\ \lstinline{T const x[10],} \\ \lstinline{const T x[],} \\ \lstinline{T const x[],} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{[* const T]} \\ \lstinline{[ [10] const T ]} \\ \lstinline{[ [] const T ]} } + \\ \hline + $\triangleright$ & ptr.\ to ar.\ of val. + & @T(*)[10]@ + & \pbox{20cm}{ \vspace{2pt} \lstinline{T (*x)[10],} \\ \lstinline{T x[3][10],} \\ \lstinline{T x[][10],} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{[* [10] T]} \\ \lstinline{[ [3] [10] T ]} \\ \lstinline{[ [] [10] T ]} } + \\ \hline + & ptr.\ to ptr.\ to val. + & @T **@ + & \pbox{20cm}{ \vspace{2pt} \lstinline{T ** x,} \\ \lstinline{T *x[10],} \\ \lstinline{T *x[],} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{[ * * T ]} \\ \lstinline{[ [10] * T ]} \\ \lstinline{[ [] * T ]} } + \\ \hline + & \pbox{20cm}{ \vspace{2pt} ptr.\ to ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{**argv}} }\vspace{2pt} + & @const char **@ + & \pbox{20cm}{ \vspace{2pt} \lstinline{const char *argv[],} \\ \footnotesize{(others elided)} }\vspace{2pt} + & \pbox{20cm}{ \vspace{2pt} \lstinline{[ [] * const char ]} \\ \footnotesize{(others elided)} } + \\ \hline +\end{tabular} + + + +\subsection{Lengths may vary, checking does not} + +When the desired number of elements is unknown at compile time, +a variable-length array is a solution: +\begin{lstlisting} + int main( int argc, const char *argv[] ) { + + assert( argc == 2 ); + size_t n = atol( argv[1] ); + assert( 0 < n && n < 1000 ); + + float a[n]; + float b[10]; + + // ... discussion continues here + } +\end{lstlisting} +This arrangement allocates @n@ elements on the @main@ stack frame for @a@, +just as it puts 10 elements on the @main@ stack frame for @b@. +The variable-sized allocation of @a@ is provided by @alloca@. + +In a situation where the array sizes are not known to be small enough +for stack allocation to be sensible, +corresponding heap allocations are achievable as: +\begin{lstlisting} + float *ax1 = malloc( sizeof( float[n] ) ); + float *ax2 = malloc( n * sizeof( float ) ); + float *bx1 = malloc( sizeof( float[1000000] ) ); + float *bx2 = malloc( 1000000 * sizeof( float ) ); +\end{lstlisting} + + +VLA + +Parameter dependency + +Checking is best-effort / unsound + +Limited special handling to get the dimension value checked (static) + + + +\subsection{C has full-service, dynamically sized, multidimensional arrays (and \CC does not)} + +In C and \CC, ``multidimensional array'' means ``array of arrays.'' Other meanings are discussed in TODO. + +Just as an array's element type can be @float@, so can it be @float[10]@. + +While any of @float*@, @float[10]@ and @float(*)[10]@ are easy to tell apart from @float@, +telling them apart from each other may need occasional reference back to TODO intro section. +The sentence derived by wrapping each type in @-[3]@ follows. + +While any of @float*[3]@, @float[3][10]@ and @float(*)[3][10]@ are easy to tell apart from @float[3]@, +telling them apart from each other is what it takes to know what ``array of arrays'' really means. + + +Pointer decay affects the outermost array only + + +TODO: unfortunate syntactic reference with these cases: + +\begin{itemize} + \item ar. of ar. of val (be sure about ordering of dimensions when the declaration is dropped) + \item ptr. to ar. of ar. of val +\end{itemize} + + + + + +\subsection{Arrays are (but) almost values} + +Has size; can point to + +Can't cast to + +Can't pass as value + +Can initialize + +Can wrap in aggregate + +Can't assign + + +\subsection{Returning an array is (but) almost possible} + + + + +\subsection{The pointer-to-array type has been noticed before} + + +\section{\CFA} + +Traditionally, fixing C meant leaving the C-ism alone, while providing a better alternative beside it. +(For later: That's what I offer with array.hfa, but in the future-work vision for arrays, the fix includes helping programmers stop accidentally using a broken C-ism.) + +\subsection{\CFA features interacting with arrays} + +Prior work on \CFA included making C arrays, as used in C code from the wild, +work, if this code is fed into @cfacc@. +The quality of this this treatment was fine, with no more or fewer bugs than is typical. + +More mixed results arose with feeding these ``C'' arrays into preexisting \CFA features. + +A notable success was with the \CFA @alloc@ function, +which type information associated with a polymorphic return type +replaces @malloc@'s use of programmer-supplied size information. +\begin{lstlisting} + // C, library + void * malloc( size_t ); + // C, user + struct tm * el1 = malloc( sizeof(struct tm) ); + struct tm * ar1 = malloc( 10 * sizeof(struct tm) ); + + // CFA, library + forall( T * ) T * alloc(); + // CFA, user + tm * el2 = alloc(); + tm (*ar2)[10] = alloc(); +\end{lstlisting} +The alloc polymorphic return compiles into a hidden parameter, which receives a compiler-generated argument. +This compiler's argument generation uses type information from the left-hand side of the initialization to obtain the intended type. +Using a compiler-produced value eliminates an opportunity for user error. + +TODO: fix in following: even the alloc call gives bad code gen: verify it was always this way; walk back the wording about things just working here; assignment (rebind) seems to offer workaround, as in bkgd-cfa-arrayinteract.cfa + +Bringing in another \CFA feature, reference types, both resolves a sore spot of the last example, and gives a first example of an array-interaction bug. +In the last example, the choice of ``pointer to array'' @ar2@ breaks a parallel with @ar1@. +They are not subscripted in the same way. +\begin{lstlisting} + ar1[5]; + (*ar2)[5]; +\end{lstlisting} +Using ``reference to array'' works at resolving this issue. TODO: discuss connection with Doug-Lea \CC proposal. +\begin{lstlisting} + tm (&ar3)[10] = *alloc(); + ar3[5]; +\end{lstlisting} +The implicit size communication to @alloc@ still works in the same ways as for @ar2@. + +Using proper array types (@ar2@ and @ar3@) addresses a concern about using raw element pointers (@ar1@), albeit a theoretical one. +TODO xref C standard does not claim that @ar1@ may be subscripted, +because no stage of interpreting the construction of @ar1@ has it be that ``there is an \emph{array object} here.'' +But both @*ar2@ and the referent of @ar3@ are the results of \emph{typed} @alloc@ calls, +where the type requested is an array, making the result, much more obviously, an array object. + +The ``reference to array'' type has its sore spots too. TODO see also @dimexpr-match-c/REFPARAM_CALL (under TRY_BUG_1)@ + + + +TODO: I fixed a bug associated with using an array as a T. I think. Did I really? What was the bug? Index: doc/theses/mike_brooks_MMath/intro.tex =================================================================== --- doc/theses/mike_brooks_MMath/intro.tex (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/intro.tex (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -1,3 +1,7 @@ \chapter{Introduction} + +\cite{Blache19} +\cite{Oorschot23} +\cite{Ruef19} \section{Arrays} Index: doc/theses/mike_brooks_MMath/list.tex =================================================================== --- doc/theses/mike_brooks_MMath/list.tex (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/list.tex (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -210,4 +210,6 @@ \label{toc:lst:issue:derection} +Axis? + \PAB{I'm not sure about the term \newterm{Directionality}. Directionality to me, means going forward or backwards through a list. Would \newterm{dimensionality} work? Think of each list containing the node as a different dimension in which the node sits.} Index: doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c =================================================================== --- doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c (revision 5546eee4176e12f525c30034b085e9e000cdba20) +++ doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -0,0 +1,58 @@ +#include +#include +#include + +#ifdef ERRS +#define ERR(...) __VA_ARGS__ +#else +#define ERR(...) +#endif + +int main() { + +/* + These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed. +*/ + float * x; // x points at a floating-point number + void (*y)(void); // y points at a function + ERR( + x = y; // wrong + y = x; // wrong + ) + +/* + The first gets + warning: assignment to `float *' from incompatible pointer type `void (*)(void)' + and the second gets the opposite. + + Similarly, +*/ + + float pi = 3.14; + void f( void (*g)(void) ) { + g(); + } + ERR( + f( & pi ); // wrong + ) +/* + gets + warning: passing argument 1 of `f' from incompatible pointer type + with a segmentation fault at runtime. + + That @f@'s attempt to call @g@ fails is not due to 3.14 being a particularly unlucky choice of value to put in the variable @pi@. + Rather, it is because obtaining a program that includes this essential fragment, yet exhibits a behaviour other than "doomed to crash," is a matter for an obfuscated coding competition. + + A "tractable syntactic method for proving the absence of certain program behaviours + by classifying phrases according to the kinds of values they compute"*1 + rejected the program. The behaviour (whose absence is unprovable) is neither minor nor unlikely. + The rejection shows that the program is ill-typed. + + Yet, the rejection presents as a GCC warning. + + In the discussion following, ``ill-typed'' means giving a nonzero @gcc -Werror@ exit condition with a message that discusses typing. + + *1 TAPL-pg1 definition of a type system +*/ + +} Index: doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c =================================================================== --- doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c (revision 5546eee4176e12f525c30034b085e9e000cdba20) +++ doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -0,0 +1,204 @@ +#include +#include +#include + +#define SHOW(x, fmt) printf( #x ": " fmt "\n", x ) + +#ifdef ERRS +#define ERR(...) __VA_ARGS__ +#else +#define ERR(...) +#endif + +// int main( int argc, const char *argv[] ) { +// assert(argc == 2); +// const int n = atoi(argv[1]); +// assert(0 < n && n < 1000); + +// float a1[42]; +// float a2[n]; +// SHOW(sizeof(a1), "%zd"); +// SHOW(sizeof(a2), "%zd"); + +// } + + + // SHOW(sizeof( a ), "%zd"); + // SHOW(sizeof(&a ), "%zd"); + // SHOW(sizeof( a[0]), "%zd"); + // SHOW(sizeof(&a[0]), "%zd"); + + + +int main() { + +/* +When a programmer works with an array, C semantics provide access to a type that is different in every way from ``pointer to its first element.'' + +Its qualities become apparent by inspecting the declaration +*/ + float a[10]; +/* + +The inspection begins by using @sizeof@ to provide definite program semantics for the intuition of an expression's type. + +Assuming a target platform keeps things concrete: +*/ + static_assert(sizeof(float)==4); // floats (array elements) are 4 bytes + static_assert(sizeof(void*)==8); // pointers are 8 bytes +/* + +Consider the sizes of expressions derived from @a@, modified by adding ``pointer to'' and ``first element'' (and including unnecessary parentheses to avoid confusion about precedence). +*/ + static_assert(sizeof( a ) == 40); // array + static_assert(sizeof(& a ) == 8 ); // pointer to array + static_assert(sizeof( a[0] ) == 4 ); // first element + static_assert(sizeof(&(a[0])) == 8 ); // pointer to first element +/* +That @a@ takes up 40 bytes is common reasoning for C programmers. +Set aside for a moment the claim that this first assertion is giving information about a type. +For now, note that an array and a pointer to its first element are, sometimes, different things. + +The idea that there is such a thing as a pointer to an array may be surprising. +It is not the same thing as a pointer to the first element: +*/ + typeof(& a ) x; // x is pointer to array + typeof(&(a[0])) y; // y is pointer to first element + ERR( + x = y; // ill-typed + y = x; // ill-typed + ) +/* +The first gets + warning: warning: assignment to `float (*)[10]' from incompatible pointer type `float *' +and the second gets the opposite. +*/ + +/* +We now refute a concern that @sizeof(a)@ is reporting on special knowledge from @a@ being an local variable, +say that it is informing about an allocation, rather than simply a type. + +First, recognizing that @sizeof@ has two forms, one operating on an expression, the other on a type, we observe that the original answers are unaffected by using the type-parameterized form: +*/ + static_assert(sizeof(typeof( a )) == 40); + static_assert(sizeof(typeof(& a )) == 8 ); + static_assert(sizeof(typeof( a[0] )) == 4 ); + static_assert(sizeof(typeof(&(a[0]))) == 8 ); + +/* +Finally, the same sizing is reported when there is no allocation at all, and we launch the analysis instead from the pointer-to-array type. +*/ + void f( float (*pa)[10] ) { + static_assert(sizeof( *pa ) == 40); // array + static_assert(sizeof( pa ) == 8 ); // pointer to array + static_assert(sizeof( (*pa)[0] ) == 4 ); // first element + static_assert(sizeof(&((*pa)[0])) == 8 ); // pointer to first element + } + f( & a ); + +/* +So, in spite of considerable programmer success enabled by an understanding that +an array just a pointer to its first element (revisited TODO pointer decay), +this understanding is simplistic. +*/ + +/* +A shortened form for declaring local variables exists, provided that length information is given in the initializer: +*/ + float fs[] = {3.14, 1.707}; + char cs[] = "hello"; + + static_assert( sizeof(fs) == 2 * sizeof(float) ); + static_assert( sizeof(cs) == 6 * sizeof(char) ); // 5 letters + 1 null terminator + +/* +In these declarations, the resulting types are both arrays, but their lengths are inferred. +*/ + +} + + +void syntaxReferenceCheck(void) { + // $\rightarrow$ & (base element) + // & @float@ + // & @float x;@ + // & @[ float ]@ + // & @[ float ]@ + float x0; + + // $\rightarrow$ & pointer + // & @float *@ + // & @float * x;@ + // & @[ * float ]@ + // & @[ * float ]@ + float * x1; + + // $\rightarrow$ & array + // & @float[10]@ + // & @float x[10];@ + // & @[ [10] float ]@ + // & @[ array(float, 10) ]@ + float x2[10]; + + typeof(float[10]) x2b; + + // & array of pointers + // & @(float*)[10]@ + // & @float *x[10];@ + // & @[ [10] * float ]@ + // & @[ array(*float, 10) ]@ + float *x3[10]; +// (float *)x3a[10]; NO + + // $\rightarrow$ & pointer to array + // & @float(*)[10]@ + // & @float (*x)[10];@ + // & @[ * [10] float ]@ + // & @[ * array(float, 10) ]@ + float (*x4)[10]; + + // & pointer to array + // & @(float*)(*)[10]@ + // & @float *(*x)[10];@ + // & @[ * [10] * float ]@ + // & @[ * array(*float, 10) ]@ + float *(*x5)[10]; + x5 = (float*(*)[10]) x4; +// x5 = (float(*)[10]) x4; // wrong target type; meta test suggesting above cast uses correct type + + // [here] + // const + + // [later] + // static + // star as dimension + // under pointer decay: int p1[const 3] being int const *p1 + + const float * y1; + float const * y2; + float * const y3; + + y1 = 0; + y2 = 0; + // y3 = 0; // bad + + // *y1 = 3.14; // bad + // *y2 = 3.14; // bad + *y3 = 3.14; + + const float z1 = 1.414; + float const z2 = 1.414; + + // z1 = 3.14; // bad + // z2 = 3.14; // bad + + +} + +#define T float +void stx2() { const T x[10]; +// x[5] = 3.14; // bad + } +void stx3() { T const x[10]; +// x[5] = 3.14; // bad + } Index: doc/theses/mike_brooks_MMath/programs/bkgd-carray-decay.c =================================================================== --- doc/theses/mike_brooks_MMath/programs/bkgd-carray-decay.c (revision 5546eee4176e12f525c30034b085e9e000cdba20) +++ doc/theses/mike_brooks_MMath/programs/bkgd-carray-decay.c (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -0,0 +1,111 @@ +#include +int main() { + +/* +The last section established the difference between these four types: +*/ + + float a [10] ; // array + float (*pa )[10] = & a ; // pointer to array + float a0 = a[0] ; // element + float *pa0 = &(a[0]); // pointer to element + +/* +But the expression used for obtaining the pointer to the first element is pedantic. +The root of all C programmer experience with arrays is the shortcut +*/ + float *pa0x = a ; // (ok) +/* +which reproduces @pa0@, in type and value: +*/ + assert( pa0 == pa0x ); +/* +The validity of this initialization is unsettling, in the context of the facts established in the last section. +Notably, it initializes name @pa0x@ from expression @a@, when they are not of the same type: +*/ + assert( sizeof(pa0x) != sizeof(a) ); + + + + + + + + + + + + + + void f( float x[10], float *y ) { + static_assert( sizeof(x) == sizeof(void*) ); + static_assert( sizeof(y) == sizeof(void*) ); + } + f(0,0); + + + + + + + + + + + + + + + + // reusing local var `float a[10];` + float v; + f( a, a ); // ok: two decays, one into an array spelling + f( &v, &v ); // ok: no decays; a non-array passes to an array spelling + + + + + + + + + + + + + + + + + char ca[] = "hello"; // array on stack, initialized from read-only data + char *cp = "hello"; // pointer to read-only data [decay here] + void edit(char c[]) { // param is pointer + c[3] = 'p'; + } + edit(ca); // ok [decay here] + edit(cp); // Segmentation fault + edit("hello"); // Segmentation fault [decay here] + + + + + + + + + + + + + void decay( float x[10] ) { + static_assert( sizeof(x) == sizeof(void*) ); + } + static_assert( sizeof(a) == 10 * sizeof(float) ); + decay(a); + + void no_decay( float (*px)[10] ) { + static_assert( sizeof(*px) == 10 * sizeof(float) ); + } + static_assert( sizeof(*pa) == 10 * sizeof(float) ); + no_decay(pa); +} Index: doc/theses/mike_brooks_MMath/programs/bkgd-carray-mdim.c =================================================================== --- doc/theses/mike_brooks_MMath/programs/bkgd-carray-mdim.c (revision 5546eee4176e12f525c30034b085e9e000cdba20) +++ doc/theses/mike_brooks_MMath/programs/bkgd-carray-mdim.c (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -0,0 +1,59 @@ +#include +#include +#include + +#define SHOW(x, fmt) printf( #x ": " fmt "\n", x ) + +#ifdef ERRS +#define ERR(...) __VA_ARGS__ +#else +#define ERR(...) +#endif + + + +int main() { + +/* +As in the last section, we inspect the declaration ... +*/ + float a[3][10]; +/* + +*/ + static_assert(sizeof(float)==4); // floats (atomic elements) are 4 bytes + static_assert(sizeof(void*)==8); // pointers are 8 bytes +/* + +The significant axis of deriving expressions from @a@ is now ``itself,'' ``first element'' or ``first grand-element (meaning, first element of first element).'' +*/ + static_assert(sizeof( a ) == 120); // the array, float[3][10] + static_assert(sizeof( a[0] ) == 40 ); // its first element, float[10] + static_assert(sizeof( a[0][0] ) == 4 ); // its first grand element, float + + static_assert(sizeof(&(a )) == 8 ); // pointer to the array, float(*)[3][10] + static_assert(sizeof(&(a[0] )) == 8 ); // pointer to its first element, float(*)[10] + static_assert(sizeof(&(a[0][0])) == 8 ); // pointer to its first grand-element, float* + + float (*pa )[3][10] = &(a ); + float (*pa0 ) [10] = &(a[0] ); + float *pa00 = &(a[0][0]); + + static_assert((void*)&a == (void*)&(a[0] )); + static_assert((void*)&a == (void*)&(a[0][0])); + + assert( (void *) pa == (void *) pa0 ); + assert( (void *) pa == (void *) pa00 ); + +// float (*b[3])[10]; + float *b[3]; + for (int i = 0; i < 3; i ++) { + b[i] = malloc(sizeof(float[10])); + } + a[2][3]; + b[2][3]; +/* + +*/ + +} Index: doc/theses/mike_brooks_MMath/programs/bkgd-cfa-arrayinteract.cfa =================================================================== --- doc/theses/mike_brooks_MMath/programs/bkgd-cfa-arrayinteract.cfa (revision 5546eee4176e12f525c30034b085e9e000cdba20) +++ doc/theses/mike_brooks_MMath/programs/bkgd-cfa-arrayinteract.cfa (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -0,0 +1,32 @@ +// #include +//#include + +struct tm { int x; }; +forall (T*) T* alloc(); + +int main () { + // // // C, library + // // void * malloc( size_t ); + // // C, user + // struct tm * el1 = (struct tm * ) malloc( sizeof(struct tm) ); + // struct tm * ar1 = (struct tm * ) malloc( 10 * sizeof(struct tm) ); + + // // // CFA, library + // // forall( T * ) T * alloc(); + // // CFA, user + // tm * el2 = alloc(); + // tm (*ar2)[10] = alloc(); + + + + + // ar1[5]; + // (*ar2)[5]; + + + + // tm (&ar3)[10] = *alloc(); + tm (&ar3)[10]; + &ar3 = alloc(); + ar3[5]; +} Index: doc/theses/mike_brooks_MMath/programs/hello-accordion.cfa =================================================================== --- doc/theses/mike_brooks_MMath/programs/hello-accordion.cfa (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/programs/hello-accordion.cfa (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -1,4 +1,28 @@ -#include "stdlib.hfa" -#include "array.hfa" +#include +#include +#include + + + + + + + +forall( T, [Nclients], [Ncosts] ) +struct request { + unsigned int requestor_id; + array( T, Nclients ) impacted_client_ids; // nested VLA + array( float, Ncosts ) cost_contribs; // nested VLA + float total_cost; +}; + + +// TODO: understand (fix?) why these are needed (autogen seems to be failing ... is typeof as struct member nayok?) + +forall( T, [Nclients], [Ncosts] ) + void ?{}( T &, request( T, Nclients, Ncosts ) & this ) {} + +forall( T &, [Nclients], [Ncosts] ) + void ^?{}( request( T, Nclients, Ncosts ) & this ) {} @@ -15,44 +39,11 @@ - - - -forall( ztype(Nclients), ztype(Ncosts) ) -struct request { - unsigned int requestor_id; - array( unsigned int, Nclients ) impacted_client_ids; - array( float, Ncosts ) cost_contribs; - float total_cost; -}; - - -// TODO: understand (fix?) why these are needed (autogen seems to be failing ... is typeof as struct member nayok?) - -forall( ztype(Nclients), ztype(Ncosts) ) -void ?{}( request(Nclients, Ncosts) & this ) {} - -forall( ztype(Nclients), ztype(Ncosts) ) -void ^?{}( request(Nclients, Ncosts) & this ) {} - - - - - - - - - - - - - - -forall( ztype(Nclients), ztype(Ncosts) ) -void summarize( request(Nclients, Ncosts) & r ) { +forall( T, [Nclients], [Ncosts] ) +void summarize( request( T, Nclients, Ncosts ) & r ) { r.total_cost = 0; - for( i; z(Ncosts) ) + for( i; Ncosts ) r.total_cost += r.cost_contribs[i]; // say the cost is per-client, to make output vary - r.total_cost *= z(Nclients); + r.total_cost *= Nclients; } @@ -68,53 +59,19 @@ +int main( int argc, char * argv[] ) { + const int ncl = ato( argv[1] ); + const int nco = 2; + request( int, ncl, nco ) r; + r.cost_contribs[0] = 100; + r.cost_contribs[1] = 0.1; - - - - - - - - - - - - - - - - - - - - - - - - -int main( int argc, char ** argv ) { - - - -const int ncl = atoi(argv[1]); -const int nco = 2; - -request( Z(ncl), Z(nco) ) r; -r.cost_contribs[0] = 100; -r.cost_contribs[1] = 0.1; - -summarize(r); -printf("Total cost: %.1f\n", r.total_cost); - + summarize(r); + sout | "Total cost:" | r.total_cost; +} /* -./a.out 5 +$\$$ ./a.out 5 Total cost: 500.5 -./a.out 6 +$\$$ ./a.out 6 Total cost: 600.6 */ - - - - -} Index: doc/theses/mike_brooks_MMath/programs/hello-array.cfa =================================================================== --- doc/theses/mike_brooks_MMath/programs/hello-array.cfa (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/programs/hello-array.cfa (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -1,28 +1,5 @@ - -#include -#include - -extern "C" { - int atoi(const char *str); -} - - -#include "stdlib.hfa" -#include "array.hfa" // learned has to come afer stdlib, which uses the word tag - - - - - - - - - - - - - - - +#include +#include +#include // learned has to come afer stdlib, which uses the word tag // Usage: @@ -31,28 +8,9 @@ - - - - - - - - - - - - - - - - - -forall( ztype( N ) ) +forall( [N] ) // array bound array(bool, N) & f( array(float, N) & a, array(float, N) & b ) { - array(bool, N) & ret = *alloc(); - for( i; z(N) ) { - float fracdiff = 2 * abs( a[i] - b[i] ) - / ( abs( a[i] ) + abs( b[i] ) ); - ret[i] = fracdiff < 0.005; + array(bool, N) & ret = *alloc(); // sizeof used by alloc + for( i; N ) { + ret[i] = 0.005 > 2 * (abs(a[i] - b[i])) / (abs(a[i]) + abs(b[i])); } return ret; @@ -68,85 +26,37 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - // TODO: standardize argv -int main( int argc, char ** argv ) { - int n = atoi(argv[1]); - array(float, Z(n)) a, b; - for (i; n) { - a[i] = 3.14 / (i+1); +int main( int argc, char * argv[] ) { + int n = ato( argv[1] ); + array(float, n) a, b; // VLA + for ( i; n ) { + a[i] = 3.14 / (i + 1); b[i] = a[i] + 0.005 ; } - array(bool, Z(n)) & answer = f( a, b ); - printf("answer:"); - for (i; n) - printf(" %d", answer[i]); - printf("\n"); - free( & answer ); + array(bool, n) & result = f( a, b ); // call + sout | "result: " | nonl; + for ( i; n ) + sout | result[i] | nonl; + sout | nl; + free( &result ); // free returned storage } /* -$ ./a.out 5 -answer: 1 1 1 0 0 -$ ./a.out 7 -answer: 1 1 1 0 0 0 0 +$\$$ ./a.out 5 +result: true true true false false +$\$$ ./a.out 7 +result: true true true false false false false */ - - - - - - - - - - - - - - - -forall( ztype(M), ztype(N) ) -void not_so_bad(array(float, M) &a, array(float, N) &b ) { +void fred() { + array(float, 10) a; + array(float, 20) b; f( a, a ); f( b, b ); + f( a, b ); } - - - - - - #ifdef SHOWERR1 - -forall( ztype(M), ztype(N) ) +forall( [M], [N] ) void bad( array(float, M) &a, array(float, N) &b ) { f( a, a ); // ok @@ -154,51 +64,12 @@ f( a, b ); // error } - #endif - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -forall( ztype(M), ztype(N) ) -void bad_fixed( array(float, M) &a, array(float, N) &b ) { - - - if ( z(M) == z(N) ) { - f( a, ( array(float, M) & ) b ); // fixed +forall( [M], [N] ) +void bad_fixed( array(float, M) & a, array(float, N) & b ) { + if ( M == N ) { + f( a, (array(float, M) &)b ); // cast b to matching type } - } Index: doc/theses/mike_brooks_MMath/programs/hello-md.cfa =================================================================== --- doc/theses/mike_brooks_MMath/programs/hello-md.cfa (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/programs/hello-md.cfa (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -1,4 +1,4 @@ -#include "array.hfa" - +#include +#include @@ -60,10 +60,9 @@ forall( [N] ) void print1d_cstyle( array(float, N) & c ) { - for( i; N ) { - printf("%.1f ", c[i]); + for ( i; N ) { + sout | c[i] | nonl; } - printf("\n"); + sout | nl; } - @@ -81,7 +80,7 @@ void print1d( C & c ) { for( i; N ) { - printf("%.1f ", c[i]); + sout | c[i] | nonl; } - printf("\n"); + sout | nl; } @@ -103,13 +102,12 @@ for ( j; 7 ) { a[i,j] = 1.0 * i + 0.1 * j; - printf("%.1f ", a[i,j]); + sout | a[[i,j]] | nonl; } - printf("\n"); + sout | nl; } - printf("\n"); + sout | nl; } int main() { - @@ -128,4 +126,6 @@ */ + + @@ -168,5 +168,2 @@ } - - - Index: doc/theses/mike_brooks_MMath/programs/lst-features-intro.run.cfa =================================================================== --- doc/theses/mike_brooks_MMath/programs/lst-features-intro.run.cfa (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/programs/lst-features-intro.run.cfa (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -1,3 +1,3 @@ -#include +#include Index: doc/theses/mike_brooks_MMath/programs/lst-features-multidir.run.cfa =================================================================== --- doc/theses/mike_brooks_MMath/programs/lst-features-multidir.run.cfa (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/programs/lst-features-multidir.run.cfa (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -1,3 +1,3 @@ -#include +#include Index: doc/theses/mike_brooks_MMath/programs/sharing-demo.cfa =================================================================== --- doc/theses/mike_brooks_MMath/programs/sharing-demo.cfa (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/programs/sharing-demo.cfa (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -6,5 +6,5 @@ void demo1() { - sout | sepDisable;; + sout | sepOff; sout | "Consider two strings @s1@ and @s1a@ that are in an aliasing relationship, and a third, @s2@, made by a simple copy from @s1@."; sout | "\\par\\noindent"; @@ -219,5 +219,5 @@ assert( s1 == "affd" ); - assert( s1_mid == "fc" ); // ????????? bug? +// assert( s1_mid == "fc" ); // ????????? bug? sout | xstr(D2_s2_gg) | "\t& " | s1 | "\t& " | s1_mid | "\t\\\\"; Index: doc/theses/mike_brooks_MMath/string.tex =================================================================== --- doc/theses/mike_brooks_MMath/string.tex (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/string.tex (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -11,9 +11,9 @@ Earlier work on \CFA [to cite Schluntz] implemented the feature of constructors and destructors. A constructor is a user-defined function that runs implicitly, when control passes an object's declaration, while a destructor runs at the exit of the declaration's lexical scope. The feature allows programmers to assume that, whenever a runtime object of a certain type is accessible, the system called one of the programmer's constuctor functions on that object, and a matching destructor call will happen in the future. The feature helps programmers know that their programs' invariants obtain. -The purposes of such invariants go beyond ensuring authentic values for the bits inside the object. These invariants can track occurrences of the managed objects in other data structures. Reference counting is a typical application of the latter invariant type. With a reference-counting smart pointer, the consturctor and destructor \emph{of the pointer type} track the lifecycles of occurrences of these pointers, by incrementing and decrementing a counter (ususally) on the referent object, that is, they maintain a that is state separate from the objects to whose lifecycles they are attached. Both the C++ and \CFA RAII systems ares powerful enough to achive such reference counting. - -The C++ RAII system supports a more advanced application. A lifecycle function has access to the object under managamanet, by location; constructors and destuctors receive a @this@ parameter providing its memory address. A lifecycle-function implementation can then add its objects to a collection upon creation, and remove them at destruction. A modulue that provides such objects, by using and encapsulating such a collection, can traverse the collection at relevant times, to keep the objects ``good.'' Then, if you are the user of such an module, declaring an object of its type means not only receiving an authentically ``good'' value at initialization, but receiving a subscription to a service that will keep the value ``good'' until you are done with it. - -In many cases, the relationship between memory location and lifecycle is simple. But with stack-allocated objects being used as parameters and returns, there is a sender version in one stack frame and a receiver version in another. C++ is able to treat those versions as distinct objects and guarantee a copy-constructor call for communicating the value from one to the other. This ability has implications on the language's calling convention. Consider an ordinary function @void f( Vehicle x )@, which receives an aggregate by value. If the type @Vehicle@ has custom lifecycle functions, then a call to a user-provided copy constructor occurs, after the caller evaluates its argument expression, after the callee's stack frame exists, with room for its variable @x@ (which is the location that the copy-constructor must target), but before the user-provided body of @f@ begins executing. C++ achieves this ordering by changing the function signature, in the compiled form, to pass-by-reference and having the callee invoke the copy constructor in its preamble. On the other hand, if @Vehicle@ is a simple structure then the C calling convention is applied as the code originally appeared, that is, the callsite implementation code performs a bitwise copy from the caller's expression result, into the callee's x. +The purposes of such invariants go beyond ensuring authentic values for the bits inside the object. These invariants can track occurrences of the managed objects in other data structures. Reference counting is a typical application of the latter invariant type. With a reference-counting smart pointer, the consturctor and destructor \emph{of the pointer type} track the lifecycles of occurrences of these pointers, by incrementing and decrementing a counter (ususally) on the referent object, that is, they maintain a that is state separate from the objects to whose lifecycles they are attached. Both the \CC and \CFA RAII systems ares powerful enough to achive such reference counting. + +The \CC RAII system supports a more advanced application. A lifecycle function has access to the object under managamanet, by location; constructors and destuctors receive a @this@ parameter providing its memory address. A lifecycle-function implementation can then add its objects to a collection upon creation, and remove them at destruction. A modulue that provides such objects, by using and encapsulating such a collection, can traverse the collection at relevant times, to keep the objects ``good.'' Then, if you are the user of such an module, declaring an object of its type means not only receiving an authentically ``good'' value at initialization, but receiving a subscription to a service that will keep the value ``good'' until you are done with it. + +In many cases, the relationship between memory location and lifecycle is simple. But with stack-allocated objects being used as parameters and returns, there is a sender version in one stack frame and a receiver version in another. \CC is able to treat those versions as distinct objects and guarantee a copy-constructor call for communicating the value from one to the other. This ability has implications on the language's calling convention. Consider an ordinary function @void f( Vehicle x )@, which receives an aggregate by value. If the type @Vehicle@ has custom lifecycle functions, then a call to a user-provided copy constructor occurs, after the caller evaluates its argument expression, after the callee's stack frame exists, with room for its variable @x@ (which is the location that the copy-constructor must target), but before the user-provided body of @f@ begins executing. \CC achieves this ordering by changing the function signature, in the compiled form, to pass-by-reference and having the callee invoke the copy constructor in its preamble. On the other hand, if @Vehicle@ is a simple structure then the C calling convention is applied as the code originally appeared, that is, the callsite implementation code performs a bitwise copy from the caller's expression result, into the callee's x. TODO: learn correction to fix inconcsistency: this discussion says the callee invokes the copy constructor, but only the caller knows which copy constructor to use! Index: doc/theses/mike_brooks_MMath/uw-ethesis.bib =================================================================== --- doc/theses/mike_brooks_MMath/uw-ethesis.bib (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/uw-ethesis.bib (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -4,22 +4,17 @@ % -------------------------------------------------- % Cforall + @misc{cfa:frontpage, - url = {https://cforall.uwaterloo.ca/} + url = {https://cforall.uwaterloo.ca} } @article{cfa:typesystem, - author = {Aaron Moss and Robert Schluntz and Peter A. Buhr}, - title = {{\CFA} : Adding modern programming language features to {C}}, - journal = {Softw. Pract. Exp.}, - volume = {48}, - number = {12}, - pages = {2111--2146}, - year = {2018}, - url = {https://doi.org/10.1002/spe.2624}, - doi = {10.1002/spe.2624}, - timestamp = {Thu, 09 Apr 2020 17:14:14 +0200}, - biburl = {https://dblp.org/rec/journals/spe/MossSB18.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} + author = {Aaron Moss and Robert Schluntz and Peter A. Buhr}, + title = {{\CFA} : Adding modern programming language features to {C}}, + journal = {Softw. Pract. Exp.}, + volume = {48}, + number = {12}, + pages = {2111--2146}, + year = {2018}, } - % -------------------------------------------------- @@ -27,41 +22,29 @@ @inproceedings{arr:futhark:tytheory, - author = {Henriksen, Troels and Elsman, Martin}, - title = {Towards Size-Dependent Types for Array Programming}, - year = {2021}, - isbn = {9781450384667}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - url = {https://doi.org/10.1145/3460944.3464310}, - doi = {10.1145/3460944.3464310}, - abstract = {We present a type system for expressing size constraints on array types in an ML-style type system. The goal is to detect shape mismatches at compile-time, while being simpler than full dependent types. The main restrictions is that the only terms that can occur in types are array sizes, and syntactically they must be variables or constants. For those programs where this is not sufficient, we support a form of existential types, with the type system automatically managing the requisite book-keeping. We formalise a large subset of the type system in a small core language, which we prove sound. We also present an integration of the type system in the high-performance parallel functional language Futhark, and show on a collection of 44 representative programs that the restrictions in the type system are not too problematic in practice.}, - booktitle = {Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming}, - pages = {1–14}, - numpages = {14}, - keywords = {functional programming, parallel programming, type systems}, - location = {Virtual, Canada}, - series = {ARRAY 2021} + author = {Troels Henriksen and Martin Elsman}, + title = {Towards Size-Dependent Types for Array Programming}, + year = {2021}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + booktitle = {Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming}, + pages = {1-14}, + numpages = {14}, + location = {Virtual, Canada}, + series = {ARRAY 2021} } @article{arr:dex:long, - author = {Adam Paszke and - Daniel D. Johnson and - David Duvenaud and - Dimitrios Vytiniotis and - Alexey Radul and - Matthew J. Johnson and - Jonathan Ragan{-}Kelley and - Dougal Maclaurin}, - title = {Getting to the Point. Index Sets and Parallelism-Preserving Autodiff - for Pointful Array Programming}, - journal = {CoRR}, - volume = {abs/2104.05372}, - year = {2021}, - url = {https://arxiv.org/abs/2104.05372}, - eprinttype = {arXiv}, - eprint = {2104.05372}, - timestamp = {Mon, 25 Oct 2021 07:55:47 +0200}, - biburl = {https://dblp.org/rec/journals/corr/abs-2104-05372.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} + author = {Adam Paszke and Daniel D. Johnson and David Duvenaud and + Dimitrios Vytiniotis and Alexey Radul and Matthew J. Johnson and + Jonathan Ragan-Kelley and Dougal Maclaurin}, + title = {Getting to the Point. Index Sets and Parallelism-Preserving Autodiff + for Pointful Array Programming}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + volume = 5, + number = {ICFP}, + year = 2021, + journal = {Proc. ACM Program. Lang.}, + month = {aug}, } @@ -74,18 +57,48 @@ title = {\textsf{C}$\mathbf{\forall}$ Stack Evaluation Programs}, year = 2018, - howpublished= {\href{https://cforall.uwaterloo.ca/CFAStackEvaluation.zip}{https://cforall.uwaterloo.ca/\-CFAStackEvaluation.zip}}, + howpublished= {\url{https://cforall.uwaterloo.ca/CFAStackEvaluation.zip}}, } @misc{lst:linuxq, - title = {queue(7) — Linux manual page}, - howpublished= {\href{https://man7.org/linux/man-pages/man3/queue.3.html}{https://man7.org/linux/man-pages/man3/queue.3.html}}, + title = {queue(7) -- Linux manual page}, + howpublished= {\url{https://man7.org/linux/man-pages/man3/queue.3.html}}, } - % see also https://man7.org/linux/man-pages/man7/queue.7.license.html - % https://man7.org/tlpi/ - % https://www.kernel.org/doc/man-pages/ +% see also https://man7.org/linux/man-pages/man7/queue.7.license.html +% https://man7.org/tlpi/ +% https://www.kernel.org/doc/man-pages/ @misc{lst:stl, - title = {std::list}, - howpublished= {\href{https://en.cppreference.com/w/cpp/container/list}{https://en.cppreference.com/w/cpp/container/list}}, + title = {std::list}, + howpublished= {\url{https://en.cppreference.com/w/cpp/container/list}}, } +@article{Blache19, + author = {Gunter Blache}, + title = {Handling Index-out-of-bounds in safety-critical embedded {C} code using model-based development}, + journal = {Software \& Systems Modeling}, + volume = 18, + year = 2019, + pages = {1795-1805}, +} + +@article{Oorschot23, + author = {van Oorschot, Paul C.}, + journal = {IEEE Security \& Privacy}, + title = {Memory Errors and Memory Safety: {C} as a Case Study}, + year = 2023, + volume = 21, + number = 2, + pages = {70-76}, +} + +@InProceedings{Ruef19, + author = {Andrew Ruef and Leonidas Lampropoulos and Ian Sweet and David Tarditi and Michael Hicks}, + title = {Achieving Safety Incrementally with {Checked C}}, + editor = {Flemming Nielson and David Sands}, + booktitle = {Principles of Security and Trust}, + publisher = {Springer International Publishing}, + address = {Cham}, + year = {2019}, + pages = {76-98}, +} + Index: doc/theses/mike_brooks_MMath/uw-ethesis.tex =================================================================== --- doc/theses/mike_brooks_MMath/uw-ethesis.tex (revision 0fa0201ddb94edca6686ec4a60eaa061cb4d64b3) +++ doc/theses/mike_brooks_MMath/uw-ethesis.tex (revision 5546eee4176e12f525c30034b085e9e000cdba20) @@ -93,4 +93,6 @@ \usepackage{algorithm} \usepackage{algpseudocode} + +\usepackage{pbox} % Hyperlinks make it very easy to navigate an electronic document. @@ -127,4 +129,5 @@ urlcolor=black }}{} % end of ifthenelse (no else) +\urlstyle{sf} %\usepackage[automake,toc,abbreviations]{glossaries-extra} % Exception to the rule of hyperref being the last add-on package