Changeset b4c6e10

Timestamp:

Dec 7, 2024, 6:47:05 PM (9 months ago)

Author:

Peter A. Buhr <pabuhr@…>

Branches:

master

Children:

0b98381

Parents:

9861ef2

Message:

thesis proofreading

Location:

doc

Files:

• bibliography/pl.bib (modified) (1 diff)
• theses/fangren_yu_MMath/content1.tex (modified) (1 diff)
• theses/fangren_yu_MMath/content2.tex (modified) (1 diff)
• theses/fangren_yu_MMath/intro.tex (modified) (13 diffs)

doc/bibliography/pl.bib

@@ -6305 +6305 @@
 }
 
+@techreport{Yu20,
+    keywords    = {Cforall, cfa-cc, transpiler},
+    contributer = {pabuhr@plg},
+    title       = {Optimization of \textsf{C}$\mathbf{\forall}$ Compiler with Case Studies},
+    author      = {Fangren Yu},
+    institution = {School of Computer Science},
+    address     = {University of Waterloo, Waterloo, Ontario, Canada},
+    month       = jan,
+    year        = {2021},
+    note        = {\url{https://cforall.uwaterloo.ca/doc/Fangren_Yu_Report_F20.pdf}},
+}
+
 @article{Ford82,
     keywords    = {},

doc/theses/fangren_yu_MMath/content1.tex

@@ -674 +674 @@
 In addition, a semi-non-compatible change is made so that Plan-9 syntax means a forward declaration in a nested type.
 Since the Plan-9 extension is not part of C and rarely used, this change has minimal impact.
-Hence, all Plan-9 semantics are denoted by the @inline@ qualifier, which good ``eye-candy'' when reading a structure definition to spot Plan-9 definitions.
+Hence, all Plan-9 semantics are denoted by the @inline@ qualifier, which is good ``eye-candy'' when reading a structure definition to spot Plan-9 definitions.
 Finally, the following code shows the value and pointer polymorphism.
 \begin{cfa}

doc/theses/fangren_yu_MMath/content2.tex

@@ -2 +2 @@
 \label{c:content2}
 
-\CFA's type system is powerful but fairly complicated, which leads to higher compilation cost.
-The compiler needs to analyze each expression with many possible forms of overloading.
-Variables can be overloaded in \CFA, and functions can be overloaded by the argument types as well as the return types.
-Combined with the polymorphism introduced by forall clauses and generic types, the complexity of expression analysis can go up very quickly.
-Designing a rule set that behaves mostly as expected, and implementing it as an efficient algorithm for actual use, are both very challenging tasks.
-As the \CFA translator's performance improves to a level that can compile a mid-sized program in a reasonable amount of time, the development of \CFA's standard library also speeds up and many new features utilizing the expressiveness of \CFA's type system has been implemented, such as generic container types similar to those in \CC's standard template library.
-During the process of development, many weaknesses and design flaws of \CFA type system have been discovered.
-Some of those problems arise from the newly introduced language features described in the previous chapter, and fixing those unexpected interactions with the type system is especially difficult.
-This chapter describes the type resolution rules currently in use and some major problems that have been identified.
-Not all of those problems have got solutions yet, because fixing them may require redesigning parts of the \CFA language at a larger scale.
-
-
-\section{Expression Cost Model}
-
-\CFA has been using an expression cost model to resolve ambiguity of overloaded expressions from the very beginning.
-Since most operators can be overloaded in \CFA (excluding a few operators that have special semantics, such as the comma operator, and the short-circuit logical operators \&\& and ||, which require the operands to be evaluated in order), they are treated the same way as other function calls and the same rules for overload resolution must apply to them as well.
-
-In \CFA, candidates of an overloaded expression are ranked by numerical cost elements, that accounts for the type conversions needed from the argument type to the corresponding declared function parameter type, as well as the polymorphic types and restrictions introduces by the forall clause.
+The \CFA's type-system provides expressive polymorphism: variables can be overloaded, functions can be overloaded by argument and return types, tuple types, generic (polymorphic) functions and types (aggregates) can have multiple type parameters with associated restrictions, and C's multiple implicit type-conversions must be respected.
+This generality leads to internal complexity and correspondingly higher compilation cost.
+The reason is that the type resolver must analyze \emph{each} component of an expression with many possible forms of overloading, type restrictions, and conversions.
+Designing a ruleset that behaves as expected, \ie matches with C programmer expectations, and implementing an efficient algorithm is a very challenging task.
+
+My first work on the \CFA type-system was as a co-op student.
+At that time, compiling a medium-sized \CFA program using advanced polymorphism took multiple minutes (5+ minutes)~\cite[\S~5]{Yu20}.
+After finding and fixing the following resolution problems:
+\begin{enumerate}[itemsep=0pt]
+\item
+new AST data structure
+\item
+special symbol table and argument-dependent lookup
+\item
+late assertion-satisfaction
+\item
+revised function-type representation
+\item
+skip pruning on expressions for function types
+\end{enumerate}
+\VRef[Table]{t:SelectedFileByCompilerBuild} shows the improvement of selected tests with accumulated reductions in compile time across each of the 5 fixes.
+The large reduction in compilation times, significantly improved the development of the \CFA's runtime because of its frequent compilation cycles.
+
+\begin{table}[htb]
+\centering
+\caption{Compile time of selected files by compiler build in seconds}
+\label{t:SelectedFileByCompilerBuild}
+\lstset{deletekeywords={mutex,thread}}
+\setlength{\extrarowheight}{1pt}
+\vspace*{-4pt}
+\begin{tabular}{l|r|rrrrr}
+                                & \multicolumn{1}{c|}{Original} & \multicolumn{5}{c}{Accumulative fixes}        \\
+\cline{3-7}                             
+Test case               & \multicolumn{1}{c|}{resolver} & \multicolumn{1}{c}{1} & \multicolumn{1}{c}{2} & \multicolumn{1}{c}{3} & \multicolumn{1}{c}{4} & \multicolumn{1}{c}{5} \\
+\hline
+@lib/fstream@   & 86.4  & 25.2  & 10.8  & 9.5   & 7.8   & 7.1   \\
+@lib/mutex@             & 210.4 & 77.4  & 16.7  & 15.1  & 12.6  & 11.7  \\
+@lib/vector@    & 17.2  & 8.9   & 3.1   & 2.8   & 2.4   & 2.2   \\
+@lib/stdlib@    & 16.6  & 8.3   & 3.2   & 2.9   & 2.6   & 2.4   \\
+@test/io2@              & 300.8 & 53.6  & 43.2  & 27.9  & 19.1  & 16.3  \\
+@test/thread@   & 210.9 & 73.5  & 17.0  & 15.1  & 12.6  & 11.8  \\
+\end{tabular}
+\smallskip
+\newline
+Results are average of 5 runs (3 runs if time exceeds 100 seconds)
+\end{table}
+
+Since then, many new features utilizing the expressiveness of \CFA's type system have been implemented, such as generic container types similar to those in \CC's standard template library.
+During the development of multiple \CFA programs and libraries, more weaknesses and design flaws have been discovered within the type system.
+Some of those problems arise from the newly introduced language features described in the previous chapter.
+In addition, fixing unexpected interactions within the type system has presented challenges.
+This chapter describes in detail the type-resolution rules currently in use and some major problems that have been identified.
+Not all of those problems have solutions, because fixing them may require redesigning parts of the \CFA type system at a larger scale, which correspondingly affects the language design.
+
+
+\section{Expression Cost-Model}
+
+\CFA has been using an expression cost-model to resolve ambiguity of overloaded expressions from the very beginning.
+Most \CFA operators can be overloaded in \CFA\footnote{
+Excluding the comma operator, short-circuit logical operators \lstinline{&&} and \lstinline{||} (control structures) and ternary conditional operator \lstinline{?} (control structure).
+While \CC overloads the short-circuit logical operators, the overloaded operators do not exhibit the short-circuit semantics, which is confusing.};
+hence, they are treated the same way as other function calls, and the same rules for overload resolution must apply to them as well.
+
+In \CFA, candidates of an overloaded expression are ranked by numerical cost elements, that accounts for the type conversions needed from the argument type to the corresponding declared function parameter type, as well as the polymorphic types and restrictions introduces by the @forall@ clause.
 Currently the expression cost used in \CFA has the following components, ranked from higher to lower by importance:
 \begin{enumerate}

doc/theses/fangren_yu_MMath/intro.tex

@@ -2 +2 @@
 
 This thesis is exploratory work I did to understand, fix, and extend the \CFA type-system, specifically, the type resolver used to select polymorphic types among overloaded names.
-The \CFA type-system has a number of unique features making it different from all other programming languages.
-
 Overloading allows programmers to use the most meaningful names without fear of name clashes within a program or from external sources, like include files.
 \begin{quote}
@@ -10 +8 @@
 Experience from \CC and \CFA developers is that the type system implicitly and correctly disambiguates the majority of overloaded names, \ie it is rare to get an incorrect selection or ambiguity, even among hundreds of overloaded (variables and) functions.
 In many cases, a programmer has no idea there are name clashes, as they are silently resolved, simplifying the development process.
-Depending on the language, ambiguous cases are resolved using some form of qualification and/or casting.
-
-One of the key goals in \CFA is to push the boundary on overloading, and hence, overload resolution.
+Depending on the language, any ambiguous cases are resolved using some form of qualification and/or casting.
+
+Therefore, one of the key goals in \CFA is to push the boundary on overloading, and hence, overload resolution.
+As well, \CFA follows the current trend of replacing nominal inheritance with traits.
+Together, the resulting \CFA type-system has a number of unique features making it different from all other programming languages.
 
 
@@ -22 +22 @@
 
 All computers have multiple types because computer architects optimize the hardware around a few basic types with well defined (mathematical) operations: boolean, integral, floating-point, and occasionally strings.
-A programming language and its compiler present ways to declare types that ultimately map into those provided by the underlying hardware.
-These language types are thrust upon programmers, with their syntactic and semantic rules, and resulting restrictions.
-A language type-system defines these rules and uses them to understand how an expression is to be evaluated by the hardware.
+A programming language and its compiler present ways to declare types that ultimately map into the ones provided by the underlying hardware.
+These language types are thrust upon programmers, with their syntactic and semantic rules and restrictions.
+These rules are used to transform a language expression to a hardware expression.
 Modern programming-languages allow user-defined types and generalize across multiple types using polymorphism.
 Type systems can be static, where each variable has a fixed type during execution and an expression's type is determined once at compile time, or dynamic, where each variable can change type during execution and so an expression's type is reconstructed on each evaluation.
@@ -34 +34 @@
 Virtually all programming languages overload the arithmetic operators across the basic computational types using the number and type of parameters and returns.
 Like \CC, \CFA also allows these operators to be overloaded with user-defined types.
-The syntax for operator names uses the @'?'@ character to denote a parameter, \eg unary operators: @?++@, @++?@, binary operator @?+?@.
+The syntax for operator names uses the @'?'@ character to denote a parameter, \eg unary left and right operators: @?++@ and @++?@, and binary operators @?+?@ and @?<=?@.
 Here, a user-defined type is extended with an addition operation with the same syntax as builtin types.
 \begin{cfa}
@@ -43 +43 @@
 s1 = @?+?@( s1, s2 );   $\C{// direct call}\CRT$
 \end{cfa}
-The type system examines each call size and selects the best matching overloaded function based on the number and types of arguments.
+The type system examines each call site and selects the best matching overloaded function based on the number and types of arguments.
 If there are mixed-mode operands, @2 + 3.5@, the type system, like in C/\CC, attempts (safe) conversions, converting the argument type(s) to the parameter type(s).
 Conversions are necessary because the hardware rarely supports mix-mode operations, so both operands must be the same type.
@@ -71 +71 @@
 double d = f( 3 );              $\C{// select (2)}\CRT$
 \end{cfa}
-However, if the type system looks at the return type, there is an exact match for each call, which matches with programmer intuition and expectation.
+Alternatively, if the type system looks at the return type, there is an exact match for each call, which matches with programmer intuition and expectation.
 This capability can be taken to the extreme, where there are no function parameters.
 \begin{cfa}
@@ -98 +98 @@
 }
 \end{cfa}
-It is interesting that shadow overloading is considered a normal programming-language feature with only slight software-engineering problems, but variable overloading within a scope is often considered extremely dangerous.
+It is interesting that shadow overloading is considered a normal programming-language feature with only slight software-engineering problems.
+However, variable overloading within a scope is considered extremely dangerous, without any evidence to corroborate this claim.
+Similarly, function overloading occurs silently within the global scope in \CC from @#include@ files all the time without problems.
 
 In \CFA, the type system simply treats overloaded variables as an overloaded function returning a value with no parameters.
-Hence, no significant effort is required to support this feature.
-Leveraging the return type to disambiguate is essential because variables have no parameters.
+Hence, no significant effort is required to support this feature by leveraging the return type to disambiguate as variables have no parameters.
 \begin{cfa}
 int MAX = 2147483647;   $\C[2in]{// (1); overloaded on return type}$
-double MAX = ...;               $\C{// (2); overloaded on return type}$
+long int MAX = ...;             $\C{// (2); overloaded on return type}$
+double MAX = ...;               $\C{// (3); overloaded on return type}$
 int i = MAX;                    $\C{// select (1)}$
-double d = MAX;                 $\C{// select (2)}\CRT$
-\end{cfa}
+long int i = MAX;               $\C{// select (2)}$
+double d = MAX;                 $\C{// select (3)}\CRT$
+\end{cfa}
+Hence, the name @MAX@ can replace all the C type-specific names, \eg @INT_MAX@, @LONG_MAX@, @DBL_MAX@, \etc.
+The result is a significant reduction in names to access typed constants.
+% Paraphrasing Shakespeare, ``The \emph{name} is the thing.''.
+
+
+\section{Constant Overloading}
+
+\CFA is unique in providing restricted constant overloading for the values @0@ and @1@, which have special status in C, \eg the value @0@ is both an integer and a pointer literal, so its meaning depends on context.
+In addition, several operations are defined in terms of values @0@ and @1@, \eg:
+\begin{cfa}
+if (x) x++                                                                      $\C{// if (x != 0) x += 1;}$
+\end{cfa}
+Every @if@ and iteration statement in C compares the condition with @0@, and every increment and decrement operator is semantically equivalent to adding or subtracting the value @1@ and storing the result.
+These two constants are given types @zero_t@ and @one_t@ in \CFA, which allows overloading various operations for new types that seamlessly connect to all special @0@ and @1@ contexts.
+The types @zero_t@ and @one_t@ have special builtin implicit conversions to the various integral types, and a conversion to pointer types for @0@, which allows standard C code involving @0@ and @1@ to work.
+\begin{cfa}
+struct S { int i, j; };
+void ?{}( S & s, zero_t ) { s.[i,j] = 0; }
+void ?{}( S & s, one_t ) { s.[i,j] = 1; }
+int ?!=?( S s, zero_t ) { return s.i != 0 && s.j != 0; }
+S ?+=?( S & s, one_t ) { s.i++; s.j++; return s; }
+S ?-=?( S & s, one_t ) { s.i--; s.j--; return s; }
+S ?=?( S & dst, one_t ) { return dst.[i,j] = 1; }
+void foo() {
+        S s = @0@;
+        s = @1@;
+        if ( @s@ ) @s++@;
+}
+\end{cfa}
+Hence, type @S@ is first-class with respect to the basic types, working with all existing implicit C mechanisms.
 
 
@@ -121 +154 @@
 z = "abc";                              $\C{// assignment}$
 \end{cfa}
+For type-only, the programmer specifies the initial type, which remains fixed for the variable's lifetime in statically typed languages.
 For type-and-initialization, the specified and initialization types may not agree.
-Similarity, for assignment the current variable and expression types may not agree.
-For type-only, the programmer specifies the initial type, which remains fixed for the variable's lifetime in statically typed languages.
-In the other cases, the compiler may select the type by melding programmer and context information.
+For initialization-only, the compiler may select the type by melding programmer and context information.
 When the compiler participates in type selection, it is called \newterm{type inferencing}.
 Note, type inferencing is different from type conversion: type inferencing \emph{discovers} a variable's type before setting its value, whereas conversion has two typed values and performs a (possibly lossy) action to convert one value to the type of the other variable.
+Finally, for assignment, the current variable and expression types may not agree.
 
 One of the first and powerful type-inferencing system is Hindley--Milner~\cite{Damas82}.
@@ -147 +180 @@
 \end{cfa}
 In both overloads of @f@, the type system works from the constant initializations inwards and/or outwards to determine the types of all variables and functions.
-Note, like template meta-programming, there could be a new function generated for the second @f@ depending on the types of the arguments, assuming these types are meaningful in the body of the @f@.
+Note, like template meta-programming, there could be a new function generated for the second @f@ depending on the types of the arguments, assuming these types are meaningful in the body of @f@.
 Inferring type constraints, by analysing the body of @f@ is possible, and these constraints must be satisfied at each call site by the argument types;
 in this case, parametric polymorphism can allow separate compilation.
 In languages with type inferencing, there is often limited overloading to reduce the search space, which introduces the naming problem.
-Return-type inferencing goes in the opposite direction to Hindley--Milner: knowing the type of the result and flowing back through an expression to help select the best possible overloads, and possibly converting the constants for a best match.
-
-In simpler type inferencing systems, such as C/\CC/\CFA, there are more specific usages.
+Note, return-type inferencing goes in the opposite direction to Hindley--Milner: knowing the type of the result and flowing back through an expression to help select the best possible overloads, and possibly converting the constants for a best match.
+
+In simpler type-inferencing systems, such as C/\CC/\CFA, there are more specific usages.
 \begin{cquote}
 \setlength{\tabcolsep}{10pt}
@@ -190 +223 @@
 This issue is exaggerated with \CC templates, where type names are 100s of characters long, resulting in unreadable error messages.
 \item
-Ensuring the type of secondary variables, always matches a primary variable.
+Ensuring the type of secondary variables, always match a primary variable.
 \begin{cfa}
 int x; $\C{// primary variable}$
 typeof(x) y, z, w; $\C{// secondary variables match x's type}$
 \end{cfa}
-If the type of @x@ changes, the types of the secondary variables correspondingly update.
+If the type of @x@ changes, the type of the secondary variables correspondingly updates.
 \end{itemize}
 Note, the use of @typeof@ is more restrictive, and possibly safer, than general type-inferencing.
@@ -208 +241 @@
 \section{Type-Inferencing Issues}
 
-Each kind of type-inferencing system has its own set of issues that flow onto the programmer in the form of convenience, restrictions or confusions.
+Each kind of type-inferencing system has its own set of issues that flow onto the programmer in the form of convenience, restrictions, or confusions.
 
 A convenience is having the compiler use its overarching program knowledge to select the best type for each variable based on some notion of \emph{best}, which simplifies the programming experience.
@@ -227 +260 @@
 In Haskell, it is common for programmers to brand (type) function parameters.
 
-A confusion is large blocks of code where all declarations are @auto@.
+A confusion is large blocks of code where all declarations are @auto@, as is now common in \CC.
 As a result, understanding and changing the code becomes almost impossible.
 Types provide important clues as to the behaviour of the code, and correspondingly to correctly change or add new code.
-In these cases, a programmer is forced to re-engineer types, which is fragile, or rely on a fancy IDE that can re-engineer types.
+In these cases, a programmer is forced to re-engineer types, which is fragile, or rely on a fancy IDE that can re-engineer types for them.
 For example, given:
 \begin{cfa}
@@ -243 +276 @@
 In this situation, having the type name or its short alias is essential.
 
-\CFA's type system tries to prevent type-resolution mistakes by relying heavily on the type of the left-hand side of assignment to pinpoint the right types within an expression.
+The \CFA's type system tries to prevent type-resolution mistakes by relying heavily on the type of the left-hand side of assignment to pinpoint the right types within an expression.
 Type inferencing defeats this goal because there is no left-hand type.
 Fundamentally, type inferencing tries to magic away variable types from the programmer.
 However, this results in lazy programming with the potential for poor performance and safety concerns.
 Types are as important as control-flow in writing a good program, and should not be masked, even if it requires the programmer to think!
-A similar issue is garbage collection, where storage management is masked, resulting in poor program design and performance.
+A similar issue is garbage collection, where storage management is magicked away, often resulting in poor program design and performance.\footnote{
+There are full-time Java consultants, who are hired to find memory-management problems in large Java programs.}
 The entire area of Computer-Science data-structures is obsessed with time and space, and that obsession should continue into regular programming.
 Understanding space and time issues are an essential part of the programming craft.