uwthesis.tex

%  ========================================================================
%  Copyright (c) 1985 The University of Washington
%
%  Licensed under the Apache License, Version 2.0 (the "License");
%  you may not use this file except in compliance with the License.
%  You may obtain a copy of the License at
%
%      http://www.apache.org/licenses/LICENSE-2.0
%
%  Unless required by applicable law or agreed to in writing, software
%  distributed under the License is distributed on an "AS IS" BASIS,
%  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
%  See the License for the specific language governing permissions and
%  limitations under the License.
%  ========================================================================
%

% Documentation for University of Washington thesis LaTeX document class
% by Jim Fox
% fox@washington.edu
%
%    Revised 2020/02/24, added \caption()[]{} option.  No ToC.
%
%    Revised for version 2015/03/03 of uwthesis.cls
%    Revised, 2016/11/22, for cleanup of sample copyright and title pages
%
%    This document is contained in a single file ONLY because
%    I wanted to be able to distribute it easily.  A real thesis ought
%    to be contained on many files (e.g., one for each chapter, at least).
%
%    To help you identify the files and sections in this large file
%    I use the string '==========' to identify new files.
%
%    To help you ignore the unusual things I do with this sample document
%    I try to use the notation
%       
%    % --- sample stuff only -----
%    special stuff for my document, but you don't need it in your thesis
%    % --- end-of-sample-stuff ---


%    Printed in twoside style now that that's allowed
%
 
\documentclass [11pt, proquest] {uwthesis}[2020/02/24]
 
%
% The following line would print the thesis in a postscript font 

\usepackage{natbib}
\def\bibpreamble{\protect\addcontentsline{toc}{chapter}{Bibliography}}

\setcounter{tocdepth}{1}  % Print the chapter and sections to the toc

\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{xspace}
\usepackage{natbib}
\usepackage{csvsimple}
\usepackage{microtype}
\usepackage{tikz}
\usepackage{tikz-qtree}
\usepackage{tabularx}
\usepackage{makecell}
\usepackage[ruled,vlined]{algorithm2e}
\usepackage{hhline}
\usepackage{subfigure}
\usepackage{listings}

\usetikzlibrary{hobby,arrows,backgrounds,calc,trees,automata}

\pgfdeclarelayer{background}
\pgfsetlayers{background,main}

\newcommand{\convexpath}[2]{
[   
    create hullnodes/.code={
        \global\edef\namelist{#1}
        \foreach [count=\counter] \nodename in \namelist {
            \global\edef\numberofnodes{\counter}
            \node at (\nodename) [draw=none,name=hullnode\counter] {};
        }
        \node at (hullnode\numberofnodes) [name=hullnode0,draw=none] {};
        \pgfmathtruncatemacro\lastnumber{\numberofnodes+1}
        \node at (hullnode1) [name=hullnode\lastnumber,draw=none] {};
    },
    create hullnodes
]
($(hullnode1)!#2!-90:(hullnode0)$)
\foreach [
    evaluate=\currentnode as \previousnode using \currentnode-1,
    evaluate=\currentnode as \nextnode using \currentnode+1
    ] \currentnode in {1,...,\numberofnodes} {
  let
    \p1 = ($(hullnode\currentnode)!#2!-90:(hullnode\previousnode)$),
    \p2 = ($(hullnode\currentnode)!#2!90:(hullnode\nextnode)$),
    \p3 = ($(\p1) - (hullnode\currentnode)$),
    \n1 = {atan2(\y3,\x3)},
    \p4 = ($(\p2) - (hullnode\currentnode)$),
    \n2 = {atan2(\y4,\x4)},
    \n{delta} = {-Mod(\n1-\n2,360)}
  in 
    {-- (\p1) arc[start angle=\n1, delta angle=\n{delta}, radius=#2] -- (\p2)}
}
-- cycle
}
\tikzset{
  leaf/.style={sibling distance=5mm}
}

% ==========   Local defs and mods
\definecolor{uwpurple}{RGB}{128,0,128}
\definecolor{darkgreen}{RGB}{0,64,0}
%\newcommand{\jln}[1]{\textcolor{uwpurple}{\textit{[{#1} --JLN]}}}
\newcommand{\jln}[1]{\textcolor{uwpurple}{}}
\newcommand{\sak}[1]{\textcolor{olive}{\textit{[{#1} --SK]}}}
\newcommand{\aba}[1]{\textcolor{darkgreen}{\textit{[{#1} --AA]}}}
\newcommand{\rb}[1]{\textcolor{blue}{\textit{[{#1} --RB]}}}

\newcommand{\modified}[1]{\textcolor{black}{{#1}}}
\newcommand{\modifiedagain}[1]{\textcolor{black}{{#1}}}

\newcommand{\trsone}[0]{TRS1}
\newcommand{\trstwo}[0]{TRS}
\newcommand{\goallang}[0]{\mathcal{L}}
\newcommand{\termlang}[0]{T(\Sigma,V)}
\newcommand{\goalorder}[0]{>_{\phi}}
\newcommand{\st}[0]{\;.\;}

\newcommand{\hmax}[0]{\texttt{max}}
\newcommand{\hmin}[0]{\texttt{min}}
%\newcommand{\rewrites}[0]{\mathop{\rightarrow}\limits_{\scriptscriptstyle{R}}}
\newcommand{\rewrites}[0]{\:\rightarrow_{R}\:}
%\newcommand{\rewrites}[0]{\longrightarrow}
%\newcommand{\rewrites}[0]{\rightharpoonup}
\newcommand{\pred}[0]{\textrm{ if }}
\newcommand{\hfalse}[0]{\texttt{false}}
\newcommand{\htrue}[0]{\texttt{true}}
\newcommand{\hsel}[0]{\texttt{select}}
\usepackage{syntax}

\newtheorem*{remark}{Remark}
\newtheorem{assumption}{Assumption}

%% Macros for quantities
\newcommand{\NumApps}{{\color{black} 10}\xspace}
\newcommand{\NumRulesFixed}{{\color{black} 4}\xspace}
\newcommand{\NumPredicatesRelaxed}{{\color{black} 17}\xspace}
\newcommand{\NumOrderingProblems}{{\color{black} 8}\xspace}
\newcommand{\NumRulesSynthesized}{{\color{black} 4127}\xspace}
\newcommand{\NumOpSequences}{{\color{black} 6246}\xspace}
\newcommand{\NumFailureExamples}{{\color{black} 61000}\xspace}
\newcommand{\NumSimplifiedExpressions}{{\color{black} 195371}\xspace} 
\newcommand{\NumBugsAutomated}{{\color{black} 5}\xspace}
\newcommand{\NumOriginalRules}{{\color{black} 999}\xspace}
\newcommand{\NumZdivCoqProvedRules}{{\color{black} 141}\xspace}
\newcommand{\NumZdivFalseRules}{{\color{black} 44}\xspace}
\newcommand{\NumZdivRelaxedPredicates}{{\color{black} 37}\xspace}

\newtheorem{theorem}{Theorem}[section]

% --- sample stuff only -----
% These format the sample code in this document

\usepackage{alltt}  % 
\newenvironment{demo}
  {\begin{alltt}\leftskip3em
     \def\\{\ttfamily\char`\\}%
     \def\{{\ttfamily\char`\{}%
     \def\}{\ttfamily\char`\}}}
  {\end{alltt}}
 
% metafont font.  If logo not available, use the second form
%
% \font\mffont=logosl10 scaled\magstep1
\let\mffont=\sf
% --- end-of-sample-stuff ---
 
\usepackage{hyperref}


\begin{document}
 
% ==========   Preliminary pages
%
% ( revised 2012 for electronic submission )
%

\prelimpages
 
%
% ----- copyright and title pages
%
\Title{Augmenting and Synthesizing Term Rewriting Systems}
\Author{Julie L. Newcomb}
\Year{2021}
\Program{Computer Science and Engineering}

\Chair{Rastislav Bodik}{Professor}{Computer Science and Engineering}
\Signature{René Just}
\Signature{Zachary Tatlock}
\Signature{Duane Storti}

\copyrightpage

\titlepage  

%
% ----- signature and quoteslip are gone
%

%
% ----- abstract
%


\setcounter{page}{-1}
\abstract{%
  Halide is a domain-specific language for high-performance image processing and tensor computations, widely adopted in industry.
  Internally, the Halide compiler relies on a term rewriting system to
  prove properties of code required for efficient and correct compilation.  This rewrite
  system is a collection of handwritten transformation rules 
  that incrementally rewrite expressions into simpler forms; the system requires high performance 
  in both time and memory usage to keep compile times low,
  while operating over the undecidable theory of integers.
  In this work, we apply formal techniques to prove the correctness of existing
  rewrite rules and provide a guarantee of termination. Then,
  we build an automatic program synthesis system 
  in order to craft new, provably correct rules from failure cases
  where the compiler was unable to prove properties. We identify and fix
  \NumRulesFixed incorrect rules as well as \NumOrderingProblems rules which
  could give rise to infinite rewriting loops.
  %% We run our synthesis process against 
  %% a large suite of failed proofs from compiler output, synthesizing a new body
  %% of rules that improves the system's proving power as evaluated on realistic
  %% benchmarks.
  %% The automated system can replace tedious human effort required to craft new rules
  %% in response to user-reported bugs.  We demonstrate that the new
  %% term rewriting system is provably sound, more robust, and more general, without
  %% slowing down the compiler.
  We demonstrate that the synthesizer can produce better rules than hand-authored ones in five bug fixes, and describe four cases in which it has served as an assistant to a human compiler engineer. We further show that it can proactively improve weaknesses in the compiler by synthesizing a large number of rules without human supervision and showing that the enhanced ruleset lowers peak memory usage of compiled code without appreciably increasing compilation times.

  We then turn from the goal of improving a handwritten term rewriting system to synthesizing an entirely new one. We argue that an artifact from a TRS termination proof, a special type of order over terms known as a reduction order, is an effective and expressive means of writing a specification for a term rewriting system. We demonstrate its own on a case study of another component of the Halide compiler called the variable solver. We present a synthesis process that takes a specification written in the form of a reduction order and a set of sample input expressions and produces a new ruleset. Furthermore, we show that we can use this synthesis process to allow users to experiment with different specifications by automatically generating new TRSs and evaluating them empirically, without ever handing to write a rule by hand.
}
 
%
% ----- contents & etc.
%
\tableofcontents
%\listoffigures
%\listoftables  % I have no tables
 
%


%
% ----- acknowledgments
%
\acknowledgments{% \vskip2pc
   {\narrower\noindent
  I would like to express my sincerest gratitude 

  to Shoaib Kamil and Andrew Adams, my mentors at my internship at Adobe Research, who have been insightful and inspiring collaborators ever since;

  to all of my fellow students in the PL synthesis group, past and present, at both the University of Washington and the University of California at Berkeley, who have been unfailingly welcoming and supportive from even before I was accepted into the program;

  and to my advisor, Ras Bodik.


   \par}
}

%
% ----- dedication
%
\dedication{\begin{center}\textit{to the memory of Catherine Anne Newcomb}\end{center}}

%
% end of the preliminary pages
 
 
 
%
% ==========      Text pages
%

\textpages

% ========== chapters
\input{chapters/01-intro}
\input{chapters/02-overview}
\input{chapters/03-verification}
\input{chapters/05-synthesis}
\input{chapters/06-synthesisB}
\input{chapters/07-conclusion}



\appendix
\include{chapters/A1-grammar}
\include{chapters/A2-sreductionorder}

\bibliographystyle{plainnat}
%\setcitestyle{square}
\bibliography{uwthesis}

\end{document}