Context Navigation

-              r2c065ed
+              r579427b
 though using a new style of generic parameter.
 \begin{cfa}
 @array( float, 99 )@ x;                                 $\C[2.75in]{// x contains 99 floats}$
 \end{cfa}
 Here, the arguments to the @array@ type are @float@ (element type) and @99@ (length).
 When this type is used as a function parameter, the type-system requires that a call's argument is a perfect match.
+@array( float, 99 )@ x;                                 $\C[2.5in]{// x contains 99 floats}$
+\end{cfa}
+Here, the arguments to the @array@ type are @float@ (element type) and @99@ (dimension).
+When this type is used as a function parameter, the type-system requires the argument is a perfect match.
 \begin{cfa}
 void f( @array( float, 42 )@ & p ) {}   $\C{// p accepts 42 floats}$
 f( x );                                                                 $\C{// statically rejected: type lengths are different, 99 != 42}$
 test2.cfa:3:1 error: Invalid application of existing declaration(s) in expression.
 Applying untyped:  Name: f ... to:  Name: x
 \end{cfa}
+Here, the function @f@'s parameter @p@ is declared with length 42.
+However, the call @f( x )@ is invalid, because @x@'s length is @99@, which does not match @42@.
+A function declaration can be polymorphic over these @array@ arguments by using the \CFA @forall@ declaration prefix.
+Function @f@'s parameter expects an array with dimension 42, but the argument dimension 99 does not match.
+A function can be polymorphic over @array@ arguments using the \CFA @forall@ declaration prefix.
 \begin{cfa}
 forall( T, @[N]@ )
 …
+}
 g( x, 0 );                                                              $\C{// T is float, N is 99, dynamic subscript check succeeds}$
+g( x, 1000 );                                                   $\C{// T is float, N is 99, dynamic subscript check fails}\CRT$
+g( x, 1000 );                                                   $\C{// T is float, N is 99, dynamic subscript check fails}$
 Cforall Runtime error: subscript 1000 exceeds dimension range [0,99) $for$ array 0x555555558020.
 \end{cfa}
+Function @g@ takes an arbitrary type parameter @T@ and a \emph{dimension parameter} @N@.
+A dimension parameter represents a to-be-determined count of elements, managed by the type system.
+The 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@.
+Inferring values for @T@ and @N@ is implicit.
+Furthermore, 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@.
+However, the call @g( x, 1000 )@ is also accepted through compile time;
+however, this case's subscript, @x[1000]@, generates an error, because @1000@ is outside the dimension range $[0,99)$ of argument @x@.
+Function @g@ takes an arbitrary type parameter @T@ and an unsigned integer \emph{dimension} @N@.
+The dimension represents a to-be-determined number of elements, managed by the type system, where 0 represents an empty array.
+The type system implicitly infers @float@ for @T@ and @99@ for @N@.
+Furthermore, the runtime subscript @x[0]@ (parameter @i@ being @0@) in @g@ is valid because 0 is in the dimension range $[0,99)$ for argument @x@.
+The call @g( x, 1000 )@ is also accepted at compile time.
+However, the subscript, @x[1000]@, generates a runtime error, because @1000@ is outside the dimension range $[0,99)$ of argument @x@.
 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.
 The syntactic form is chosen to parallel other @forall@ forms:
 \begin{cfa}
 forall( @[N]@ ) ...     $\C[1.5in]{// dimension}$
 forall( T ) ...         $\C{// value datatype (formerly, "otype")}$
 forall( T & ) ...       $\C{// opaque datatype (formerly, "dtype")}\CRT$
+forall( @[N]@ ) ...     $\C{// dimension}$
+forall( T ) ...         $\C{// value datatype}$
+forall( T & ) ...       $\C{// opaque datatype}$
 \end{cfa}
 % The notation @array(thing, N)@ is a single-dimensional case, giving a generic type instance.
 …
 \begin{cfa}
 forall( [N] )
+void declDemo( ... ) {
+        float x1[N];                                            $\C{// built-in type ("C array")}$
+        array(float, N) x2;                                     $\C{// type from library}$
+}
+\end{cfa}
+Both of the locally-declared array variables, @x1@ and @x2@, have 42 elements, each element being a @float@.
+The two variables have identical size and layout; they both encapsulate 42-float stack allocations, with no additional ``bookkeeping'' allocations or headers.
+void f( ... ) {
+        float x1[@N@];                                          $\C{// C array, no subscript checking}$
+        array(float, N) x2;                                     $\C{// \CFA array, subscript checking}\CRT$
+}
+\end{cfa}
+Both of the stack declared array variables, @x1@ and @x2@, have 42 elements, each element being a @float@.
+The two variables have identical size and layout, with no additional ``bookkeeping'' allocations or headers.
+The C array, @x1@, has no subscript checking, while \CFA array, @x2@, does.
 Providing 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.
+In 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@.
+Admittedly, the @array@ library type for @x2@ is syntactically different from its C counterpart.
+A future goal (TODO xref) is to provide the new @array@ features with syntax approaching C's (declaration style of @x1@).
+In all following discussion, ``C array'' means types like @x1@ and ``\CFA array'' means types like @x2@.
+A future goal is to provide the new @array@ features with syntax approaching C's (declaration style of @x1@).
 Then, the library @array@ type could be removed, giving \CFA a largely uniform array type.
+At present, the C-syntax @array@ is only partially supported, so the generic @array@ is used exclusively in the thesis;
+feature support and C compatibility are revisited in Section ? TODO.
+At present, the C-syntax @array@ is only partially supported, so the generic @array@ is used exclusively in the thesis.
 My contributions in this chapter are:
 \begin{enumerate}
+\begin{enumerate}[leftmargin=*]
 \item A type system enhancement that lets polymorphic functions and generic types be parameterized by a numeric value: @forall( [N] )@.
 \item Provide a length-checked array-type in the \CFA standard library, where the array's length is statically managed and dynamically valued.
+\item Provide a dimension/subscript-checked array-type in the \CFA standard library, where the array's length is statically managed and dynamically valued.
 \item Provide argument/parameter passing safety for arrays and subscript safety.
-\item TODO: general parking...
 \item Identify the interesting specific abilities available by the new @array@ type.
 \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.
 …
+\begin{comment}
 \section{Dependent Typing}
+General dependent typing allows the type system to encode arbitrary predicates (\eg behavioural specifications for functions),
+which is an anti-goal for my work.
+General dependent typing allows a type system to encode arbitrary predicates, \eg behavioural specifications for functions, which is an anti-goal for my work.
 Firstly, this application is strongly associated with pure functional languages,
 where a characterization of the return value (giving it a precise type, generally dependent upon the parameters)
 …
 Secondly, TODO: bash Rust.
 TODO: cite the crap out of these claims.
+\end{comment}
 \section{Features Added}
 This section shows more about using the \CFA array and dimension parameters, demonstrating their syntax and semantics by way of motivating examples.
+This section shows more about using the \CFA array and dimension parameters, demonstrating syntax and semantics by way of motivating examples.
 As stated, the core capability of the new array is tracking all dimensions within the type system, where dynamic dimensions are represented using type variables.
 By declaring type variables at the front of object declarations, an array dimension is lexically referenceable where it is needed.
+For example, a declaration can share one length, @N@, among a pair of parameters and the return,
+meaning that it requires both input arrays to be of the same length, and guarantees that the result is of that length as well.
+For example, a declaration can share one length, @N@, among a pair of parameters and return type, meaning the input arrays and return array are the same length.
 \lstinput{10-17}{hello-array.cfa}
 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.
 The dynamic allocation of the @ret@ array, by the library @alloc@ function,
+The dynamic allocation of the @ret@ array uses the library @alloc@ function,
 \begin{cfa}
 forall( T & | sized(T) )
 …
+}
 \end{cfa}
 uses the parameterized dimension information implicitly within its @sizeof@ determination, and casts the return type.
 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@.
+which captures the parameterized dimension information implicitly within its @sizeof@ determination, and casts the return type.
+Note, @alloc@ only sees the whole type for its @T@, @array(bool, N)@, where this type's size is a computation based on @N@.
 This example illustrates how the new @array@ type plugs into existing \CFA behaviour by implementing necessary \emph{sized} assertions needed by other types.
 (\emph{sized} implies a concrete \vs abstract type with a runtime-available size, exposed as @sizeof@.)
 …
 \lstinput{30-43}{hello-array.cfa}
 \lstinput{45-48}{hello-array.cfa}
 \caption{\lstinline{f} Harness}
 \label{f:fHarness}
+\caption{\lstinline{f} Example}
+\label{f:fExample}
 \end{figure}
 \VRef[Figure]{f:fHarness} shows a harness that uses function @f@, illustrating how dynamic values are fed into the @array@ type.
+\VRef[Figure]{f:fExample} shows an example using function @f@, illustrating how dynamic values are fed into the @array@ type.
 Here, the dimension of arrays @x@, @y@, and @result@ is specified from a command-line value, @dim@, and these arrays are allocated on the stack.
 Then the @x@ array is initialized with decreasing values, and the @y@ array with amounts offset by constant @0.005@, giving relative differences within tolerance initially and diverging for later values.
 …
 In summary:
 \begin{itemize}
+\begin{itemize}[leftmargin=*]
 \item
 @[N]@ within a @forall@ declares the type variable @N@ to be a managed length.
 \item
 @N@ can be used an expression of type @size_t@ within the declared function body.
+@N@ can be used in an expression with type @size_t@ within the function body.
 \item
 The value of an @N@-expression is the acquired length, derived from the usage site, \ie generic declaration or function call.
 …
 \begin{enumerate}[leftmargin=*]
 \item
+The \CC template @N@ can only be compile-time value, while the \CFA @N@ may be a runtime value.
+% agreed, though already said
+The \CC template @N@ can only be a compile-time value, while the \CFA @N@ may be a runtime value.
 \item
 \CC does not allow a template function to be nested, while \CFA lets its polymorphic functions to be nested.
+% why is this important?
+\item
+Hence, \CC precludes a simple form of information hiding.
+\item
+\label{p:DimensionPassing}
 The \CC template @N@ must be passed explicitly at the call, unless @N@ has a default value, even when \CC can deduct the type of @T@.
 The \CFA @N@ is part of the array type and passed implicitly at the call.
 …
 % mycode/arrr/thesis-examples/check-peter/cs-cpp.cpp, v2
 \item
 \CC cannot have an array of references, but can have an array of pointers.
+\CC cannot have an array of references, but can have an array of @const@ pointers.
 \CC has a (mistaken) belief that references are not objects, but pointers are objects.
 In the \CC example, the arrays fall back on C arrays, which have a duality with references with respect to automatic dereferencing.
 …
 % https://stackoverflow.com/questions/922360/why-cant-i-make-a-vector-of-references
 \item
+\label{p:ArrayCopy}
 C/\CC arrays cannot be copied, while \CFA arrays can be copied, making them a first-class object (although array copy is often avoided for efficiency).
 % fixed by comparing to std::array
 % mycode/arrr/thesis-examples/check-peter/cs-cpp.cpp, v10
 \end{enumerate}
 TODO: settle Mike's concerns with this comparison (perhaps, remove)
+The \CC template @array@ type mitigates points \VRef[]{p:DimensionPassing} and \VRef[]{p:ArrayCopy}, but it is also trying to accomplish a similar mechanism to \CFA @array@.
 \begin{figure}
 …
 Just as the first example in \VRef[Section]{s:ArrayIntro} shows a compile-time rejection of a length mismatch,
 so are length mismatches stopped when they involve dimension parameters.
 While \VRef[Figure]{f:fHarness} shows successfully calling a function @f@ expecting two arrays of the same length,
+While \VRef[Figure]{f:fExample} shows successfully calling a function @f@ expecting two arrays of the same length,
 \begin{cfa}
 array( bool, N ) & f( array( float, N ) &, array( float, N ) & );
 …
 The same argument safety and the associated implicit communication of array length occurs.
 Preexisting \CFA allowed aggregate types to be generalized with type parameters, enabling parameterizing of element types.
+Now, \CFA also allows parameterizing them by length.
+Doing so gives a refinement of C's ``flexible array member'' pattern[TODO: cite ARM 6.7.2.1 pp18]\cite{arr:gnu-flex-mbr}.
+While a C flexible array member can only occur at the end of the enclosing structure,
+\CFA allows length-parameterized array members to be nested at arbitrary locations.
+This flexibility, in turn, allows for multiple array members.
+This has been extended to allow parameterizing by dimension.
+Doing so gives a refinement of C's ``flexible array member''~\cite[\S~6.7.2.1.18]{C11}.
+\begin{cfa}
+struct S {
+        ...
+        double d []; // incomplete array type => flexible array member
+} * s = malloc( sizeof( struct S ) + sizeof( double [10] ) );
+\end{cfa}
+which creates a VLA of size 10 @double@s at the end of the structure.
+A C flexible array member can only occur at the end of a structure;
+\CFA allows length-parameterized array members to be nested at arbitrary locations, with intervening member declarations.
 \lstinput{10-15}{hello-accordion.cfa}
 The structure has course- and student-level metatdata (their respective field names) and a position-based preferences' matrix.
 Its 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.
 \VRef[Figure]{f:checkHarness} shows a program main using @School@ and results with different array sizes.
+\VRef[Figure]{f:checkExample} shows a program main using @School@ and results with different array sizes.
 The @school@ variable holds many students' course-preference forms.
 It is on the stack and its initialization does not use any casting or size arithmetic.
 …
 \end{cquote}
 \caption{\lstinline{School} harness, input and output}
 \label{f:checkHarness}
+\caption{\lstinline{School} Example, Input and Output}
+\label{f:checkExample}
 \end{figure}
 When a function operates on a @School@ structure, the type system handles its memory layout transparently.
 \lstinput{30-37}{hello-accordion.cfa}
 In the example, this @getPref@ function answers, for the student at position @is@, what is the position of its @pref@\textsuperscript{th}-favoured class?
+In the example, function @getPref@ returns, for the student at position @is@, what is the position of their @pref@\textsuperscript{th}-favoured class?
 …
 The repurposed heavy equipment is
 \begin{itemize}
+\begin{itemize}[leftmargin=*]
 \item
         Resolver provided values for a used declaration's type-system variables,
 …
 int main() {
         thing( @10@ ) x;  f( x );  $\C{// prints 10, [4]}$
+        thing( 100 ) y;  f( y );  $\C{// prints 100}$
+        return 0;
+        thing( @100@ ) y;  f( y );  $\C{// prints 100}$
+}
 \end{cfa}
 This example has:
 \begin{enumerate}
+\begin{enumerate}[leftmargin=*]
 \item
         The symbol @N@ being declared as a type variable (a variable of the type system).
 …
 Because the box pass handles a type's size as its main datum, the encoding is chosen to use it.
 The production and recovery are then straightforward.
 \begin{itemize}
+\begin{itemize}[leftmargin=*]
 \item
         The value $n$ is encoded as a type whose size is $n$.
 \item
         Given a dimension expression $e$, produce type @char[@$e$@]@ to represent it.
+        Given a dimension expression $e$, produce an internal type @char[@$e$@]@ to represent it.
         If $e$ evaluates to $n$ then the encoded type has size $n$.
 \item
 …
+}
 int main() {
+        thing( char[@10@] ) x;  f( x );  $\C{// prints 10, [4]}$
+        thing( char[100] ) y;  f( y );  $\C{// prints 100}$
+        return 0;
+        thing( @char[10]@ ) x;  f( x );  $\C{// prints 10, [4]}$
+        thing( @char[100]@ ) y;  f( y );  $\C{// prints 100}$
+}
 \end{cfa}
 Observe:
 \begin{enumerate}
+\begin{enumerate}[leftmargin=*]
 \item
         @N@ is now declared to be a type.
         It is declared to be \emph{sized} (by the @*@), meaning that the box pass shall do its @sizeof(N)@--@__sizeof_N@ extra parameter and expression translation.
+        It is declared to be \emph{sized} (by the @*@), meaning that the box pass shall do its @sizeof(N)@$\rightarrow$@__sizeof_N@ extra parameter and expression translation.
 \item
         @thing(N)@ is a type; the argument to the generic @thing@ is a type (type variable).
 …
         The @sout...@ expression (being an application of the @?|?@ operator) has a second argument that is an ordinary expression.
 \item
         The type of variable @x@ is another @thing(-)@ type; the argument to the generic @thing@ is a type (array type of bytes, @char@).
+        The type of variable @x@ is another @thing(-)@ type; the argument to the generic @thing@ is a type (array type of bytes, @char[@$e$@]@).
 \end{enumerate}
 …
         struct __conc_thing_10 {} x;  f( @10@, &x );  $\C{// prints 10, [4]}$
         struct __conc_thing_100 {} y;  f( @100@, &y );  $\C{// prints 100}$
-        return 0;
+}
 \end{cfa}
 Observe:
 \begin{enumerate}
+\begin{enumerate}[leftmargin=*]
 \item
         The type parameter @N@ is gone.
 …
         The @sout...@ expression (being an application of the @?|?@ operator) has a regular variable (parameter) usage for its second argument.
 \item
         Information about the particular @thing@ instantiation (value 10) has moved, from the type, to a regular function-call argument.
+        Information about the particular @thing@ instantiation (value 10) is moved, from the type, to a regular function-call argument.
 \end{enumerate}
 At the end of the desugaring and downstream processing, the original C idiom of ``pass both a length parameter and a pointer'' has been reconstructed.
 …
 The compiler's action produces the more complex form, which if handwritten, would be error-prone.
 Back at the compiler front end, the parsing changes AST schema extensions and validation rules for enabling the sugared user input.
 \begin{itemize}
+At the compiler front end, the parsing changes AST schema extensions and validation rules for enabling the sugared user input.
+\begin{itemize}[leftmargin=*]
 \item
         Recognize the form @[N]@ as a type-variable declaration within a @forall@.
 …
         Have the new brand of type-variable, \emph{Dimension}, in the AST form of a type-variable, to represent one parsed from @[-]@.
 \item
         Allow a type variable to occur in an expression.  Validate (after parsing) that only dimension-branded type variables are used here.
+        Allow a type variable to occur in an expression.  Validate (after parsing) that only dimension-branded type-variables are used here.
 \item
         Allow an expression to occur in type-argument position.  Brand the resulting type argument as a dimension.
 …
 \label{s:ArrayTypingC}
+Essential in giving a guarantee of accurate length is the compiler's ability
+to reject a program that presumes to mishandle length.
+By contrast, most discussion so far dealt with communicating length,
+from one party who knows it, to another who is willing to work with any given length.
+For scenarios where the concern is a mishandled length,
+the interaction is between two parties who both claim to know something about it.
+Such a scenario occurs in this pure C fragment, which today's C compilers accept:
+\begin{cfa}
+int n = @42@;
+float x[n];
+float (*xp)[@999@] = &x;
+Essential in giving a guarantee of accurate length is the compiler's ability to reject a program that presumes to mishandle length.
+By contrast, most discussion so far deals with communicating length, from one party who knows it, to another willing to work with any given length.
+For scenarios where the concern is a mishandled length, the interaction is between two parties who both claim to know something about it.
+C and \CFA can check when working with two static values.
+\begin{cfa}
+enum { n = 42 };
+float x[@n@];   // or just 42
+float (*xp1)[@42@] = &x;    // accept
+float (*xp2)[@999@] = &x;   // reject
+warning: initialization of 'float (*)[999]' from incompatible pointer type 'float (*)[42]'
+\end{cfa}
+When a variable is involved, C and \CFA take two different approaches.
+Today's C compilers accept the following without warning.
+\begin{cfa}
+static const int n = 42;
+float x[@n@];
+float (* xp)[@999@] = &x; $\C{// should be static rejection here}$
 (*xp)[@500@]; $\C{// in "bound"?}$
 \end{cfa}
 Here, the array @x@ has length 42, while a pointer to it (@xp@) claims length 999.
 So, while the subscript of @xp@ at position 500 is out of bound of its referent @x@,
+So, while the subscript of @xp@ at position 500 is out of bound with its referent @x@,
 the access appears in-bound of the type information available on @xp@.
+Truly, length is being mishandled in the previous step,
+where the type-carried length information on @x@ is not compatible with that of @xp@.
+The \CFA new-array rejects the analogous case:
+\begin{cfa}
+int n = @42@;
+array(float, n) x;
+array(float, 999) * xp = x; $\C{// static rejection here}$
+(*xp)[@500@]; $\C{// runtime check vs len 999}$
+\end{cfa}
+The way the \CFA array is implemented, the type analysis of this case reduces to a case similar to the earlier C version.
+In fact, length is being mishandled in the previous step, where the type-carried length information on @x@ is not compatible with that of @xp@.
+In \CFA, I choose to reject this C example at the point where the type-carried length information on @x@ is not compatible with that of @xp@, and correspondingly, its array counterpart at the same location:
+\begin{cfa}
+static const int n = 42;
+array( float, @n@ ) x;
+array( float, @999@ ) * xp = &x; $\C{// static rejection here}$
+(*xp)[@500@]; $\C{// runtime check passes}$
+\end{cfa}
+The way the \CFA array is implemented, the type analysis for this case reduces to a case similar to the earlier C version.
 The \CFA compiler's compatibility analysis proceeds as:
 \begin{itemize}[parsep=0pt]
 \item
+        Is @array(float, 999)@ type-compatible with @array(float, n)@?
+\item
+        Is @arrayX(float, char[999])@ type-compatible with @arrayX(float, char[n])@?\footnote{
+                Here, \lstinline{arrayX} represents the type that results
+                from desugaring the \lstinline{array} type
+                into a type whose generic parameters are all types.
+                This presentation elides the noisy fact that
+                \lstinline{array} is actually a macro for something bigger;
+                the reduction to \lstinline{char[-]} still proceeds as sketched.}
+\item
+        Is @char[999]@ type-compatible with @char[n]@?
+        Is @array( float, 999 )@ type-compatible with @array( float, n )@?
+\item
+        Is desugared @array( float, char[999] )@ type-compatible with desugared @array( float, char[n] )@?
+%               \footnote{
+%               Here, \lstinline{arrayX} represents the type that results from desugaring the \lstinline{array} type into a type whose generic parameters are all types.
+%               This presentation elides the noisy fact that \lstinline{array} is actually a macro for something bigger;
+%               the reduction to \lstinline{char [-]} still proceeds as sketched.}
+\item
+        Is internal type @char[999]@ type-compatible with internal type @char[n]@?
 \end{itemize}
+To achieve the necessary \CFA rejections meant rejecting the corresponding C case, which is not backward compatible.
+There are two complementary mitigations for this incompatibility.
+First, a simple recourse is available to a programmer who intends to proceed
+with the statically unsound assignment.
+This situation might arise if @n@ were known to be 999,
+rather than 42, as in the introductory examples.
+The programmer can add a cast in the \CFA code.
+\begin{cfa}
+xp = @(float (*)[999])@ &x;
+\end{cfa}
+This addition causes \CFA to accept, because now, the programmer has accepted blame.
+This addition is benign in plain C, because the cast is valid, just unnecessary there.
+Moreover, the addition can even be seen as appropriate ``eye candy,''
+marking where the unchecked length knowledge is used.
+Therefore, a program being onboarded to \CFA can receive a simple upgrade,
+to satisfy the \CFA rules (and arguably become clearer),
+without giving up its validity to a plain C compiler.
+Second, the incompatibility only affects types like pointer-to-array,
+which are are infrequently used in C.
+The more common C idiom for aliasing an array is to use a pointer-to-first-element type,
+which does not participate in the \CFA array's length checking.\footnote{
+The answer is false because, in general, the value of @n@ is unknown at compile time, and hence, an error is raised.
+For safety, it makes sense to reject the corresponding C case, which is a non-backwards compatible change.
+There are two mitigations for this incompatibility.
+First, a simple recourse is available in a situation where @n@ is \emph{known} to be 999 by using a cast.
+\begin{cfa}
+float (* xp)[999] = @(float (*)[999])@&x;
+\end{cfa}
+The cast means the programmer has accepted blame.
+Moreover, the cast is ``eye candy'' marking where the unchecked length knowledge is used.
+Therefore, a program being onboarded to \CFA requires some upgrading to satisfy the \CFA rules (and arguably become clearer), without giving up its validity to a plain C compiler.
+Second, the incompatibility only affects types like pointer-to-array, which are infrequently used in C.
+The more common C idiom for aliasing an array is to use a pointer-to-first-element type, which does not participate in the \CFA array's length checking.\footnote{
         Notably, the desugaring of the \lstinline{array} type avoids letting any \lstinline{-[-]} type decay,
         in order to preserve the length information that powers runtime bound-checking.}
+Therefore, the frequency of needing to upgrade legacy C code (as discussed in the first mitigation)
+is anticipated to be low.
+Because the incompatibility represents a low cost to a \CFA onboarding effort
+(with a plausible side benefit of linting the original code for a missing annotation),
+no special measures were added to retain the compatibility.
+It would be possible to flag occurrences of @-[-]@ types that come from @array@ desugaring,
+treating those with stricter \CFA rules, while treating others with classic C rules.
+If future lessons from C project onboarding warrant it,
+this special compatibility measure can be added.
+Having allowed that both the initial C example's check
+\begin{itemize}
+        \item
+                Is @float[999]@ type-compatible with @float[n]@?
+\end{itemize}
+and the second \CFA example's induced check
+\begin{itemize}
+        \item
+                Is @char[999]@ type-compatible with @char[n]@?
+\end{itemize}
+shall have the same answer, (``no''),
+discussion turns to how I got the \CFA compiler to produce this answer.
+In its preexisting form, it produced a (buggy) approximation of the C rules.
+To implement the new \CFA rules, I took the syntactic recursion a step further, obtaining,
+in both cases:
+\begin{itemize}
+        \item
+                Is @999@ compatible with @n@?
+\end{itemize}
+This compatibility question applies to a pair of expressions, where the earlier implementation were to types.
+Such an expression-compatibility question is a new addition to the \CFA compiler.
+Note, these questions only arise in the context of dimension expressions on (C) array types.
+TODO: ensure these compiler implementation matters are treated under \CFA compiler background:
+type unification,
+cost calculation,
+GenPoly.
+The relevant technical component of the \CFA compiler is the type unification procedure within the type resolver.
+I added rules for continuing this unification into expressions that occur within types.
+It is still fundamentally doing \emph{type} unification
+because it is participating in binding type variables,
+and not participating in binding any variables that stand in for expression fragments
+(for there is no such sort of variable in \CFA's analysis.)
+An unfortunate fact about the \CFA compiler's preexisting implementation is that
+type unification suffers from two forms of duplication.
+The first duplication has (many of) the unification rules stated twice.
+As a result, my additions for dimension expressions are stated twice.
+The extra statement of the rules occurs in the @GenPoly@ module,
+where concrete types like @array(int, 5)@\footnote{
+        Again, the presentation is simplified
+        by leaving the \lstinline{array} macro unexpanded.}
+are lowered into corresponding C types @struct __conc_array_1234@ (the suffix being a generated index).
+In this case, the struct's definition contains fields that hardcode the argument values of @float@ and @5@.
+The next time an @array(-,-)@ concrete instance is encountered, it checks if the previous @struct __conc_array_1234@ is suitable for it.
+Yes, for another occurrence of @array(int, 5)@;
+no, for either @array(rational(int), 5)@ or @array(int, 42)@.
+By the last example, this phase must ``reject''
+the hypothesis that it should reuse the dimension-5 instance's C-lowering for a dimension-42 instance.
+The second duplication has unification (proper) being invoked at two stages of expression resolution.
+As a result, my added rule set needs to handle more cases than the preceding discussion motivates.
+In the program
+\begin{cfa}
+void @f@( double );
+forall( T & ) void @f@( T & );
+void g( int n ) {
+        array( float, n + 1 ) x;
+        f(x);   // overloaded
+}
+\end{cfa}
+when resolving the function call, @g@, the first unification stage
+compares the type @T@ of the parameter with @array( float, n + 1 )@, of the argument.
+TODO: finish.
+The actual rules for comparing two dimension expressions are conservative.
+To answer, ``yes, consider this pair of expressions to be matching,''
+is to imply, ``all else being equal, allow an array with length calculated by $e_1$
+to be passed to a function expecting a length-$e_2$ array.''\footnote{
+        TODO: Deal with directionality, that I'm doing exact-match, no ``at least as long as,'' no subtyping.
+        Should it be an earlier scoping principle?  Feels like it should matter in more places than here.}
+So, a ``yes'' answer must represent a guarantee that both expressions evaluate the
+same result, while a ``no'' can tolerate ``they might, but we're not sure'',
+provided that practical recourses are available
+to let programmers express better knowledge.
+The new rule-set in the current release is, in fact, extremely conservative.
+I chose to keep things simple,
+and allow future needs to drive adding additional complexity, within the new framework.
+For starters, the original motivating example's rejection
+is not based on knowledge that
+the @xp@ length of (the literal) 999 is value-unequal to
+the (obvious) runtime value of the variable @n@, which is the @x@ length.
+Rather, the analysis assumes a variable's value can be anything,
+and so there can be no guarantee that its value is 999.
+So, a variable and a literal can never match.
+Two occurrences of the same literal value are obviously a fine match.
+For two occurrences of the same variable, more information is needed.
+For example, this one is fine
+\begin{cfa}
+void f( const int n ) {
+        float x[n];
+        float (*xp)[n] = x;   // accept
+}
+\end{cfa}
+while this one is not:
+\begin{cfa}
+Therefore, the need to upgrade legacy C code is low.
+Finally, if this incompatibility is a problem onboarding C programs to \CFA, it is should be possible to change the C type check to a warning rather than an error, acting as a \emph{lint} of the original code for a missing type annotation.
+To handle two occurrences of the same variable, more information is needed, \eg, this is fine,
+\begin{cfa}
+int n = 42;
+float x[@n@];
+float (*xp)[@n@] = x;   // accept
+\end{cfa}
+where @n@ remains fixed across a contiguous declaration context.
+However, intervening dynamic statement cause failures.
+\begin{cfa}
+int n = 42;
+float x[@n@];
+@n@ = 999; // dynamic change
+float (*xp)[@n@] = x;   // reject
+\end{cfa}
+However, side-effects can occur in a contiguous declaration context.
+\begin{cquote}
+\setlength{\tabcolsep}{20pt}
+\begin{tabular}{@{}ll@{}}
+\begin{cfa}
+// compile unit 1
+extern int @n@;
+extern float g();
 void f() {
+        int n = 42;
+        float x[n];
+        n = 999;
+        float (*xp)[n] = x;   // reject
+}
+\end{cfa}
+Furthermore, the fact that the first example sees @n@ as @const@
+is not actually sufficient.
+In this example, @f@'s length expression's declaration is as @const@ as it can be,
+yet its value still changes between the two invocations:
+\begin{cquote}
+\setlength{\tabcolsep}{15pt}
+\begin{tabular}{@{}ll@{}}
+\begin{cfa}
+// compile unit 1
+void g();
+void f( const int & const nr ) {
+        float x[nr];
+        g();    // change n
+        @float (*xp)[nr] = x;@   // reject
+        float x[@n@] = { g() };
+        float (*xp)[@n@] = x;   // reject
+}
 \end{cfa}
 …
 \begin{cfa}
 // compile unit 2
 static int n = 42;
+int @n@ = 42;
 void g() {
         n = 99;
+}
+f( n );
+        @n@ = 99;
+}
 \end{cfa}
 \end{tabular}
 …
 The issue here is that knowledge needed to make a correct decision is hidden by separate compilation.
 Even within a translation unit, static analysis might not be able to provide all the information.
+My rule set also respects a traditional C feature: In spite of the several limitations of the C rules
+accepting cases that produce different values, there are a few mismatches that C stops.
+C is quite precise when working with two static values.
+\begin{cfa}
+enum { fortytwo = 42 };
+float x[fortytwo];
+float (*xp1)[42] = &x;    // accept
+float (*xp2)[999] = &x;   // reject
+\end{cfa}
+My \CFA rules agree with C's on these cases.
+However, if the example uses @const@, the check is possible.
+\begin{cquote}
+\setlength{\tabcolsep}{20pt}
+\begin{tabular}{@{}ll@{}}
+\begin{cfa}
+// compile unit 1
+extern @const@ int n;
+extern float g();
+void f() {
+        float x[n] = { g() };
+        float (*xp)[n] = x;   // reject
+}
+\end{cfa}
+&
+\begin{cfa}
+// compile unit 2
+@const@ int n = 42;
+void g() {
+        @n = 99@; // allowed
+}
+\end{cfa}
+\end{tabular}
+\end{cquote}
 In summary, the new rules classify expressions into three groups:
 \begin{description}
 \item[Statically Evaluable]
+        Expressions for which a specific value can be calculated (conservatively)
+        at compile-time.
+        A preexisting \CFA compiler module defines which literals, enumerators, and expressions qualify,
+        and evaluates them.
+        Expressions for which a specific value can be calculated (conservatively) at compile-time.
+        A preexisting \CFA compiler module defines which literals, enumerators, and expressions qualify and evaluates them.
 \item[Dynamic but Stable]
         The value of a variable declared as @const@, including a @const@ parameter.
 \item[Potentially Unstable]
         The catch-all category.  Notable examples include:
+        any function-call result, @float x[foo()];@,
+        the particular function-call result that is a pointer dereference, @void f(const int * n)@ @{ float x[*n]; }@, and
+        any use of a reference-typed variable.
+        any function-call result, @float x[foo()]@, the particular function-call result that is a pointer dereference, @void f(const int * n)@ @{ float x[*n]; }@, and any use of a reference-typed variable.
 \end{description}
 Within these groups, my \CFA rules are:
 \begin{itemize}
+\begin{itemize}[leftmargin=*]
 \item
         Accept a Statically Evaluable pair, if both expressions have the same value.
 …
 \end{itemize}
 The traditional C rules are:
 \begin{itemize}
+\begin{itemize}[leftmargin=*]
 \item
         Reject a Statically Evaluable pair, if the expressions have two different values.
 …
         Otherwise, accept.
 \end{itemize}
+\VRef[Figure]{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
+It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafe.
+It also shows that C-incompatibilities only occur in cases that C treats unsafe.
 \begin{figure}
 …
                 where \lstinline{expr1} and \lstinline{expr2} are meta-variables varying according to the row's Case.
                 Each row's claim applies to other harnesses too, including,
                 \begin{itemize}
+                \begin{itemize}[leftmargin=*]
                 \item
                         calling a function with a parameter like \lstinline{x} and an argument of the \lstinline{xp} type,
 …
                 The table treats symbolic identity (Same/Different on rows)
                 apart from value equality (Equal/Unequal on columns).
                 \begin{itemize}
+                \begin{itemize}[leftmargin=*]
                 \item
                         The expressions \lstinline{1}, \lstinline{0+1} and \lstinline{n}
 …
 \end{figure}
+\VRef[Figure]{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
+It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafe.
+It also shows that C-incompatibilities only occur in cases that C treats unsafe.
+The conservatism of the new rule set can leave a programmer needing a recourse,
+when needing to use a dimension expression whose stability argument
+is more subtle than current-state analysis.
+\begin{comment}
+Given that the above check
+\begin{itemize}
+        \item
+        Is internal type @char[999]@ type-compatible with internal type @char[n]@?
+\end{itemize}
+answers false, discussion turns to how I got the \CFA compiler to produce this answer.
+In its preexisting form, the type system had a buggy approximation of the C rules.
+To implement the new \CFA rules, I added one further step.
+\begin{itemize}
+        \item
+                Is @999@ compatible with @n@?
+\end{itemize}
+This question applies to a pair of expressions, where the earlier question applies to types.
+An expression-compatibility question is a new addition to the \CFA compiler, and occurs in the context of dimension expressions, and possibly enumerations assigns, which must be unique.
+% TODO: ensure these compiler implementation matters are treated under \CFA compiler background: type unification, cost calculation, GenPoly.
+The relevant technical component of the \CFA compiler is the standard type-unification within the type resolver.
+\begin{cfa}
+example
+\end{cfa}
+I added rules for continuing this unification into expressions that occur within types.
+It is still fundamentally doing \emph{type} unification because it is participating in binding type variables, and not participating in binding any variables that stand in for expression fragments (for there is no such sort of variable in \CFA's analysis.)
+An unfortunate fact about the \CFA compiler's preexisting implementation is that type unification suffers from two forms of duplication.
+In detail, the first duplication has (many of) the unification rules stated twice.
+As a result, my additions for dimension expressions are stated twice.
+The extra statement of the rules occurs in the @GenPoly@ module, where concrete types like @array( int, 5 )@\footnote{
+        Again, the presentation is simplified
+        by leaving the \lstinline{array} macro unexpanded.}
+are lowered into corresponding C types @struct __conc_array_1234@ (the suffix being a generated index).
+In this case, the struct's definition contains fields that hardcode the argument values of @float@ and @5@.
+The next time an @array( -, - )@ concrete instance is encountered, it checks if the previous @struct __conc_array_1234@ is suitable for it.
+Yes, for another occurrence of @array( int, 5 )@;
+no, for examples like @array( int, 42 )@ or @array( rational(int), 5 )@.
+In the first example, it must reject the reuse hypothesis for a dimension-@5@ and a dimension-@42@ instance.
+The second duplication has unification (proper) being invoked at two stages of expression resolution.
+As a result, my added rule set needs to handle more cases than the preceding discussion motivates.
+In the program
+\begin{cfa}
+void @f@( double ); // overload
+forall( T & ) void @f@( T & ); // overload
+void g( int n ) {
+        array( float, n + 1 ) x;
+        f(x);   // overloaded
+}
+\end{cfa}
+when resolving a function call to @g@, the first unification stage compares the type @T@ of the parameter with @array( float, n + 1 )@, of the argument.
+\PAB{TODO: finish.}
+The actual rules for comparing two dimension expressions are conservative.
+To answer, ``yes, consider this pair of expressions to be matching,''
+is to imply, ``all else being equal, allow an array with length calculated by $e_1$
+to be passed to a function expecting a length-$e_2$ array.''\footnote{
+        TODO: Deal with directionality, that I'm doing exact-match, no ``at least as long as,'' no subtyping.
+        Should it be an earlier scoping principle?  Feels like it should matter in more places than here.}
+So, a ``yes'' answer must represent a guarantee that both expressions evaluate the
+same result, while a ``no'' can tolerate ``they might, but we're not sure'',
+provided that practical recourses are available
+to let programmers express better knowledge.
+The new rule-set in the current release is, in fact, extremely conservative.
+I chose to keep things simple,
+and allow future needs to drive adding additional complexity, within the new framework.
+For starters, the original motivating example's rejection is not based on knowledge that the @xp@ length of (the literal) 999 is value-unequal to the (obvious) runtime value of the variable @n@, which is the @x@ length.
+Rather, the analysis assumes a variable's value can be anything, and so there can be no guarantee that its value is 999.
+So, a variable and a literal can never match.
+TODO: Discuss the interaction of this dimension hoisting with the challenge of extra unification for cost calculation
+\end{comment}
+The conservatism of the new rule set can leave a programmer needing a recourse, when needing to use a dimension expression whose stability argument is more subtle than current-state analysis.
 This recourse is to declare an explicit constant for the dimension value.
+Consider these two dimension expressions,
+whose reuses are rejected by the blunt current-state rules:
+\begin{cfa}
+void f( int & nr, const int nv ) {
+        float x[nr];
+        float (*xp)[nr] = &x;   // reject: nr varying (no references)
+        float y[nv + 1];
+        float (*yp)[nv + 1] = &y;   // reject: ?+? unpredictable (no functions)
+Consider these two dimension expressions, whose uses are rejected by the blunt current-state rules:
+\begin{cfa}
+void f( int @&@ nr, @const@ int nv ) {
+        float x[@nr@];
+        float (*xp)[@nr@] = &x;   // reject: nr varying (no references)
+        float y[@nv + 1@];
+        float (*yp)[@nv + 1@] = &y;   // reject: ?+? unpredictable (no functions)
+}
 \end{cfa}
 Yet, both dimension expressions are reused safely.
+The @nr@ reference is never written, not volatile
+and control does not leave the function between the uses.
+The name @?+?@ resolves to a function that is quite predictable.
+Here, the programmer can add the constant declarations (cast does not work):
+The @nr@ reference is never written, not volatile meaning no implicit code (load) between declarations, and control does not leave the function between the uses.
+As well, the build-in @?+?@ function is predictable.
+To make these cases work, the programmer must add the follow constant declarations (cast does not work):
 \begin{cfa}
 void f( int & nr, const int nv ) {
 …
 achieved by adding a superfluous ``snapshot it as of now'' directive.
 The snapshotting trick is also used by the translation, though to achieve a different outcome.
+The snapshot trick is also used by the \CFA translation, though to achieve a different outcome.
 Rather obviously, every array must be subscriptable, even a bizarre one:
 \begin{cfa}
+array( float, rand(10) ) x;
+x[0];  // 10% chance of bound-check failure
+\end{cfa}
+Less obvious is that the mechanism of subscripting is a function call,
+which must communicate length accurately.
+The bound-check above (callee logic) must use the actual allocated length of @x@,
+without mistakenly reevaluating the dimension expression, @rand(10)@.
+array( float, @rand(10)@ ) x;
+x[@0@];  // 10% chance of bound-check failure
+\end{cfa}
+Less obvious is that the mechanism of subscripting is a function call, which must communicate length accurately.
+The bound-check above (callee logic) must use the actual allocated length of @x@, without mistakenly reevaluating the dimension expression, @rand(10)@.
 Adjusting the example to make the function's use of length more explicit:
 \begin{cfa}
 forall ( T * )
 void f( T * x ) { sout | sizeof(*x); }
+forall( T * )
+void f( T * x ) { sout | sizeof( *x ); }
 float x[ rand(10) ];
 f( x );
 …
 void f( size_t __sizeof_T, void * x ) { sout | __sizeof_T; }
 \end{cfa}
 the translation must call the dimension argument twice:
+the translation calls the dimension argument twice:
 \begin{cfa}
 float x[ rand(10) ];
 f( rand(10), &x );
 \end{cfa}
 Rather, the translation is:
+The correct form is:
 \begin{cfa}
 size_t __dim_x = rand(10);
 …
 f( __dim_x, &x );
 \end{cfa}
 The occurrence of this dimension hoisting during translation was in the preexisting \CFA compiler.
 But its cases were buggy, particularly with determining, ``Can hoisting the expression be skipped here?'', for skipping this hoisting is clearly desirable in some cases.
 For example, when the programmer has already done so manually. \PAB{I don't know what this means.}
+Dimension hoisting already existed in the \CFA compiler.
+But its was buggy, particularly with determining, ``Can hoisting the expression be skipped here?'', for skipping this hoisting is clearly desirable in some cases.
+For example, when a programmer has already hoisted to perform an optimiation to prelude duplicate code (expression) and/or expression evaluation.
 In the new implementation, these cases are correct, harmonized with the accept/reject criteria.
-TODO: Discuss the interaction of this dimension hoisting with the challenge of extra unification for cost calculation
 …
 A multidimensional array implementation has three relevant levels of abstraction, from highest to lowest, where the array occupies \emph{contiguous memory}.
 \begin{enumerate}
+\begin{enumerate}[leftmargin=*]
 \item
 Flexible-stride memory:
 …
 Preexisting \CFA mechanisms achieve this requirement, but with poor performance.
 Furthermore, advanced array users need an exception to the basic mechanism, which does not occur with other aggregates.
 Hence, arrays introduce subleties in supporting an element's lifecycle.
+Hence, arrays introduce subtleties in supporting an element's lifecycle.
 The preexisting \CFA support for contained-element lifecycle is based on recursive occurrences of the object-type (@otype@) pseudo-trait.
 …
 The @worker@ type is designed this way to work with the threading system.
 A thread type forks a thread at the end of each constructor and joins with it at the start of each destructor.
 But a @worker@ cannot begin its forked-thead work without knowing its @id@.
+But a @worker@ cannot begin its forked-thread work without knowing its @id@.
 Therefore, there is a conflict between the implicit actions of the builtin @thread@ type and a user's desire to defer these actions.
 …
 The \CFA array and the field of ``array language'' comparators all leverage dependent types to improve on the expressiveness over C and Java, accommodating examples such as:
 \begin{itemize}
+\begin{itemize}[leftmargin=*]
 \item a \emph{zip}-style operation that consumes two arrays of equal length
 \item a \emph{map}-style operation whose produced length matches the consumed length
 …
 The details in this presentation aren't meant to be taken too precisely as suggestions for how it should look in \CFA.
 But the example shows these abilities:
 \begin{itemize}
+\begin{itemize}[leftmargin=*]
 \item a built-in way (the @is_enum@ trait) for a generic routine to require enumeration-like information about its instantiating type
 \item an implicit implementation of the trait whenever a user-written enum occurs (@weekday@'s declaration implies @is_enum@)

Note: See TracChangeset for help on using the changeset viewer.

Context Navigation

Changeset 579427b for doc/theses/mike_brooks_MMath/array.tex

Legend:

doc/theses/mike_brooks_MMath/array.tex

Download in other formats: