Ignore:
Timestamp:
Nov 23, 2024, 8:28:37 PM (11 months ago)
Author:
JiadaL <j82liang@…>
Branches:
master
Children:
956b389
Parents:
b006c51e (diff), de7b7a5 (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.
Message:

Merge branch 'master' of plg.uwaterloo.ca:software/cfa/cfa-cc

File:
1 edited

Legend:

Unmodified
Added
Removed

  • doc/theses/mike_brooks_MMath/array.tex

    rb006c51e r10a9479d  
    22\label{c:Array}
    33
     4Arrays in C are possibly the single most misunderstood and incorrectly used feature in the language, resulting in the largest proportion of runtime errors and security violations.
     5This chapter describes the new \CFA language and library features that introduce a length-checked array type, @array@, to the \CFA standard library~\cite{Cforall}.
     6
     7Offering the @array@ type, as a distinct alternative to the C array, is consistent with \CFA's goal of backwards compatibility, \ie virtually all existing C (@gcc@) programs can be compiled by \CFA with only a small number of changes, similar to \CC (@g++@).
     8However, a few compatibility-breaking changes to the behaviour of the C array are necessary, both as an implementation convenience and to fix C's lax treatment of arrays.
     9Hence, the @array@ type is an opportunity to start from a clean slate and show a cohesive selection of features, making it unnecessary to deal with every inherited complexity of the C array.
     10
    411
    512\section{Introduction}
    613\label{s:ArrayIntro}
    714
    8 Arrays in C are possibly the single most misunderstood and incorrectly used feature in the language, resulting in the largest proportion of runtime errors and security violations.
    9 This chapter describes the new \CFA language and library features that introduce a length-checked array type to the \CFA standard library~\cite{Cforall}.
    10 
    11 Specifically, a new \CFA array is declared by instantiating the generic @array@ type,
    12 much like instantiating any other standard-library generic type (such as @dlist@),
     15The new \CFA array is declared by instantiating the generic @array@ type,
     16much like instantiating any other standard-library generic type (such as \CC @vector@),
    1317though using a new style of generic parameter.
    1418\begin{cfa}
    … …  
    1620\end{cfa}
    1721Here, the arguments to the @array@ type are @float@ (element type) and @99@ (length).
    18 When this type is used as a function parameter, the type-system requires that a call's argument matches, down to the length.
     22When this type is used as a function parameter, the type-system requires that a call's argument is a perfect match.
    1923\begin{cfa}
    2024void f( @array( float, 42 )@ & p ) {}   $\C{// p accepts 42 floats}$
    21 f( x );                                                                 $\C{// statically rejected: types are different, 99 != 42}$
     25f( x );                                                                 $\C{// statically rejected: type lengths are different, 99 != 42}$
    2226
    2327test2.cfa:3:1 error: Invalid application of existing declaration(s) in expression.
    … …  
    2529\end{cfa}
    2630Here, the function @f@'s parameter @p@ is declared with length 42.
    27 The call @f( x )@, with the argument being the previously-declared object, is invalid, because the @array@ lengths @99@ and @42@ do not match.
    28 
    29 A function declaration can be polymorphic over these @array@ arguments by using the @forall@ declaration prefix.
    30 This function @g@'s takes arbitrary type parameter @T@ (familiar) and \emph{dimension parameter} @N@ (new).
    31 A dimension paramter represents a to-be-determined count of elements, managed by the type system.
     31However, the call @f( x )@ is invalid, because @x@'s length is @99@, which does not match @42@.
     32
     33A function declaration can be polymorphic over these @array@ arguments by using the \CFA @forall@ declaration prefix.
    3234\begin{cfa}
    3335forall( T, @[N]@ )
    … …  
    4042Cforall Runtime error: subscript 1000 exceeds dimension range [0,99) $for$ array 0x555555558020.
    4143\end{cfa}
     44Function @g@ takes an arbitrary type parameter @T@ and a \emph{dimension parameter} @N@.
     45A dimension parameter represents a to-be-determined count of elements, managed by the type system.
    4246The call @g( x, 0 )@ is valid because @g@ accepts any length of array, where the type system infers @float@ for @T@ and length @99@ for @N@.
    43 Inferring values for @T@ and @N@ is implicit, without programmer involvement.
     47Inferring values for @T@ and @N@ is implicit.
    4448Furthermore, in this case, the runtime subscript @x[0]@ (parameter @i@ being @0@) in @g@ is valid because 0 is in the dimension range $[0,99)$ of argument @x@.
    45 The call @g( x, 1000 )@ is also accepted through compile time;
     49However, the call @g( x, 1000 )@ is also accepted through compile time;
    4650however, this case's subscript, @x[1000]@, generates an error, because @1000@ is outside the dimension range $[0,99)$ of argument @x@.
     51In general, the @forall( ..., [N] )@ participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and within a function.
     52The syntactic form is chosen to parallel other @forall@ forms:
     53\begin{cfa}
     54forall( @[N]@ ) ...     $\C[1.5in]{// dimension}$
     55forall( T ) ...         $\C{// value datatype (formerly, "otype")}$
     56forall( T & ) ...       $\C{// opaque datatype (formerly, "dtype")}\CRT$
     57\end{cfa}
     58% The notation @array(thing, N)@ is a single-dimensional case, giving a generic type instance.
    4759
    4860The generic @array@ type is comparable to the C array type, which \CFA inherits from C.
    4961Their runtime characteristics are often identical, and some features are available in both.
    50 For example, assume a caller instantiates @N@ with 42 (discussion about how to follow) in:
     62For example, assume a caller has an argument that instantiates @N@ with 42.
    5163\begin{cfa}
    5264forall( [N] )
    53 void declDemo() {
     65void declDemo( ... ) {
    5466        float x1[N];                                            $\C{// built-in type ("C array")}$
    5567        array(float, N) x2;                                     $\C{// type from library}$
    … …  
    5971The two variables have identical size and layout; they both encapsulate 42-float stack allocations, with no additional ``bookkeeping'' allocations or headers.
    6072Providing this explicit generic approach requires a significant extension to the \CFA type system to support a full-feature, safe, efficient (space and time) array-type, which forms the foundation for more complex array forms in \CFA.
    61 
    62 Admittedly, the @array@ library type (type for @x2@) is syntactically different from its C counterpart.
    63 A future goal (TODO xref) is to provide the new features upon a built-in type whose syntax approaches C's (declaration style of @x1@).
     73In all following discussion, ``C array'' means the types like that of @x@ and ``\CFA array'' means the standard-library @array@ type (instantiations), like the type of @x2@.
     74
     75Admittedly, the @array@ library type for @x2@ is syntactically different from its C counterpart.
     76A future goal (TODO xref) is to provide the new @array@ features with syntax approaching C's (declaration style of @x1@).
    6477Then, the library @array@ type could be removed, giving \CFA a largely uniform array type.
    65 At present, the C-syntax array gets partial support for the new features, so the generic @array@ is used exclusively when introducing features;
     78At present, the C-syntax @array@ is only partially supported, so the generic @array@ is used exclusively in the thesis;
    6679feature support and C compatibility are revisited in Section ? TODO.
    67 
    68 Offering the @array@ type, as a distinct alternative to the C array, is consistent with \CFA's goal of backwards compatibility, \ie virtually all existing C (@gcc@) programs can be compiled by \CFA with only a small number of changes, similar to \CC (@g++@).
    69 However, a few compatibility-breaking changes to the behaviour of the C array are necessary, both as an implementation convenience and to fix C's lax treatment of arrays.
    70 Hence, the @array@ type is an opportunity to start from a clean slate and show a cohesive selection of features, making it unnecessary to deal with every inherited complexity of the C array.
    71 
    72 In all discussion following, ``C array'' means the types like that of @x@ and ``\CFA array'' means the standard-library @array@ type (instantiations), like the type of @x2@.
    7380
    7481My contributions in this chapter are:
    … …  
    8390
    8491
    85 \section{Definitions and design considerations}
    86 
    87 
    88 \subsection{Dependent typing}
    89 
    90 
    91 
    92 General dependent typing allows the type system to encode arbitrary predicates (e.g. behavioural specifications for functions),
     92\section{Dependent typing}
     93
     94General dependent typing allows the type system to encode arbitrary predicates (\eg behavioural specifications for functions),
    9395which is an anti-goal for my work.
    9496Firstly, this application is strongly associated with pure functional languages,
    … …  
    101103
    102104
    103 
    104105\section{Features added}
    105106
    … …  
    109110By declaring type variables at the front of object declarations, an array dimension is lexically referenceable where it is needed.
    110111For example, a declaration can share one length, @N@, among a pair of parameters and the return,
    111 meaning that it requires both input arrays to be of the same length, and guarantees that the result with be of that length as well.
     112meaning that it requires both input arrays to be of the same length, and guarantees that the result is of that length as well.
    112113\lstinput{10-17}{hello-array.cfa}
    113 This function @f@ does a pointwise comparison of its two input arrays, checking if each pair of numbers is within half a percent of each other, returning the answers in a newly allocated @bool@ array.
    114 The dynamic allocation of the @ret@ array by preexisting @alloc@ uses the parameterized dimension information implicitly within its @sizeof@ determination, and casts the return type.
    115 Note that alloc only sees one whole type for its @T@ (which is @f@'s @array(bool, N)@); this type's size is a computation based on @N@.
    116 \begin{cfa}
    117 // simplification
    118 static inline forall( T & | sized(T) )
     114Function @f@ does a pointwise comparison of its two input arrays, checking if each pair of numbers is within half a percent of each other, returning the answers in a newly allocated @bool@ array.
     115The dynamic allocation of the @ret@ array, by the library @alloc@ function,
     116\begin{cfa}
     117forall( T & | sized(T) )
    119118T * alloc() {
    120         return (T *)malloc( sizeof(T) );
    121 }
    122 \end{cfa}
    123 This example illustrates how the new @array@ type plugs into existing \CFA behaviour by implementing necessary @sized@ assertions needed by other types.
    124 (@sized@ implies a concrete \vs abstract type with a runtime-available size, exposed as @sizeof@.)
     119        return @(T *)@malloc( @sizeof(T)@ );
     120}
     121\end{cfa}
     122uses the parameterized dimension information implicitly within its @sizeof@ determination, and casts the return type.
     123Note that @alloc@ only sees one whole type for its @T@ (which is @f@'s @array(bool, N)@); this type's size is a computation based on @N@.
     124This example illustrates how the new @array@ type plugs into existing \CFA behaviour by implementing necessary \emph{sized} assertions needed by other types.
     125(\emph{sized} implies a concrete \vs abstract type with a runtime-available size, exposed as @sizeof@.)
    125126As a result, there is significant programming safety by making the size accessible and implicit, compared with C's @calloc@ and non-array supporting @memalign@, which take an explicit length parameter not managed by the type system.
    126127
    … …  
    142143The result is a significant improvement in safety and usability.
    143144
    144 In general, the @forall( ..., [N] )@ participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and within a function.
    145 The syntactic form is chosen to parallel other @forall@ forms:
    146 \begin{cfa}
    147 forall( @[N]@ ) ...     $\C[1.5in]{// dimension}$
    148 forall( T & ) ...       $\C{// opaque datatype (formerly, "dtype")}$
    149 forall( T ) ...         $\C{// value datatype (formerly, "otype")}\CRT$
    150 \end{cfa}
    151 % The notation @array(thing, N)@ is a single-dimensional case, giving a generic type instance.
    152145In summary:
    153146\begin{itemize}
    … …  
    168161% agreed, though already said
    169162\item
    170 \CC does not allow a template function to be nested, while \CFA lests its polymorphic functions to be nested.
     163\CC does not allow a template function to be nested, while \CFA lets its polymorphic functions to be nested.
    171164% why is this important?
    172165\item
    … …  
    227220\end{cfa}
    228221\end{tabular}
    229 \caption{\lstinline{N}-style paramters, for \CC template \vs \CFA generic type }
     222\caption{\lstinline{N}-style parameters, for \CC template \vs \CFA generic type }
    230223\label{f:TemplateVsGenericType}
    231224\end{figure}
    232225
    233226Just as the first example in \VRef[Section]{s:ArrayIntro} shows a compile-time rejection of a length mismatch,
    234 so are length mismatches stopped when they invlove dimension parameters.
     227so are length mismatches stopped when they involve dimension parameters.
    235228While \VRef[Figure]{f:fHarness} shows successfully calling a function @f@ expecting two arrays of the same length,
    236229\begin{cfa}
    237230array( bool, N ) & f( array( float, N ) &, array( float, N ) & );
    238231\end{cfa}
    239 a static rejection occurs when attempting to call @f@ with arrays of potentially differing lengths.
     232a static rejection occurs when attempting to call @f@ with arrays of differing lengths.
    240233\lstinput[tabsize=1]{70-74}{hello-array.cfa}
    241234When the argument lengths themselves are statically unknown,
    … …  
    252245Orthogonally, the \CFA array type works within generic \emph{types}, \ie @forall@-on-@struct@.
    253246The same argument safety and the associated implicit communication of array length occurs.
    254 Preexisting \CFA allowed aggregate types to be generalized with type parameters, enabling parameterizing for element types.
     247Preexisting \CFA allowed aggregate types to be generalized with type parameters, enabling parameterizing of element types.
    255248Now, \CFA also allows parameterizing them by length.
    256249Doing so gives a refinement of C's ``flexible array member'' pattern[TODO: cite ARM 6.7.2.1 pp18]\cite{arr:gnu-flex-mbr}.
    … …  
    259252This flexibility, in turn, allows for multiple array members.
    260253\lstinput{10-15}{hello-accordion.cfa}
    261 This structure's layout has the starting offset of @studentIds@ varying according to the generic parameter @C@, and the offset of @preferences@ varying according to both generic parameters.
    262 
    263 The school example has the data structure capturing many students' course-preference forms.
    264 It has course- and student-level metadata (their respective display names) and a position-based preferecens' matrix.
    265 The input files in \VRef[Figure]{f:checkHarness} give example data.
    266 
    267 When a function operates on a @School@ structure, the type system handles its memory layout transparently.
    268 \lstinput{30-37}{hello-accordion.cfa}
    269 In the running example, this @getPref@ function answers,
    270 for the student at position @sIx@, what is the position of its @pref@\textsuperscript{th}-favoured class?
    271 
    272 \VRef[Figure]{f:checkHarness} shows the @School@ harness and results with different array sizes.
    273 This example program prints the courses in each student's preferred order, all using the looked-up display names.
    274 Note the declaration of the @school@ variable.
     254The structure has course- and student-level metatdata (their respective field names) and a position-based preferences' matrix.
     255Its layout has the starting offset of @studentIds@ varying according to the generic parameter @C@, and the offset of @preferences@ varying according to both generic parameters.
     256
     257\VRef[Figure]{f:checkHarness} shows a program main using @School@ and results with different array sizes.
     258The @school@ variable holds many students' course-preference forms.
    275259It is on the stack and its initialization does not use any casting or size arithmetic.
    276260Both of these points are impossible with a C flexible array member.
    … …  
    280264\end{cfa}
    281265This ability to avoid casting and size arithmetic improves safety and usability over C flexible array members.
    282 
     266Finally, inputs and outputs are given at the bottom for different sized schools.
     267The example program prints the courses in each student's preferred order, all using the looked-up display names.
    283268
    284269\begin{figure}
    285 % super hack to get this to line up
    286 \begin{tabular}{@{}ll@{\hspace{25pt}}l@{}}
    287 \begin{tabular}{@{}p{3.25in}@{}}
     270\begin{cquote}
    288271\lstinput{50-55}{hello-accordion.cfa}
    289 \vspace*{-3pt}
    290272\lstinput{90-98}{hello-accordion.cfa}
    291 \end{tabular}
    292 &
    293 \raisebox{0.32\totalheight}{%
    294 }%
    295 &
    296 \end{tabular}
    297 
    298 TODO: Get Peter's layout help
    299 
    300 \$ cat school1
    301 
     273\ \\
     274@$ cat school1@
    302275\lstinput{}{school1}
    303276
    304 \$ ./a.out < school1
    305 
     277@$ ./a.out < school1@
    306278\lstinput{}{school1.out}
    307279
    308 \$ cat school2
    309 
     280@$ cat school2@
    310281\lstinput{}{school2}
    311282
    312 \$ ./a.out < school2
    313 
     283@$ ./a.out < school2@
    314284\lstinput{}{school2.out}
     285\end{cquote}
    315286
    316287\caption{\lstinline{School} harness, input and output}
    317288\label{f:checkHarness}
    318289\end{figure}
     290
     291When a function operates on a @School@ structure, the type system handles its memory layout transparently.
     292\lstinput{30-37}{hello-accordion.cfa}
     293In the example, this @getPref@ function answers, for the student at position @is@, what is the position of its @pref@\textsuperscript{th}-favoured class?
    319294
    320295
    … …  
    333308But simplifications close enough for the present discussion are:
    334309\begin{cfa}
    335         forall( [N] )
    336         struct array_1d_float {
    337                 float items[N];
    338         };
    339         forall( T, [N] )
    340         struct array_1d {
    341                 T items[N];
    342         };
    343 \end{cfa}
    344 This structure pattern, plus a subscript operator, is all that @array@ provides.
     310forall( [N] )
     311struct array_1d_float {
     312        float items[N];
     313};
     314forall( T, [N] )
     315struct array_1d_T {
     316        T items[N];
     317};
     318\end{cfa}
     319These two structure patterns, plus a subscript operator, is all that @array@ provides.
    345320
    346321My main work is letting a programmer define
    347 such a structre (one whose type is parameterized by @[N]@)
     322such a structure (one whose type is parameterized by @[N]@)
    348323and functions that operate on it (these being similarly parameterized).
    349324
    … …  
    351326\begin{itemize}
    352327\item
    353         The resolver, providing values for a used declaration's type-system variables,
     328        Resolver provided values for a used declaration's type-system variables,
    354329        gathered from type information in scope at the usage site.
    355 
    356330\item
    357331        The box pass, encoding information about type parameters
    358332        into ``extra'' regular parameters/arguments on declarations and calls.
    359333        Notably, it conveys the size of a type @foo@ as a @__sizeof_foo@ parameter,
    360         and rewrites the @sizeof(foo)@ expression as @__sizeof_foo@, i.e. a use of the parameter.
     334        and rewrites the @sizeof(foo)@ expression as @__sizeof_foo@, \ie a use of the parameter.
    361335\end{itemize}
    362336
    … …  
    364338This work is detailed in \VRef[Section]{s:ArrayTypingC}.
    365339However, the resolution--boxing scheme, in its preexisting state, was already equipped to work on (desugared) dimension parameters.
    366 The discussion following explains the desugaring and how correct lowered code results.
    367 
    368 An even simpler structure, and a toy function on it, demonstrate what's needed for the encoding.
    369 \begin{cfa}
    370         forall( [@N@] ) { // [1]
    371                 struct thing {};
    372                 void f( thing(@N@) ) { sout | @N@; } // [2], [3]
    373         }
    374         int main() {
    375                 thing( @10@ ) x;  f(x);  // prints 10, [4]
    376                 thing( 100 ) y;  f(y);  // prints 100
    377                 return 0;
    378         }
     340The following discussion explains the desugaring and how correctly lowered code results.
     341
     342A simpler structure, and a toy function on it, demonstrate what is needed for the encoding.
     343\begin{cfa}
     344forall( [@N@] ) { $\C{// [1]}$
     345        struct thing {};
     346        void f( thing(@N@) ) { sout | @N@; } $\C{// [2], [3]}$
     347}
     348int main() {
     349        thing( @10@ ) x;  f( x );  $\C{// prints 10, [4]}$
     350        thing( 100 ) y;  f( y );  $\C{// prints 100}$
     351        return 0;
     352}
    379353\end{cfa}
    380354This example has:
    … …  
    389363        A value like 10 being used as an argument to the parameter @N@.
    390364\end{enumerate}
    391 The chosen solution being to encode the value @N@ \emph{as a type}, items 1 and 2 are immediately available for free.
     365The chosen solution is to encode the value @N@ \emph{as a type}, so items 1 and 2 are immediately available for free.
    392366Item 3 needs a way to recover the encoded value from a (valid) type (and to reject invalid types occurring here).
    393367Item 4 needs a way to produce a type that encodes the given value.
    … …  
    400374\item
    401375        Given a dimension expression $e$, produce type @char[@$e$@]@ to represent it.
    402         If $e$ evaluates to $n$ then the endoded type has size $n$.
     376        If $e$ evaluates to $n$ then the encoded type has size $n$.
    403377\item
    404378        Given a type $T$ (produced by these rules), recover the value that it represents with the expression @sizeof(@$T$@)@.
    … …  
    410384The running example is lowered to:
    411385\begin{cfa}
    412         forall( @N*@ ) { // [1]
    413                 struct thing {};
    414                 void f( thing(@N@) ) { sout | @sizeof(N)@; } // [2], [3]
    415         }
    416         int main() {
    417                 thing( char[@10@] ) x;  f(x);  // prints 10, [4]
    418                 thing( char[100] ) y;  f(y);  // prints 100
    419                 return 0;
    420         }
     386forall( @N *@ ) { $\C{// [1]}$
     387        struct thing {};
     388        void f( thing(@N@) ) { sout | @sizeof(N)@; } $\C{// [2], [3]}$
     389}
     390int main() {
     391        thing( char[@10@] ) x;  f( x );  $\C{// prints 10, [4]}$
     392        thing( char[100] ) y;  f( y );  $\C{// prints 100}$
     393        return 0;
     394}
    421395\end{cfa}
    422396Observe:
    … …  
    430404        The @sout...@ expression (being an application of the @?|?@ operator) has a second argument that is an ordinary expression.
    431405\item
    432         The type of variable @x@ is another @thing(-)@ type;  the argument to the generic @thing@ is a type (array type).
     406        The type of variable @x@ is another @thing(-)@ type; the argument to the generic @thing@ is a type (array type of bytes, @char@).
    433407\end{enumerate}
    434408
    435409From this point, preexisting \CFA compilation takes over lowering it the rest of the way to C.
    436 Inspecting the result shows what the above translation achieves.
    437 A form that shows only the relevant changes of the box pass (as informed by the resolver), leaving the rest unadulterated, is:
    438 \begin{cfa}
    439         // [1]
    440         void f( size_t __sizeof_N, @void *@ ) { sout | @__sizeof_N@; } // [2], [3]
    441         int main() {
    442                 struct __conc_thing_10 {} x;  f(@10@, &x);  // prints 10, [4]
    443                 struct __conc_thing_100 {} y;  f(@100@, &y);  // prints 100
    444                 return 0;
    445         }
     410Here the result shows only the relevant changes of the box pass (as informed by the resolver), leaving the rest unadulterated:
     411\begin{cfa}
     412// [1]
     413void f( size_t __sizeof_N, @void *@ ) { sout | @__sizeof_N@; } $\C{// [2], [3]}$
     414int main() {
     415        struct __conc_thing_10 {} x;  f( @10@, &x );  $\C{// prints 10, [4]}$
     416        struct __conc_thing_100 {} y;  f( @100@, &y );  $\C{// prints 100}$
     417        return 0;
     418}
    446419\end{cfa}
    447420Observe:
    … …  
    452425        The type @thing(N)@ is (replaced by @void *@, but thereby effectively) gone.
    453426\item
    454         The @sout...@ expression (being an application of the @?|?@ operator) has a second argument that is a regular variable (parameter) usage.
     427        The @sout...@ expression (being an application of the @?|?@ operator) has a regular variable (parameter) usage for its second argument.
    455428\item
    456429        Information about the particular @thing@ instantiation (value 10) has moved, from the type, to a regular function-call argument.
    457430\end{enumerate}
    458 At the end of the desugaring and downstream processing, the original C idiom of ``pass both a pointer and a length parameter'' has been reconstructed.
    459 In the programmer-written form, only the thing is passed.
     431At the end of the desugaring and downstream processing, the original C idiom of ``pass both a length parameter and a pointer'' has been reconstructed.
     432In the programmer-written form, only the @thing@ is passed.
    460433The compiler's action produces the more complex form, which if handwritten, would be error-prone.
    461434
    462 Back at the very front end, the parsing changes, AST schema extensions, and validation rules for enabling the sugared user input are:
     435Back at the compiler front end, the parsing changes AST schema extensions and validation rules for enabling the sugared user input.
    463436\begin{itemize}
    464437\item
    … …  
    467440        Have the new brand of type-variable, \emph{Dimension}, in the AST form of a type-variable, to represent one parsed from @[-]@.
    468441\item
    469         Allow a type variable to occur in expression position.  Validate (after parsing) that only dimension-branded type variables are used here.
     442        Allow a type variable to occur in an expression.  Validate (after parsing) that only dimension-branded type variables are used here.
    470443\item
    471444        Allow an expression to occur in type-argument position.  Brand the resulting type argument as a dimension.
    … …  
    473446        Validate (after parsing), on a generic-type usage, \eg the type part of the declaration
    474447        \begin{cfa}
    475                 @array_1d( foo, bar ) x;@
     448        array_1d( foo, bar ) x;
    476449        \end{cfa}
     450        \vspace*{-10pt}
    477451        that the brands on the generic arguments match the brands of the declared type variables.
    478452        Here, that @foo@ is a type and @bar@ is a dimension.
    … …  
    488462from one party who knows it, to another who is willing to work with any given length.
    489463For scenarios where the concern is a mishandled length,
    490 the interaction is between two parties who both claim to know (something about) it.
    491 Such a scenario occurs in this pure C fragment, wich today's C compilers accept:
    492 \begin{cfa}
    493         int n = @42@;
    494         float x[n];
    495         float (*xp)[@999@] = &x;
    496         (*xp)[@500@];  // in "bound"?
    497 \end{cfa}
    498 
     464the interaction is between two parties who both claim to know something about it.
     465Such a scenario occurs in this pure C fragment, which today's C compilers accept:
     466\begin{cfa}
     467int n = @42@;
     468float x[n];
     469float (*xp)[@999@] = &x;
     470(*xp)[@500@]; $\C{// in "bound"?}$
     471\end{cfa}
    499472Here, the array @x@ has length 42, while a pointer to it (@xp@) claims length 999.
    500473So, while the subscript of @xp@ at position 500 is out of bound of its referent @x@,
    … …  
    505478The \CFA new-array rejects the analogous case:
    506479\begin{cfa}
    507         int n = @42@;
    508         array(float, n) x;
    509         array(float, 999) * xp = x; // static rejection here
    510         (*xp)[@500@]; // runtime check vs len 999
    511 \end{cfa}
    512 
    513 % TODO: kill the vertical whitespace around these lists
    514 % nothing from https://stackoverflow.com/questions/1061112/eliminate-space-before-beginitemize is working
    515 
    516 The way the \CFA array is implemented,
    517 the type analysis of this \CFA case reduces to a case similar to the earlier C version.
     480int n = @42@;
     481array(float, n) x;
     482array(float, 999) * xp = x; $\C{// static rejection here}$
     483(*xp)[@500@]; $\C{// runtime check vs len 999}$
     484\end{cfa}
     485The way the \CFA array is implemented, the type analysis of this case reduces to a case similar to the earlier C version.
    518486The \CFA compiler's compatibility analysis proceeds as:
    519 \begin{itemize}[noitemsep,partopsep=-\parskip,parsep=0pt,leftmargin=4em]
     487\begin{itemize}[parsep=0pt]
    520488\item
    521489        Is @array(float, 999)@ type-compatible with @array(float, n)@?
    522490\item
    523         Is @arrayX(float, char[999])@ type-compatible with @arrayX(float, char[n])@?
    524         \footnote{Here, \lstinline{arrayX} represents the type that results
     491        Is @arrayX(float, char[999])@ type-compatible with @arrayX(float, char[n])@?\footnote{
     492                Here, \lstinline{arrayX} represents the type that results
    525493                from desugaring the \lstinline{array} type
    526494                into a type whose generic parameters are all types.
    … …  
    531499        Is @char[999]@ type-compatible with @char[n]@?
    532500\end{itemize}
    533 
    534 I chose to achieve the necessary rejection of the \CFA case
    535 by adding a rejection of the corresponding C case.
    536 
    537 This decision is not backward compatible.
     501To achieve the necessary \CFA rejections meant rejecting the corresponding C case, which is not backward compatible.
    538502There are two complementary mitigations for this incompatibility.
    539503
    … …  
    542506This situation might arise if @n@ were known to be 999,
    543507rather than 42, as in the introductory examples.
    544 The programmer can add a cast, as in:
    545 \begin{cfa}
    546         xp = ( float (*)[999] ) & x;
    547 \end{cfa}
    548 This addition causes \CFA to accept, beacause now, the programmer has accepted blame.
     508The programmer can add a cast in the \CFA code.
     509\begin{cfa}
     510xp = @(float (*)[999])@ &x;
     511\end{cfa}
     512This addition causes \CFA to accept, because now, the programmer has accepted blame.
    549513This addition is benign in plain C, because the cast is valid, just unnecessary there.
    550514Moreover, the addition can even be seen as appropriate ``eye candy,''
    … …  
    556520Second, the incompatibility only affects types like pointer-to-array,
    557521which are are infrequently used in C.
    558 The more common C idiom for aliasing an array is to use the pointer-to-first-element type,
    559 which does not participate in the \CFA array's length checking.
    560 \footnote{Notably, the desugaring of the \lstinline{array@} type,
    561         avoids letting any \lstinline{-[-]} type decay,
    562         in order to preserve the length information that powers runtime bound checking.}
    563 Therefore, the frequency of needing to upgrade wild C code (as discussed in the first mitigation)
     522The more common C idiom for aliasing an array is to use a pointer-to-first-element type,
     523which does not participate in the \CFA array's length checking.\footnote{
     524        Notably, the desugaring of the \lstinline{array} type avoids letting any \lstinline{-[-]} type decay,
     525        in order to preserve the length information that powers runtime bound-checking.}
     526Therefore, the frequency of needing to upgrade legacy C code (as discussed in the first mitigation)
    564527is anticipated to be low.
    565528
    566529Because the incompatibility represents a low cost to a \CFA onboarding effort
    567530(with a plausible side benefit of linting the original code for a missing annotation),
    568 I elected not to add special measures to retain the compatibility.
     531no special measures were added to retain the compatibility.
    569532It would be possible to flag occurrences of @-[-]@ types that come from @array@ desugaring,
    570533treating those with stricter \CFA rules, while treating others with classic C rules.
    … …  
    573536
    574537Having allowed that both the initial C example's check
    575 \begin{itemize}[noitemsep,partopsep=-\parskip,parsep=0pt,leftmargin=4em]
     538\begin{itemize}
    576539        \item
    577540                Is @float[999]@ type-compatible with @float[n]@?
    578541\end{itemize}
    579 and the second \CFA exmple's induced check
    580 \begin{itemize}[noitemsep,partopsep=-\parskip,parsep=0pt,leftmargin=4em]
     542and the second \CFA example's induced check
     543\begin{itemize}
    581544        \item
    582545                Is @char[999]@ type-compatible with @char[n]@?
    … …  
    587550To implement the new \CFA rules, I took the syntactic recursion a step further, obtaining,
    588551in both cases:
    589 \begin{itemize}[noitemsep,partopsep=-\parskip,parsep=0pt,leftmargin=4em]
     552\begin{itemize}
    590553        \item
    591                 Is @999@ TBD-compatible with @n@?
     554                Is @999@ compatible with @n@?
    592555\end{itemize}
    593 This compatibility question applies to a pair of expressions, where the earlier ones were to types.
     556This compatibility question applies to a pair of expressions, where the earlier implementation were to types.
    594557Such an expression-compatibility question is a new addition to the \CFA compiler.
    595 These questions only arise in the context of dimension expressions on (C) array types.
     558Note, these questions only arise in the context of dimension expressions on (C) array types.
    596559
    597560TODO: ensure these compiler implementation matters are treated under \CFA compiler background:
    … …  
    600563GenPoly.
    601564
    602 The relevant technical component of the \CFA compiler is,
    603 within the type resolver, the type unification procedure.
     565The relevant technical component of the \CFA compiler is the type unification procedure within the type resolver.
    604566I added rules for continuing this unification into expressions that occur within types.
    605567It is still fundamentally doing \emph{type} unification
    … …  
    607569and not participating in binding any variables that stand in for expression fragments
    608570(for there is no such sort of variable in \CFA's analysis.)
    609 
    610571An unfortunate fact about the \CFA compiler's preexisting implementation is that
    611572type unification suffers from two forms of duplication.
    … …  
    613574The first duplication has (many of) the unification rules stated twice.
    614575As a result, my additions for dimension expressions are stated twice.
    615 The extra statement of the rules occurs in the GenPoly module,
     576The extra statement of the rules occurs in the @GenPoly@ module,
    616577where concrete types like @array(int, 5)@\footnote{
    617578        Again, the presentation is simplified
    618         by leaving the \lstinline{array} macro unexpanded}
     579        by leaving the \lstinline{array} macro unexpanded.}
    619580are lowered into corresponding C types @struct __conc_array_1234@ (the suffix being a generated index).
    620 In this case, the struct's definition gives fields that hardcode the argument values of @float@ and @5@.
    621 The next time an @array(-,-)@ concrete instance is encountered,
    622 is the previous @struct __conc_array_1234@ suitable for it?
    623 Yes, for another occurrance of @array(int, 5)@;
     581In this case, the struct's definition contains fields that hardcode the argument values of @float@ and @5@.
     582The next time an @array(-,-)@ concrete instance is encountered, it checks if the previous @struct __conc_array_1234@ is suitable for it.
     583Yes, for another occurrence of @array(int, 5)@;
    624584no, for either @array(rational(int), 5)@ or @array(int, 42)@.
    625585By the last example, this phase must ``reject''
    … …  
    630590In the program
    631591\begin{cfa}
    632         void f( double );
    633         forall( T & ) void f( T & );
    634         void g( int n ) {
    635                 array( float, n + 1 ) x;
    636                 f(x);
    637         }
    638 \end{cfa}
    639 when resolving the function call, the first unification stage
    640 compares the types @T@, of the parameter, with @array( float, n + 1 )@, of the argument.
     592void @f@( double );
     593forall( T & ) void @f@( T & );
     594void g( int n ) {
     595        array( float, n + 1 ) x;
     596        f(x);   // overloaded
     597}
     598\end{cfa}
     599when resolving the function call, @g@, the first unification stage
     600compares the type @T@ of the parameter with @array( float, n + 1 )@, of the argument.
    641601TODO: finish.
    642602
    … …  
    647607        TODO: Deal with directionality, that I'm doing exact-match, no ``at least as long as,'' no subtyping.
    648608        Should it be an earlier scoping principle?  Feels like it should matter in more places than here.}
    649 So, a ``yes'' answer must represent a guarantee that both expressions will evaluate the
    650 same result, while a ``no'' can tolerate ``they might, but we're not sure,'
     609So, a ``yes'' answer must represent a guarantee that both expressions evaluate the
     610same result, while a ``no'' can tolerate ``they might, but we're not sure'',
    651611provided that practical recourses are available
    652 to let programmers express their better knowledge.
    653 The specific rule-set that I offer with the current release is, in fact, extremely conservative.
     612to let programmers express better knowledge.
     613The new rule-set in the current release is, in fact, extremely conservative.
    654614I chose to keep things simple,
    655 and allow real future needs do drive adding additional complexity,
    656 within the framework that I laid out.
     615and allow future needs to drive adding additional complexity, within the new framework.
    657616
    658617For starters, the original motivating example's rejection
    … …  
    662621Rather, the analysis assumes a variable's value can be anything,
    663622and so there can be no guarantee that its value is 999.
    664 So, a variable use and a literal can never match.
     623So, a variable and a literal can never match.
    665624
    666625Two occurrences of the same literal value are obviously a fine match.
    667 For two occurrences of the same varialbe, more information is needed.
     626For two occurrences of the same variable, more information is needed.
    668627For example, this one is fine
    669628\begin{cfa}
    670         void f( const int n ) {
    671                 float x[n];
    672                 float (*xp)[n] = x; // accept
    673         }
     629void f( const int n ) {
     630        float x[n];
     631        float (*xp)[n] = x;  // accept
     632}
    674633\end{cfa}
    675634while this one is not:
    676635\begin{cfa}
    677         void f() {
    678                 int n = 42;
    679                 float x[n];
    680                 n = 999;
    681                 float (*xp)[n] = x; // reject
    682         }
     636void f() {
     637        int n = 42;
     638        float x[n];
     639        n = 999;
     640        float (*xp)[n] = x;  // reject
     641}
    683642\end{cfa}
    684643Furthermore, the fact that the first example sees @n@ as @const@
    685 is not actually a sufficent basis.
     644is not actually sufficient.
    686645In this example, @f@'s length expression's declaration is as @const@ as it can be,
    687646yet its value still changes between the two invocations:
    688 \begin{cfa}
    689         // compile unit 1
    690         void g();
    691         void f( const int & const nr ) {
    692                 float x[nr];
    693                 g();
    694                 float (*xp)[nr] = x; // reject
    695         }
    696         // compile unit 2
    697         static int n = 42;
    698         void g() {
    699                 n = 99;
    700         }
    701         void f( const int & );
    702         int main () {
    703                 f(n);
    704                 return 0;
    705         }
    706 \end{cfa}
    707 The issue in this last case is,
    708 just because you aren't able to change something doesn't mean someone else can't.
    709 
    710 My rule set also respects a feature of the C tradition.
    711 In spite of the several limitations of the C rules
     647\begin{cquote}
     648\setlength{\tabcolsep}{15pt}
     649\begin{tabular}{@{}ll@{}}
     650\begin{cfa}
     651// compile unit 1
     652void g();
     653void f( const int & const nr ) {
     654        float x[nr];
     655        g();    // change n
     656        @float (*xp)[nr] = x;@   // reject
     657}
     658\end{cfa}
     659&
     660\begin{cfa}
     661// compile unit 2
     662static int n = 42;
     663void g() {
     664        n = 99;
     665}
     666
     667f( n );
     668\end{cfa}
     669\end{tabular}
     670\end{cquote}
     671The issue here is that knowledge needed to make a correct decision is hidden by separate compilation.
     672Even within a translation unit, static analysis might not be able to provide all the information.
     673
     674My rule set also respects a traditional C feature: In spite of the several limitations of the C rules
    712675accepting cases that produce different values, there are a few mismatches that C stops.
    713 C is quite precise when working with two static values:
    714 \begin{cfa}
    715         enum { fortytwo = 42 };
    716         float x[fortytwo];
    717         float (*xp1)[42] = &x; // accept
    718         float (*xp2)[999] = &x; // reject
     676C is quite precise when working with two static values.
     677\begin{cfa}
     678enum { fortytwo = 42 };
     679float x[fortytwo];
     680float (*xp1)[42] = &x;    // accept
     681float (*xp2)[999] = &x;  // reject
    719682\end{cfa}
    720683My \CFA rules agree with C's on these cases.
    721684
    722 My rules classify expressions into three groups:
     685In summary, the new rules classify expressions into three groups:
    723686\begin{description}
    724687\item[Statically Evaluable]
    725688        Expressions for which a specific value can be calculated (conservatively)
    726689        at compile-time.
    727         A preexisting \CFA compiler module defines which expressions qualify,
     690        A preexisting \CFA compiler module defines which literals, enumerators, and expressions qualify,
    728691        and evaluates them.
    729         Includes literals and enumeration values.
    730692\item[Dynamic but Stable]
    731         The value of a variable declared as @const@.
    732         Includes a @const@ parameter.
     693        The value of a variable declared as @const@, including a @const@ parameter.
    733694\item[Potentially Unstable]
    734695        The catch-all category.  Notable examples include:
    735         any function-call result (@float x[foo()];@),
    736         the particular function-call result that is a pointer dereference (@void f(const int * n) { float x[*n]; }@), and
     696        any function-call result, @float x[foo()];@,
     697        the particular function-call result that is a pointer dereference, @void f(const int * n)@ @{ float x[*n]; }@, and
    737698        any use of a reference-typed variable.
    738699\end{description}
    739 
    740 My \CFA rules are:
     700Within these groups, my \CFA rules are:
    741701\begin{itemize}
    742702\item
    … …  
    744704        Notably, this rule allows a literal to match with an enumeration value, based on the value.
    745705\item
    746         Accept a Dynamic but Stable pair, if both expressions are written out the same, e.g. refers to same variable declaration.
     706        Accept a Dynamic but Stable pair, if both expressions are written out the same, \eg refers to the same variable declaration.
    747707\item
    748708        Otherwise, reject.
    749         Notably, reject all pairs from the Potentially Unstable group.
    750         Notably, reject all pairs that cross groups.
     709        Notably, reject all pairs from the Potentially Unstable group and all pairs that cross groups.
    751710\end{itemize}
    752 
    753711The traditional C rules are:
    754712\begin{itemize}
    … …  
    759717\end{itemize}
    760718
    761 
    762 \newcommand{\falsealarm}{{\color{orange}\small{*}}}
    763 \newcommand{\allowmisuse}{{\color{red}\textbf{!}}}
    764 \newcommand{\cmark}{\ding{51}} % from pifont
    765 \newcommand{\xmark}{\ding{55}}
    766719\begin{figure}
     720        \newcommand{\falsealarm}{{\color{blue}\small{*}}}
     721        \newcommand{\allowmisuse}{{\color{red}\textbf{!}}}
     722        \newcommand{\cmark}{\ding{51}} % from pifont
     723        \newcommand{\xmark}{\ding{55}}
     724
    767725        \begin{tabular}{@{}l@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c}
    768726         & \multicolumn{2}{c}{\underline{Values Equal}}
    … …  
    778736        \end{tabular}
    779737
    780         \vspace{12pt}
    781         \noindent\textbf{Legend:}
    782         \begin{itemize}
     738        \medskip
     739        \noindent\textbf{Legend}
     740        \begin{itemize}[leftmargin=*]
    783741        \item
    784742                Each row gives the treatment of a test harness of the form
    785743                \begin{cfa}
    786                         float x[ expr1 ];
    787                         float (*xp)[ expr2 ] = &x;
     744                float x[ expr1 ];
     745                float (*xp)[ expr2 ] = &x;
    788746                \end{cfa}
    789                 where \lstinline{expr1} and \lstinline{expr2} are metavariables varying according to the row's Case.
     747                \vspace*{-10pt}
     748                where \lstinline{expr1} and \lstinline{expr2} are meta-variables varying according to the row's Case.
    790749                Each row's claim applies to other harnesses too, including,
    791750                \begin{itemize}
    792751                \item
    793                         calling a function with a paramter like \lstinline{x} and an argument of the \lstinline{xp} type,
     752                        calling a function with a parameter like \lstinline{x} and an argument of the \lstinline{xp} type,
    794753                \item
    795754                        assignment in place of initialization,
    … …  
    801760        \item
    802761                Each case's claim is symmetric (swapping \lstinline{expr1} with \lstinline{expr2} has no effect),
    803                 even though most test harnesses are asymetric.
     762                even though most test harnesses are asymmetric.
    804763        \item
    805764                The table treats symbolic identity (Same/Different on rows)
    806                 apart from value eqality (Equal/Unequal on columns).
     765                apart from value equality (Equal/Unequal on columns).
    807766                \begin{itemize}
    808767                \item
    … …  
    819778                while every Accept under Values Unequal is an allowed misuse (\allowmisuse).
    820779        \end{itemize}
    821         \caption{Case comparison for array type compatibility, given pairs of dimension expressions.
    822                 TODO: get Peter's LaTeX help on overall appearance, probably including column spacing/centering and bullet indentation.}
     780
     781        \caption{Case comparison for array type compatibility, given pairs of dimension expressions.}
    823782        \label{f:DimexprRuleCompare}
    824783\end{figure}
    … …  
    826785
    827786Figure~\ref{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
    828 It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafely.
    829 It also shows that C-incompatibilities only occur in cases that C treats unsafely.
     787It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafe.
     788It also shows that C-incompatibilities only occur in cases that C treats unsafe.
    830789
    831790
    … …  
    837796whose reuses are rejected by the blunt current-state rules:
    838797\begin{cfa}
    839         void f( int & nr, const int nv ) {
    840                 float x[nr];
    841                 float (*xp)[nr] = & x; // reject: nr varying (no references)
    842                 float y[nv + 1];
    843                 float (*yp)[nv + 1] = & y; // reject: ?+? unpredicable (no functions)
    844         }
     798void f( int & nr, const int nv ) {
     799        float x[nr];
     800        float (*xp)[nr] = &x;  // reject: nr varying (no references)
     801        float y[nv + 1];
     802        float (*yp)[nv + 1] = &y;   // reject: ?+? unpredictable (no functions)
     803}
    845804\end{cfa}
    846805Yet, both dimension expressions are reused safely.
    847 (The @nr@ reference is never written, not volatile
     806The @nr@ reference is never written, not volatile
    848807and control does not leave the function between the uses.
    849 The name @?+?@ resolves to a function that is quite predictable.)
    850 The programmer here can add the constant declarations:
    851 \begin{cfa}
    852         void f( int & nr, const int nv ) {
    853                 @const int nx@ = nr;
    854                 float x[nx];
    855                 float (*xp)[nx] = & x; // acept
    856                 @const int ny@ = nv + 1;
    857                 float y[ny];
    858                 float (*yp)[ny] = & y; // accept
    859         }
     808The name @?+?@ resolves to a function that is quite predictable.
     809Here, the programmer can add the constant declarations (cast does not work):
     810\begin{cfa}
     811void f( int & nr, const int nv ) {
     812        @const int nx@ = nr;
     813        float x[nx];
     814        float (*xp)[nx] = & x;   // accept
     815        @const int ny@ = nv + 1;
     816        float y[ny];
     817        float (*yp)[ny] = & y;  // accept
     818}
    860819\end{cfa}
    861820The result is the originally intended semantics,
    … …  
    863822
    864823The snapshotting trick is also used by the translation, though to achieve a different outcome.
    865 Rather obviously, every array must be subscriptable, even a bizzarre one:
    866 \begin{cfa}
    867         array( float, rand(10) ) x;
    868         x[0];  // 10% chance of bound-check failure
     824Rather obviously, every array must be subscriptable, even a bizarre one:
     825\begin{cfa}
     826array( float, rand(10) ) x;
     827x[0];  // 10% chance of bound-check failure
    869828\end{cfa}
    870829Less obvious is that the mechanism of subscripting is a function call,
    … …  
    874833Adjusting the example to make the function's use of length more explicit:
    875834\begin{cfa}
    876         forall ( T * )
    877         void f( T * x ) { sout | sizeof(*x); }
    878         float x[ rand(10) ];
    879         f( x );
     835forall ( T * )
     836void f( T * x ) { sout | sizeof(*x); }
     837float x[ rand(10) ];
     838f( x );
    880839\end{cfa}
    881840Considering that the partly translated function declaration is, loosely,
    882841\begin{cfa}
    883         void f( size_t __sizeof_T, void * x ) { sout | __sizeof_T; }
    884 \end{cfa}
    885 the translated call must not go like:
    886 \begin{cfa}
    887         float x[ rand(10) ];
    888         f( rand(10), &x );
    889 \end{cfa}
    890 Rather, its actual translation is like:
    891 \begin{cfa}
    892         size_t __dim_x = rand(10);
    893         float x[ __dim_x ];
    894         f( __dim_x, &x );
    895 \end{cfa}
    896 The occurrence of this dimension hoisting during translation was present in the preexisting \CFA compiler.
    897 But its cases were buggy, particularly with determining, ``Can hoisting be skipped here?''
    898 For skipping this hoisting is clearly desirable in some cases,
    899 not the least of which is when the programmer has already done so manually.
    900 My work includes getting these cases right, harmonized with the accept/reject criteria, and tested.
    901 
    902 
     842void f( size_t __sizeof_T, void * x ) { sout | __sizeof_T; }
     843\end{cfa}
     844the translation must call the dimension argument twice:
     845\begin{cfa}
     846float x[ rand(10) ];
     847f( rand(10), &x );
     848\end{cfa}
     849Rather, the translation is:
     850\begin{cfa}
     851size_t __dim_x = rand(10);
     852float x[ __dim_x ];
     853f( __dim_x, &x );
     854\end{cfa}
     855The occurrence of this dimension hoisting during translation was in the preexisting \CFA compiler.
     856But its cases were buggy, particularly with determining, ``Can hoisting the expression be skipped here?'', for skipping this hoisting is clearly desirable in some cases.
     857For example, when the programmer has already done so manually. \PAB{I don't know what this means.}
     858In the new implementation, these cases are correct, harmonized with the accept/reject criteria.
    903859
    904860TODO: Discuss the interaction of this dimension hoisting with the challenge of extra unification for cost calculation
    905861
    906862
    907 \section{Multidimensional Arrays}
    908 \label{toc:mdimpl}
    909 
    910 % TODO: introduce multidimensional array feature and approaches
    911 
    912 When working with arrays, \eg linear algebra, array dimensions are referred to as ``rows'' and ``columns'' for a matrix, adding ``planes'' for a cube.
    913 (There is little terminology for higher dimensional arrays.)
    914 For example, an acrostic poem\footnote{A type of poetry where the first, last or other letters in a line spell out a particular word or phrase in a vertical column.}
    915 can be treated as a grid of characters, where the rows are the text and the columns are the embedded keyword(s).
    916 Within a poem, there is the concept of a \newterm{slice}, \eg a row is a slice for the poem text, a column is a slice for a keyword.
    917 In general, the dimensioning and subscripting for multidimensional arrays has two syntactic forms: @m[r,c]@ or @m[r][c]@.
    918 
    919 Commonly, an array, matrix, or cube, is visualized (especially in mathematics) as a contiguous row, rectangle, or block.
    920 This conceptualization is reenforced by subscript ordering, \eg $m_{r,c}$ for a matrix and $c_{p,r,c}$ for a cube.
    921 Few programming languages differ from the mathematical subscript ordering.
    922 However, computer memory is flat, and hence, array forms are structured in memory as appropriate for the runtime system.
    923 The closest representation to the conceptual visualization is for an array object to be contiguous, and the language structures this memory using pointer arithmetic to access the values using various subscripts.
    924 This approach still has degrees of layout freedom, such as row or column major order, \ie juxtaposed rows or columns in memory, even when the subscript order remains fixed.
    925 For example, programming languages like MATLAB, Fortran, Julia and R store matrices in column-major order since they are commonly used for processing column-vectors in tabular data sets but retain row-major subscripting.
    926 In general, storage layout is hidden by subscripting, and only appears when passing arrays among different programming languages or accessing specific hardware.
    927 
    928 \VRef[Figure]{f:FixedVariable} shows two C90 approaches for manipulating a contiguous matrix.
    929 Note, C90 does not support VLAs.
    930 The fixed-dimension approach (left) uses the type system;
    931 however, it requires all dimensions except the first to be specified at compile time, \eg @m[][6]@, allowing all subscripting stride calculations to be generated with constants.
    932 Hence, every matrix passed to @fp1@ must have exactly 6 columns but the row size can vary.
    933 The variable-dimension approach (right) ignores (violates) the type system, \ie argument and parameters types do not match, and subscripting is performed manually using pointer arithmetic in the macro @sub@.
    934 
    935 \begin{figure}
    936 \begin{tabular}{@{}l@{\hspace{40pt}}l@{}}
    937 \multicolumn{1}{c}{\textbf{Fixed Dimension}} & \multicolumn{1}{c}{\textbf{Variable Dimension}} \\
    938 \begin{cfa}
    939 
    940 void fp1( int rows, int m[][@6@] ) {
    941         ...  printf( "%d ", @m[r][c]@ );  ...
    942 }
    943 int fm1[4][@6@], fm2[6][@6@]; // no VLA
    944 // initialize matrixes
    945 fp1( 4, fm1 ); // implicit 6 columns
    946 fp1( 6, fm2 );
    947 \end{cfa}
    948 &
    949 \begin{cfa}
    950 #define sub( m, r, c ) *(m + r * sizeof( m[0] ) + c)
    951 void fp2( int rows, int cols, int *m ) {
    952         ...  printf( "%d ", @sub( m, r, c )@ );  ...
    953 }
    954 int vm1[@4@][@4@], vm2[@6@][@8@]; // no VLA
    955 // initialize matrixes
    956 fp2( 4, 4, vm1 );
    957 fp2( 6, 8, vm2 );
    958 \end{cfa}
    959 \end{tabular}
    960 \caption{C90 Fixed \vs Variable Contiguous Matrix Styles}
    961 \label{f:FixedVariable}
    962 \end{figure}
    963 
    964 Many languages allow multidimensional arrays-of-arrays, \eg in Pascal or \CC.
    965 \begin{cquote}
    966 \begin{tabular}{@{}ll@{}}
    967 \begin{pascal}
    968 var m : array[0..4, 0..4] of Integer;  (* matrix *)
    969 type AT = array[0..4] of Integer;  (* array type *)
    970 type MT = array[0..4] of AT;  (* array of array type *)
    971 var aa : MT;  (* array of array variable *)
    972 m@[1][2]@ := 1;   aa@[1][2]@ := 1 (* same subscripting *)
    973 \end{pascal}
    974 &
    975 \begin{c++}
    976 int m[5][5];
    977 
    978 typedef vector< vector<int> > MT;
    979 MT vm( 5, vector<int>( 5 ) );
    980 m@[1][2]@ = 1;  aa@[1][2]@ = 1;
    981 \end{c++}
    982 \end{tabular}
    983 \end{cquote}
    984 The language decides if the matrix and array-of-array are laid out the same or differently.
    985 For example, an array-of-array may be an array of row pointers to arrays of columns, so the rows may not be contiguous in memory nor even the same length (triangular matrix).
    986 Regardless, there is usually a uniform subscripting syntax masking the memory layout, even though a language could differentiated between the two forms using subscript syntax, \eg @m[1,2]@ \vs @aa[1][2]@.
    987 Nevertheless, controlling memory layout can make a difference in what operations are allowed and in performance (caching/NUMA effects).
    988 
    989 C also provides non-contiguous arrays-of-arrays.
    990 \begin{cfa}
    991 int m[5][5];                                                    $\C{// contiguous}$
    992 int * aa[5];                                                    $\C{// non-contiguous}$
    993 \end{cfa}
    994 both with different memory layout using the same subscripting, and both with different degrees of issues.
    995 The focus of this work is on the contiguous multidimensional arrays in C.
    996 The reason is that programmers are often forced to use the more complex array-of-array form when a contiguous array would be simpler, faster, and safer.
    997 Nevertheless, the C array-of-array form is still important for special circumstances.
    998 
    999 \VRef[Figure]{f:ContiguousNon-contiguous} shows the extensions made in C99 for manipulating contiguous \vs non-contiguous arrays.\footnote{C90 also supported non-contiguous arrays.}
    1000 First, VLAs are supported.
    1001 Second, for contiguous arrays, C99 conjoins one or more of the parameters as a downstream dimension(s), \eg @cols@, implicitly using this parameter to compute the row stride of @m@.
    1002 If the declaration of @fc@ is changed to:
    1003 \begin{cfa}
    1004 void fc( int rows, int cols, int m[@rows@][@cols@] ) ...
    1005 \end{cfa}
    1006 it is possible for C to perform bound checking across all subscripting, but it does not.
    1007 While this contiguous-array capability is a step forward, it is still the programmer's responsibility to manually manage the number of dimensions and their sizes, both at the function definition and call sites.
    1008 That is, the array does not automatically carry its structure and sizes for use in computing subscripts.
    1009 While the non-contiguous style in @faa@ looks very similar to @fc@, the compiler only understands the unknown-sized array of row pointers, and it relies on the programmer to traverse the columns in a row correctly with a correctly bounded loop index.
    1010 Specifically, there is no requirement that the rows are the same length, like a poem with different length lines.
    1011 
    1012 \begin{figure}
    1013 \begin{tabular}{@{}ll@{}}
    1014 \multicolumn{1}{c}{\textbf{Contiguous}} & \multicolumn{1}{c}{\textbf{ Non-contiguous}} \\
    1015 \begin{cfa}
    1016 void fc( int rows, @int cols@, int m[ /* rows */ ][@cols@] ) {
    1017         ...  printf( "%d ", @m[r][c]@ );  ...
    1018 }
    1019 int m@[5][5]@;
    1020 for ( int r = 0; r < 5; r += 1 ) {
    1021 
    1022         for ( int c = 0; c < 5; c += 1 )
    1023                 m[r][c] = r + c;
    1024 }
    1025 fc( 5, 5, m );
    1026 \end{cfa}
    1027 &
    1028 \begin{cfa}
    1029 void faa( int rows, int cols, int * m[ @/* cols */@ ] ) {
    1030         ...  printf( "%d ", @m[r][c]@ );  ...
    1031 }
    1032 int @* aa[5]@;  // row pointers
    1033 for ( int r = 0; r < 5; r += 1 ) {
    1034         @aa[r] = malloc( 5 * sizeof(int) );@ // create rows
    1035         for ( int c = 0; c < 5; c += 1 )
    1036                 aa[r][c] = r + c;
    1037 }
    1038 faa( 5, 5, aa );
    1039 \end{cfa}
    1040 \end{tabular}
    1041 \caption{C99 Contiguous \vs Non-contiguous Matrix Styles}
    1042 \label{f:ContiguousNon-contiguous}
    1043 \end{figure}
    1044 
    1045 
    1046 \subsection{Multidimensional array implementation}
     863\section{Multidimensional array implementation}
    1047864\label{s:ArrayMdImpl}
    1048865
    … …  
    12211038        S & | sized(S),                 $\C{// masquerading-as}$
    12221039        Timmed &,                               $\C{// immediate element, often another array}$
    1223         Tbase &                                 $\C{// base element, e.g. float, never array}$
     1040        Tbase &                                 $\C{// base element, \eg float, never array}$
    12241041) { // distribute forall to each element
    12251042        struct arpk {
    … …  
    12741091
    12751092
    1276 
    1277 
     1093\section{Array lifecycle}
     1094
     1095An array is an aggregate, like a structure;
     1096both are containers wrapping subordinate objects.
     1097Any arbitrary object type, like @string@, can be an array element or structure member.
     1098A consequence is that the lifetime of the container must match with its subordinate objects: all elements and members must be initialized/uninitialized implicitly as part of the container's allocation/deallocation.
     1099Modern programming languages implicitly perform these operations via a type's constructor and destructor.
     1100Therefore, \CFA must assure that an array's subordinate objects' lifetime operations are called.
     1101
     1102Preexisting \CFA mechanisms achieve this requirement, but with poor performance.
     1103Furthermore, advanced array users need an exception to the basic mechanism, which does not occur with other aggregates.
     1104Hence, arrays introduce subleties in supporting an element's lifecycle.
     1105
     1106The preexisting \CFA support for contained-element lifecycle is based on recursive occurrences of the object-type (@otype@) pseudo-trait.
     1107A type is an @otype@, if it provides a default (parameterless) constructor, copy constructor, assignment operator, and destructor (like \CC).
     1108When declaring a structure with @otype@ members, the compiler implicitly generates implementations of the four @otype@ functions for the outer structure.
     1109Then the generated default constructor for the outer structure calls the default constructor for each member, and the other @otype@ functions work similarly.
     1110For a member that is a C array, these calls occur in a loop for each array element, which even works for VLAs.
     1111This logic works the same, whether the member is a concrete type (that happens to be an @otype@) or if the member is a polymorphic type asserted to be an @otype@ (which is implicit in the syntax, @forall(T)@).
     1112The \CFA array has the simplified form (similar to one seen before):
     1113\begin{cfa}
     1114forall( T * )   // non-otype element, no lifecycle functions
     1115// forall( T )  // otype element, lifecycle functions asserted
     1116struct array5 {
     1117        T __items[ 5 ];
     1118};
     1119\end{cfa}
     1120Being a structure with a C-array member, using the otype-form declaration for @T@ causes @array5(float)@ to implement @otype@ too.
     1121
     1122But this @otype@-recursion pattern has a performance issue.
     1123For example, in a cube of @float@:
     1124\begin{cfa}
     1125array5( array5( array5( float ) ) )
     1126\end{cfa}
     1127the first few steps of the compiler's work to find the lifecycle functions, under the @otype@-recursion pattern, are shown in \VRef[Figure]{f:OtypeRecursionBlowup}.
     1128All the work needed for the full @float@-cube would have 256 leaves.
     1129
     1130%array5(T) offers
     1131%1 parameterless ctor, which asks for T to have
     1132%       1 parameterless ctor
     1133%       2 copy ctor
     1134%       3 asgt
     1135%       4 dtor
     1136%2 copy ctor, which asks for T to have
     1137%       1 parameterless ctor
     1138%       2 copy ctor
     1139%       3 asgt
     1140%       4 dtor
     1141%3 asgt, which asks for T to have
     1142%       1 parameterless ctor
     1143%       2 copy ctor
     1144%       3 asgt
     1145%       4 dtor
     1146%4 dtor, which asks for T to have
     1147%       1 parameterless ctor
     1148%       2 copy ctor
     1149%       3 asgt
     1150%       4 dtor
     1151
     1152\begin{figure}
     1153\centering
     1154\setlength{\tabcolsep}{15pt}
     1155\begin{tabular}{@{}lll@{}}
     1156\begin{cfa}[deletekeywords={default}]
     1157float offers
     11581 default ctor
     11592 copy ctor
     11603 asgt
     11614 dtor
     1162
     1163
     1164
     1165
     1166
     1167
     1168
     1169
     1170
     1171
     1172
     1173
     1174
     1175
     1176
     1177
     1178
     1179
     1180
     1181
     1182
     1183
     1184
     1185
     1186\end{cfa}
     1187&
     1188\begin{cfa}[deletekeywords={default}]
     1189array5(float) has
     11901 default ctor, using float's
     1191        1 default ctor
     1192        2 copy ctor
     1193        3 asgt
     1194        4 dtor
     11952 copy ctor, using float's
     1196        1 default ctor
     1197        2 copy ctor
     1198        3 asgt
     1199        4 dtor
     12003 asgt, using float's
     1201        1 default ctor
     1202        2 copy ctor
     1203        3 asgt
     1204        4 dtor
     12054 dtor, using float's
     1206        1 default ctor
     1207        2 copy ctor
     1208        3 asgt
     1209        4 dtor
     1210
     1211
     1212
     1213
     1214
     1215
     1216
     1217
     1218\end{cfa}
     1219&
     1220\begin{cfa}[deletekeywords={default}]
     1221array5(array5(float)) has
     12221 default ctor, using array5(float)'s
     1223        1 default ctor, using float's
     1224                1 default ctor
     1225                2 copy ctor
     1226                3 asgt
     1227                4 dtor
     1228        2 copy ctor, using float's
     1229                1 default ctor
     1230                2 copy ctor
     1231                3 asgt
     1232                4 dtor
     1233        3 asgt, using float's
     1234                1 default ctor
     1235                2 copy ctor
     1236                3 asgt
     1237                4 dtor
     1238        4 dtor, using float's
     1239                1 default ctor
     1240                2 copy ctor
     1241                3 asgt
     1242                4 dtor
     12432 copy ctor, using array5(float)'s
     1244        ... 4 children, 16 leaves
     12453 asgt, using array5(float)'s
     1246        ... 4 children, 16 leaves
     12474 dtor, using array5(float)'s
     1248        ... 4 children, 16 leaves
     1249(64 leaves)
     1250\end{cfa}
     1251\end{tabular}
     1252\caption{Exponential thunk generation under the otype-recursion pattern.
     1253        Each time that one type's function (\eg ctor) uses another type's function, the \CFA compiler generates a thunk, to capture the used function's dependencies, presented according to the using function's need.
     1254        So, each non-leaf line represents a generated thunk and every line represents a search request for the resolver to find a satisfying function.}
     1255\label{f:OtypeRecursionBlowup}
     1256\end{figure}
     1257
     1258So the @otype@-recursion pattern seeks a quantity of helper functions, and generates a quantity of thunks, that are exponential in the number of dimensions.
     1259Anecdotal experience with this solution found the resulting compile times annoyingly slow at three dimensions, and unusable at four.
     1260
     1261The issue is that the otype-recursion pattern uses more assertions than needed.
     1262Consider how @array5(float)@'s default constructor is getting all four lifecycle assertions about the element type, @float@.
     1263It only needs @float@'s default constructor;
     1264the full set of operations is never used.
     1265Current work by the \CFA team aims to improve this situation.
     1266Therefore, a workaround is needed for now.
     1267
     1268The workaround is to provide a default constructor, copy constructor and destructor, defined with lean, bespoke assertions:
     1269\begin{cquote}
     1270\begin{tabular}{@{}l@{\hspace{0.5in}}l@{}}
     1271\begin{cfa}
     1272// autogenerated for otype-recursion:
     1273forall( T )
     1274void ?{}( array5(T) & this ) {
     1275        for (i; 5) { ( this[i] ){}; }
     1276}
     1277forall( T )
     1278void ?{}( array5(T) & this, array5(T) & src ) {
     1279        for (i; 5) { ( this[i] ){ src[i] }; }
     1280}
     1281forall( T )
     1282void ^?{}( array5(T) & this ) {
     1283        for (i; 5) { ^( this[i] ){}; }
     1284}
     1285\end{cfa}
     1286&
     1287\begin{cfa}
     1288// lean, bespoke:
     1289forall( T* | { void @?{}( T & )@; } )
     1290void ?{}( array5(T) & this ) {
     1291        for (i; 5) { ( this[i] ){}; }
     1292}
     1293forall( T* | { void @?{}( T &, T )@; } )
     1294void ?{}( array5(T) & this, array5(T) & src ) {
     1295        for (i; 5) { ( this[i] ){ src[i] }; }
     1296}
     1297forall( T* | { void @?{}( T & )@; } )
     1298void ^?{}( array5(T) & this ) {
     1299        for (i; 5) { ^( this[i] ){}; }
     1300}
     1301\end{cfa}
     1302\end{tabular}
     1303\end{cquote}
     1304Moreover, the assignment operator is skipped, to avoid hitting a lingering growth case.
     1305Skipping assignment is tolerable because array assignment is not a common operation.
     1306With this solution, the critical lifecycle functions are available, with no growth in thunk creation.
     1307
     1308Finally, the intuition that a programmer using an array always wants the elements' default constructor called \emph{automatically} is simplistic.
     1309Arrays exist to store different values at each position.
     1310So, array initialization needs to let the programmer provide different constructor arguments to each element.
     1311\begin{cfa}
     1312thread worker { int id; };
     1313void ?{}( worker & ) = void; // remove default constructor
     1314void ?{}( worker &, int id );
     1315array( worker, 5 ) ws = @{}@; // rejected; but desire is for no initialization yet
     1316for (i; 5) (ws[i]){ @i@ }; // explicitly initialize each thread, giving id
     1317\end{cfa}
     1318Note the use of the \CFA explicit constructor call, analogous to \CC's placement-@new@.
     1319This call is where initialization is desired, and not at the declaration of @ws@.
     1320The attempt to initialize from nothing (equivalent to dropping @= {}@ altogether) is invalid because the @worker@ type removes the default constructor.
     1321The @worker@ type is designed this way to work with the threading system.
     1322A thread type forks a thread at the end of each constructor and joins with it at the start of each destructor.
     1323But a @worker@ cannot begin its forked-thead work without knowing its @id@.
     1324Therefore, there is a conflict between the implicit actions of the builtin @thread@ type and a user's desire to defer these actions.
     1325
     1326Another \CFA feature may, at first, seem viable for initializing the array @ws@, though on closer inspection, it is not.
     1327C initialization, \lstinline|array(worker, 5) ws @= {};|, ignores all \CFA lifecycle management and uses C empty initialization.
     1328This option does achieve the desired semantics on the construction side.
     1329But on destruction side, the desired semantics is for implicit destructor calls to continue, to keep the join operation tied to lexical scope.
     1330C initialization disables \emph{all} implicit lifecycle management, but the goal is to disable only the implicit construction.
     1331
     1332To fix this problem, I enhanced the \CFA standard library to provide the missing semantics, available in either form:
     1333\begin{cfa}
     1334array( @uninit@(worker), 5 ) ws1;
     1335array( worker, 5) ws2 = { @delay_init@ };
     1336\end{cfa}
     1337Both cause the @ws@-construction-time implicit call chain to stop before reaching a @worker@ constructor, while leaving the implicit destruction calls intact.
     1338Two forms are available, to parallel the development of this feature in \uCpp.
     1339Originally \uCpp offered only the @ws1@ form, using the class-template @uNoCtor@ equivalent to \CFA's @uninit@.
     1340More recently, \uCpp was extended with the declaration macro, @uArray@, with usage similar to the @ws2@ case.
     1341Based on experience piloting @uArray@ as a replacement of @uNoCtor@, it might be possible to remove the first option.
     1342
     1343% note to Mike, I have more fragments on some details available in push24\fragments\uNoCtor.txt
    12781344
    12791345\section{Comparison with other arrays}
Note: See TracChangeset for help on using the changeset viewer.