Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userPure Tensor Program Rewriting via Access Patterns (Representation Pearl)
73
0
0.0
(
0
)
Added by
Gus Henry Smith
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Tensor kernels in machine learning (ML) often correspond to pure mathematical expressions, making term rewriting an attractive strategy for optimization and mapping to specialized hardware accelerators. However, existing ML intermediate representations (IRs) tend to either be textit{pure but high-level}, making low-level rewrites to hardware targets inexpressible, or textit{low-level but impure}, hampering the use of term rewriting altogether. This paper introduces Glenside, a pure IR whose core abstraction -- the textit{access pattern} -- enables low-level, layout-aware, hardware-centric program rewrites. We demonstrate how term rewriting in Glenside can be used to map program fragments to hardware accelerator invocations and automatically discover classic data layout transformations like texttt{im2col}. Glenside establishes a new foundation for exploring further term rewriting techniques in optimizing low-level tensor programs.
rate research
Read More
This volume contains the formal proceedings of the 5th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018), held on 8th of Juli 2018 in Oxford, United Kingdom, and affiliated with FLoC 2018 and FSCD 2018. Scope of WPTE: Rewriting techniques are of great help for studying correctness of program transformations, translations and evaluation, and the aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally-based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area. Topics in the scope of WPTE include the correctness of program transformations, optimisations and translations; program transformations for proving termination, confluence and other properties; correctness of evaluation strategies; operational semantics of programs, operationally-based program equivalences such as contextual equivalences and bisimulations; cost-models for reasoning about the optimizing power of transformations and the costs of evaluation; program transformations for verification and theorem proving purposes; translation, simulation, equivalence of programs with different formalisms, and evaluation strategies; program transformations for applying rewriting techniques to programs in specific programming languages; program transformations for program
Separation logic adds two connectives to assertion languages: separating conjunction * (star) and its adjoint, separating implication -* (magic wand). Comparatively, separating implication is less widely used. This paper demonstrates that by using magic wand to express frames that relate mutable local portions of data structures to global portions, we can exploit its power while proofs are still easily understandable. Many useful separation logic theorems about partial data structures can now be proved by simple automated tactics, which were usually proved by induction. This magic-wand-as-frame technique is especially useful when formalizing the proofs by a high order logic. We verify binary search tree insert in Coq as an example to demonstrate this proof technique.
Big Data query systems represent data in a columnar format for fast, selective access, and in some cases (e.g. Apache Drill), perform calculations directly on the columnar data without row materialization, avoiding runtime costs. However, many analysis procedures cannot be easily or efficiently expressed as SQL. In High Energy Physics, the majority of data processing requires nested loops with complex dependencies. When faced with tasks like these, the conventional approach is to convert the columnar data back into an object form, usually with a performance price. This paper describes a new technique to transform procedural code so that it operates on hierarchically nested, columnar data natively, without row materialization. It can be viewed as a compiler pass on the typed abstract syntax tree, rewriting references to objects as columnar array lookups. We will also present performance comparisons between transformed code and conventional object-oriented code in a High Energy Physics context.
We present a type system for strategy languages that express program transformations as compositions of rewrite rules. Our row-polymorphic type system assists compiler engineers to write correct strategies by statically rejecting non meaningful compositions of rewrites that otherwise would fail during rewriting at runtime. Furthermore, our type system enables reasoning about how rewriting transforms the shape of the computational program. We present a formalization of our language at its type system and demonstrate its practical use for expressing compiler optimization strategies. Our type system builds the foundation for many interesting future applications, including verifying the correctness of program transformations and synthesizing program transformations from specifications encoded as types.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
