Changeset 06d75931 for doc/theses

Timestamp:

Oct 26, 2024, 8:17:20 AM (14 months ago)

Author:

Peter A. Buhr <pabuhr@…>

Branches:

master

Children:

14c31eb

Parents:

3a08cb1 (diff), d031f7f (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

Location:

doc/theses/mike_brooks_MMath

Files:

• array.tex (modified) (1 diff)
• uw-ethesis.tex (modified) (1 diff)

doc/theses/mike_brooks_MMath/array.tex

@@ -502 +502 @@
 \end{itemize}
 
-TODO: summarize the C rules and add the case-comparison table
-
-TODO: Discuss Recourse
-
-TODO: Discuss dimension hoisting, which addresses the challenge of extra unification for cost calculation
+The traditional C rules are:
+\begin{itemize}
+\item
+        Reject a Statically Evaluable pair, if the expressions have two different values.
+\item
+        Otherwise, accept.
+\end{itemize}
+
+
+\newcommand{\falsealarm}{{\color{orange}\small{*}}}
+\newcommand{\allowmisuse}{{\color{red}\textbf{!}}}
+\newcommand{\cmark}{\ding{51}} % from pifont
+\newcommand{\xmark}{\ding{55}}
+\begin{figure}
+        \begin{tabular}{@{}l@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c}
+         & \multicolumn{2}{c}{\underline{Values Equal}}
+         & \multicolumn{2}{c}{\underline{Values Unequal}} 
+         & \\
+        \textbf{Case}                                & C      & \CFA                & C                      & \CFA    & Compat. \\
+        Both Statically Evaluable, Same Symbol       & Accept & Accept              &                        &         & \cmark \\
+        Both Statically Evaluable, Different Symbols & Accept & Accept              & Reject                 & Reject  & \cmark \\
+        Both Dynamic but Stable, Same Symbol         & Accept & Accept              &                        &         & \cmark \\
+        Both Dynamic but Stable, Different Symbols   & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark \\
+        Both Potentially Unstable, Same Symbol       & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark \\
+        Any other grouping, Different Symbol         & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark
+        \end{tabular}
+
+        \vspace{12pt}
+        \noindent\textbf{Legend:}
+        \begin{itemize}
+        \item
+                Each row gives the treatment of a test harness of the form
+                \begin{cfa}
+                        float x[ expr1 ];
+                        float (*xp)[ expr2 ] = &x;
+                \end{cfa}
+                where \lstinline{expr1} and \lstinline{expr2} are metavariables varying according to the row's Case.
+                Each row's claim applies to other harnesses too, including,
+                \begin{itemize}
+                \item
+                        calling a function with a paramter like \lstinline{x} and an argument of the \lstinline{xp} type,
+                \item
+                        assignment in place of initialization,
+                \item
+                        using references in place of pointers, and
+                \item
+                        for the \CFA array, calling a polymorphic function on two \lstinline{T}-typed parameters with \lstinline{&x}- and \lstinline{xp}-typed arguments.
+                \end{itemize}
+        \item
+                Each case's claim is symmetric (swapping \lstinline{expr1} with \lstinline{expr2} has no effect),
+                even though most test harnesses are asymetric.
+        \item
+                The table treats symbolic identity (Same/Different on rows)
+                apart from value eqality (Equal/Unequal on columns).
+                \begin{itemize}
+                \item
+                        The expressions \lstinline{1}, \lstinline{0+1} and \lstinline{n}
+                        (where \lstinline{n} is a variable with value 1),
+                        are all different symbols with the value 1.
+                \item
+                        The column distinction expresses ground truth about whether an omniscient analysis should accept or reject.
+                \item
+                        The row distinction expresses the simple static factors used by today's analyses.
+                \end{itemize}
+        \item
+                Accordingly, every Reject under Values Equal is a false alarm (\falsealarm),
+                while every Accept under Values Unequal is an allowed misuse (\allowmisuse).
+        \end{itemize}
+        \caption{Case comparison for array type compatibility, given pairs of dimension expressions.
+                TODO: get Peter's LaTeX help on overall appearance, probably including column spacing/centering and bullet indentation.}
+        \label{f:DimexprRuleCompare}
+\end{figure}
+
+
+Figure~\ref{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 unsafely.
+It also shows that C-incompatibilities only occur in cases that C treats unsafely.
+
+
+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: ?+? unpredicable (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.)
+The programmer here can add the constant declarations:
+\begin{cfa}
+        void f( int & nr, const int nv ) {
+                @const int nx@ = nr;
+                float x[nx];
+                float (*xp)[nx] = & x; // acept
+                @const int ny@ = nv + 1;
+                float y[ny];
+                float (*yp)[ny] = & y; // accept
+        }
+\end{cfa}
+The result is the originally intended semantics,
+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.
+Rather obviously, every array must be subscriptable, even a bizzarre 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)@.
+Adjusting the example to make the function's use of length more explicit:
+\begin{cfa}
+        forall ( T * )
+        void f( T * x ) { sout | sizeof(*x); }
+        float x[ rand(10) ];
+        f( x );
+\end{cfa}
+Considering that the partly translated function declaration is, loosely,
+\begin{cfa}
+        void f( size_t __sizeof_T, void * x ) { sout | __sizeof_T; }
+\end{cfa}
+the translated call must not go like:
+\begin{cfa}
+        float x[ rand(10) ];
+        f( rand(10), &x );
+\end{cfa}
+Rather, its actual translation is like:
+\begin{cfa}
+        size_t __dim_x = rand(10);
+        float x[ __dim_x ];
+        f( __dim_x, &x );
+\end{cfa}
+The occurrence of this dimension hoisting during translation was present in the preexisting \CFA compiler.
+But its cases were buggy, particularly with determining, ``Can hoisting be skipped here?''
+For skipping this hoisting is clearly desirable in some cases,
+not the least of which is when the programmer has already done so manually.
+My work includes getting these cases right, harmonized with the accept/reject criteria, and tested.
+
+
+
+TODO: Discuss the interaction of this dimension hoisting with the challenge of extra unification for cost calculation
 
 \section{Multidimensional Arrays}

doc/theses/mike_brooks_MMath/uw-ethesis.tex

@@ -87 +87 @@
 \usepackage{graphicx}
 \usepackage{tabularx}
+\usepackage{pifont}
 \usepackage[labelformat=simple,aboveskip=0pt,farskip=0pt,font=normalsize]{subfig}
 \renewcommand\thesubfigure{(\alph{subfigure})}