Changeset 8d76f2b for doc/theses/mike_brooks_MMath
- Timestamp:
- Apr 11, 2022, 1:02:54 PM (3 years ago)
- Branches:
- ADT, ast-experimental, enum, master, pthread-emulation, qualifiedEnum
- Children:
- 13888c0, 437b8b5
- Parents:
- a08443b
- Location:
- doc/theses/mike_brooks_MMath
- Files:
-
- 3 added
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
doc/theses/mike_brooks_MMath/array.tex
ra08443b r8d76f2b 156 156 enq( N, S, arpk(N', S', E_i', E_b), E_b ) & = & arpk( N', S', enq(N, S, E_i', E_b), E_b ) 157 157 \end{eqnarray*} 158 158 159 160 \section{Bound checks, added and removed} 161 162 \CFA array subscripting is protected with runtime bound checks. Having dependent typing causes the opimizer to remove more of these bound checks than it would without them. This section provides a demonstration of the effect. 163 164 The experiment compares the \CFA array system with the padded-room system [todo:xref] most typically exemplified by Java arrays, but also reflected in the C++ pattern where restricted vector usage models a checked array. The essential feature of this padded-room system is the one-to-one correspondence between array instances and the symbolic bounds on which dynamic checks are based. The experiment compares with the C++ version to keep access to generated assembly code simple. 165 166 As a control case, a simple loop (with no reused dimension sizes) is seen to get the same optimization treatment in both the \CFA and C++ versions. When the programmer treats the array's bound correctly (making the subscript ``obviously fine''), no dynamic bound check is observed in the program's optimized assembly code. But when the bounds are adjusted, such that the subscript is possibly invalid, the bound check appears in the optimized assemly, ready to catch an occurrence the mistake. 167 168 TODO: paste source and assemby codes 169 170 Incorporating reuse among dimension sizes is seen to give \CFA an advantage at being optimized. The case is naive matrix multiplication over a row-major encoding. 171 172 TODO: paste source codes 173 174 175 176 177 178 \section{Comparison with other arrays} 179 180 \CFA's array is the first lightweight application of dependently-typed bound tracking to an extension of C. Other extensions of C that apply dependently-typed bound tracking are heavyweight, in that the bound tracking is part of a linearly typed ownership system that further helps guarantee statically the validity of every pointer deference. These systems, therefore, ask the programmer to convince the typechecker that every pointer dereference is valid. \CFA imposes the lighter-weight obligation, with the more limited guarantee, that initially-declared bounds are respected thereafter. 181 182 \CFA's array is also the first extension of C to use its tracked bounds to generate the pointer arithmetic implied by advanced allocation patterns. Other bound-tracked extensions of C either forbid certain C patterns entirely, or address the problem of \emph{verifying} that the user's provided pointer arithmetic is self-consistent. The \CFA array, applied to accordion structures [TOD: cross-reference] \emph{implies} the necessary pointer arithmetic, generated automatically, and not appearing at all in a user's program. 183 184 \subsction{Safety in a padded room} 185 186 Java's array [todo:cite] is a straightforward example of assuring safety against undefined behaviour, at a cost of expressiveness for more applied properties. Consider the array parameter declarations in: 187 188 \begin{tabular}{rl} 189 C & @void f( size_t n, size_t m, float a[n][m] );@ \\ 190 Java & @void f( float[][] a );@ 191 \end{tabular} 192 193 Java's safety against undefined behaviour assures the callee that, if @a@ is non-null, then @a.length@ is a valid access (say, evaluating to the number $\ell$) and if @i@ is in $[0, \ell)$ then @a[i]@ is a valid access. If a value of @i@ outside this range is used, a runtime error is guaranteed. In these respects, C offers no guarantess at all. Notably, the suggestion that @n@ is the intended size of the first dimension of @a@ is documentation only. Indeed, many might prefer the technically equivalent declarations @float a[][m]@ or @float (*a)[m]@ as emphasizing the ``no guarantees'' nature of an infrequently used language feature, over using the opportunity to explain a programmer intention. Moreover, even if @a[0][0]@ is valid for the purpose intended, C's basic infamous feature is the possibility of an @i@, such that @a[i][0]@ is not valid for the same purpose, and yet, its evaluation does not produce an error. 194 195 Java's lack of expressiveness for more applied properties means these outcomes are possible: 196 \begin{itemize} 197 \item @a[0][17]@ and @a[2][17]@ are valid accesses, yet @a[1][17]@ is a runtime error, because @a[1]@ is a null pointer 198 \item the same observation, now because @a[1]@ refers to an array of length 5 199 \item execution times vary, because the @float@ values within @a@ are sometimes stored nearly contiguously, and other times, not at all 200 \end{itemize} 201 C's array has none of these limitations, nor do any of the ``array language'' comparators discussed in this section. 202 203 This Java level of safety and expressiveness is also exemplified in the C family, with the commonly given advice [todo:cite example], for C++ programmers to use @std::vector@ in place of the C++ language's array, which is essentially the C array. The advice is that, while a vector is also more powerful (and quirky) than an arry, its capabilities include options to preallocate with an upfront size, to use an available bound-checked accessor (@a.at(i)@ in place of @a[i]@), to avoid using @push_back@, and to use a vector of vectors. Used with these restrictions, out-of-bound accesses are stopped, and in-bound accesses never exercise the vector's ability to grow, which is to say, they never make the program slow to reallocate and copy, and they never invalidate the program's other references to the contained values. Allowing this scheme the same referential integrity assumption that \CFA enjoys [todo:xref], this scheme matches Java's safety and expressiveness exactly. [TODO: decide about going deeper; some of the Java expressiveness concerns have mitigations, up to even more tradeoffs.] 204 205 \subsection{Levels of dependently typed arrays} 206 207 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: 208 \begin{itemize} 209 \item a \emph{zip}-style operation that consumes two arrays of equal length 210 \item a \emph{map}-style operation whose produced length matches the consumed length 211 \item a formulation of matrix multiplication, where the two operands must agree on a middle dimension, and where the result dimensions match the operands' outer dimensions 212 \end{itemize} 213 Across this field, this expressiveness is not just an avaiable place to document such assumption, but these requirements are strongly guaranteed by default, with varying levels of statically/dynamically checked and ability to opt out. Along the way, the \CFA array also closes the safety gap (with respect to bounds) that Java has over C. 214 215 216 217 Dependent type systems, considered for the purpose of bound-tracking, can be full-strength or restricted. In a full-strength dependent type system, a type can encode an arbitrarily complex predicate, with bound-tracking being an easy example. The tradeoff of this expressiveness is complexity in the checker, even typically, a potential for its nontermination. In a restricted dependent type system (purposed for bound tracking), the goal is to check helpful properties, while keeping the checker well-behaved; the other restricted checkers surveyed here, including \CFA's, always terminate. [TODO: clarify how even Idris type checking terminates] 218 219 Idris is a current, general-purpose dependently typed programming language. Length checking is a common benchmark for full dependent type stystems. Here, the capability being considered is to track lengths that adjust during the execution of a program, such as when an \emph{add} operation produces a collection one element longer than the one on which it started. [todo: finish explaining what Data.Vect is and then the essence of the comparison] 220 221 POINTS: 222 here is how our basic checks look (on a system that deosn't have to compromise); 223 it can also do these other cool checks, but watch how I can mess with its conservativeness and termination 224 225 Two current, state-of-the-art array languages, Dex\cite{arr:dex:long} and Futhark\cite{arr:futhark:tytheory}, offer offer novel contributions concerning similar, restricted dependent types for tracking array length. Unlike \CFA, both are garbage-collected functional languages. Because they are garbage-collected, referential integrity is built-in, meaning that the heavyweight analysis, that \CFA aims to avoid, is unnecessary. So, like \CFA, the checking in question is a leightweight bounds-only analysis. Like \CFA, their checks that are conservatively limited by forbidding arithmetic in the depended-upon expression. 226 227 228 229 The Futhark work discusses the working language's connection to a lambda calculus, with typing rules and a safety theorem proven in reference to an operational semantics. There is a particular emphasis on an existential type, enabling callee-determined return shapes. 230 231 Dex uses a novel conception of size, embedding its quantitative information completely into an ordinary type. 232 233 Futhark and full-strength dependently typed lanaguages treat array sizes are ordinary values. Futhark restricts these expressions syntactically to variables and constants, while a full-strength dependent system does not. 234 235 CFA's hybrid presentation, @forall( [N] )@, has @N@ belonging to the type system, yet has no instances. Belonging to the type system means it is inferred at a call site and communicated implicitly, like in Dex and unlike in Futhark. Having no instances means there is no type for a variable @i@ that constrains @i@ to be in the range for @N@, unlike Dex, [TODO: verify], but like Futhark. 236 237 \subsection{Static safety in C extensions} 238 239 240 \section{Future Work} 241 242 \subsection{Declaration syntax} 243 244 \subsection{Range slicing} 245 246 \subsection{With a module system} 247 248 \subsection{With described enumerations} 249 250 A project in \CFA's current portfolio will improve enumerations. In the incumbent state, \CFA has C's enumerations, unmodified. I will not discuss the core of this project, which has a tall mission already, to improve type safety, maintain appropriate C compatibility and offer more flexibility about storage use. It also has a candidate stretch goal, to adapt \CFA's @forall@ generic system to communicate generalized enumerations: 251 \begin{lstlisting} 252 forall( T | is_enum(T) ) 253 void show_in_context( T val ) { 254 for( T i ) { 255 string decorator = ""; 256 if ( i == val-1 ) decorator = "< ready"; 257 if ( i == val ) decorator = "< go" ; 258 sout | i | decorator; 259 } 260 } 261 enum weekday { mon, tue, wed = 500, thu, fri }; 262 show_in_context( wed ); 263 \end{lstlisting} 264 with output 265 \begin{lstlisting} 266 mon 267 tue < ready 268 wed < go 269 thu 270 fri 271 \end{lstlisting} 272 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: 273 \begin{itemize} 274 \item a built-in way (the @is_enum@ trait) for a generic routine to require enumeration-like information about its instantiating type 275 \item an implicit implementation of the trait whenever a user-written enum occurs (@weekday@'s declaration implies @is_enum@) 276 \item a total order over the enumeration constants, with predecessor/successor (@val-1@) available, and valid across gaps in values (@tue == 1 && wed == 500 && tue == wed - 1@) 277 \item a provision for looping (the @for@ form used) over the values of the type. 278 \end{itemize} 279 280 If \CFA gets such a system for describing the list of values in a type, then \CFA arrays are poised to move from the Futhark level of expressiveness, up to the Dex level. 281 282 [TODO: indroduce Ada in the comparators] 283 284 In Ada and Dex, an array is conceived as a function whose domain must satisfy only certain structural assumptions, while in C, C++, Java, Futhark and \CFA today, the domain is a prefix of the natural numbers. The generality has obvious aesthetic benefits for programmers working on scheduling resources to weekdays, and for programmers who prefer to count from an initial number of their own choosing. 285 286 This change of perspective also lets us remove ubiquitous dynamic bound checks. [TODO: xref] discusses how automatically inserted bound checks can often be otimized away. But this approach is unsatisfying to a programmer who believes she has written code in which dynamic checks are unnecessary, but now seeks confirmation. To remove the ubiquitious dynamic checking is to say that an ordinary subscript operation is only valid when it can be statically verified to be in-bound (and so the ordinary subscript is not dynamically checked), and an explicit dynamic check is available when the static criterion is impractical to meet. 287 288 [TODO, fix confusion: Idris has this arrangement of checks, but still the natural numbers as the domain.] 289 290 The structural assumptions required for the domain of an array in Dex are given by the trait (there, ``interface'') @Ix@, which says that the parameter @n@ is a type (which could take an argument like @weekday@) that provides two-way conversion with the integers and a report on the number of values. Dex's @Ix@ is analogous the @is_enum@ proposed for \CFA above. 291 \begin{lstlisting} 292 interface Ix n 293 get_size n : Unit -> Int 294 ordinal : n -> Int 295 unsafe_from_ordinal n : Int -> n 296 \end{lstlisting} 297 298 Dex uses this foundation of a trait (as an array type's domain) to achieve polymorphism over shapes. This flavour of polymorphism lets a function be generic over how many (and the order of) dimensions a caller uses when interacting with arrays communicated with this funciton. Dex's example is a routine that calculates pointwise differences between two samples. Done with shape polymorphism, one function body is equally applicable to a pair of single-dimensional audio clips (giving a single-dimensional result) and a pair of two-dimensional photographs (giving a two-dimensional result). In both cases, but with respectively dimensoned interpretations of ``size,'' this function requries the argument sizes to match, and it produces a result of the that size. 299 300 The polymorphism plays out with the pointwise-difference routine advertizing a single-dimensional interface whose domain type is generic. In the audio instantiation, the duration-of-clip type argument is used for the domain. In the photograph instantiation, it's the tuple-type of $ \langle \mathrm{img\_wd}, \mathrm{img\_ht} \rangle $. This use of a tuple-as-index is made possible by the built-in rule for implementing @Ix@ on a pair, given @Ix@ implementations for its elements 301 \begin{lstlisting} 302 instance {a b} [Ix a, Ix b] Ix (a & b) 303 get_size = \(). size a * size b 304 ordinal = \(i, j). (ordinal i * size b) + ordinal j 305 unsafe_from_ordinal = \o. 306 bs = size b 307 (unsafe_from_ordinal a (idiv o bs), unsafe_from_ordinal b (rem o bs)) 308 \end{lstlisting} 309 and by a user-provided adapter expression at the call site that shows how to indexing with a tuple is backed by indexing each dimension at a time 310 \begin{lstlisting} 311 img_trans :: (img_wd,img_ht)=>Real 312 img_trans.(i,j) = img.i.j 313 result = pairwise img_trans 314 \end{lstlisting} 315 [TODO: cite as simplification of example from https://openreview.net/pdf?id=rJxd7vsWPS section 4] 316 317 In the case of adapting this pattern to \CFA, my current work provides an adapter from ``successively subscripted'' to ``subscripted by tuple,'' so it is likely that generalizing my adapter beyond ``subscripted by @ptrdiff_t@'' is sufficient to make a user-provided adapter unnecessary. 318 319 \subsection{Retire pointer arithmetic} -
doc/theses/mike_brooks_MMath/uw-ethesis.bib
ra08443b r8d76f2b 2 2 % For use with BibTeX 3 3 4 % -------------------------------------------------- 5 % Cforall 6 @misc{cfa:frontpage, 7 url = {https://cforall.uwaterloo.ca/} 8 } 9 @article{cfa:typesystem, 10 author = {Aaron Moss and Robert Schluntz and Peter A. Buhr}, 11 title = {{\CFA} : Adding modern programming language features to {C}}, 12 journal = {Softw. Pract. Exp.}, 13 volume = {48}, 14 number = {12}, 15 pages = {2111--2146}, 16 year = {2018}, 17 url = {https://doi.org/10.1002/spe.2624}, 18 doi = {10.1002/spe.2624}, 19 timestamp = {Thu, 09 Apr 2020 17:14:14 +0200}, 20 biburl = {https://dblp.org/rec/journals/spe/MossSB18.bib}, 21 bibsource = {dblp computer science bibliography, https://dblp.org} 22 } 23 24 25 % -------------------------------------------------- 26 % Array prior work 27 28 @inproceedings{arr:futhark:tytheory, 29 author = {Henriksen, Troels and Elsman, Martin}, 30 title = {Towards Size-Dependent Types for Array Programming}, 31 year = {2021}, 32 isbn = {9781450384667}, 33 publisher = {Association for Computing Machinery}, 34 address = {New York, NY, USA}, 35 url = {https://doi.org/10.1145/3460944.3464310}, 36 doi = {10.1145/3460944.3464310}, 37 abstract = {We present a type system for expressing size constraints on array types in an ML-style type system. The goal is to detect shape mismatches at compile-time, while being simpler than full dependent types. The main restrictions is that the only terms that can occur in types are array sizes, and syntactically they must be variables or constants. For those programs where this is not sufficient, we support a form of existential types, with the type system automatically managing the requisite book-keeping. We formalise a large subset of the type system in a small core language, which we prove sound. We also present an integration of the type system in the high-performance parallel functional language Futhark, and show on a collection of 44 representative programs that the restrictions in the type system are not too problematic in practice.}, 38 booktitle = {Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming}, 39 pages = {1–14}, 40 numpages = {14}, 41 keywords = {functional programming, parallel programming, type systems}, 42 location = {Virtual, Canada}, 43 series = {ARRAY 2021} 44 } 45 46 @article{arr:dex:long, 47 author = {Adam Paszke and 48 Daniel D. Johnson and 49 David Duvenaud and 50 Dimitrios Vytiniotis and 51 Alexey Radul and 52 Matthew J. Johnson and 53 Jonathan Ragan{-}Kelley and 54 Dougal Maclaurin}, 55 title = {Getting to the Point. Index Sets and Parallelism-Preserving Autodiff 56 for Pointful Array Programming}, 57 journal = {CoRR}, 58 volume = {abs/2104.05372}, 59 year = {2021}, 60 url = {https://arxiv.org/abs/2104.05372}, 61 eprinttype = {arXiv}, 62 eprint = {2104.05372}, 63 timestamp = {Mon, 25 Oct 2021 07:55:47 +0200}, 64 biburl = {https://dblp.org/rec/journals/corr/abs-2104-05372.bib}, 65 bibsource = {dblp computer science bibliography, https://dblp.org} 66 }
Note: See TracChangeset
for help on using the changeset viewer.