\documentclass[10pt]{article}

\usepackage[top=1in, bottom=1in, left=1in, right=1in]{geometry}

\usepackage{amsfonts}

\usepackage{amsmath}

\usepackage{chngpage}

\usepackage{hyperref}

\usepackage{mathpartir}

\usepackage{stmaryrd}

\usepackage{todonotes}

\usepackage{K3-Reference}

\hypersetup{colorlinks,linkcolor=magenta}

\newcommand{\tinysection}[1]{\noindent{\bf #1.}}

\title{K3: System and Language Design Reference}

\author{}

\date{}

\newcommand{\K}{\ensuremath{\texttt{K3}}}

\begin{document}

\section{Introduction}

\subsection{Target applications}

\subsection{Related work}

\section{System overview}

\subsection{Framework Architecture}

\section{Computation model}

\subsection{Triggers and message passing}

\subsection{Scheduling}

\subsection{Language grammar}

\subsection{Operational semantics}

\section{Data model}

\subsection{Nested collections}

\subsection{Indirections}

\subsection{Literals}

\subsection{Mutability}

\subsection{Memory model}

\section{Extensibility model}

\subsection{Data annotations}

\subsection{Control annotations}

\subsection{Properties}

\section{Type System}

\tinysection{Zach's document contents.}

\section{Program transformations and Optimization}

\subsection{Program normalization}

\subsubsection{Effect lifting}

\subsection{Standard optimizations}

\subsubsection{Constant folding}

\subsubsection{Dead code elimination}

\subsubsection{Common subexpression elimination}

\subsection{Fusion}

\begin{itemize}

\item We want to avoid excessive effort to get our optimizations to industrial strength

\begin{itemize}

\item Define explicit optimizations supported, and those elided

\item We focus on high-level optimizations in our framework, e.g., fusion/deforestation

\end{itemize}

\end{itemize}

\subsection{Annotation inference}

\subsubsection{Data structure selection}

\subsubsection{Execution strategy selection}

\subsection{Co-design and iterative inference}

\subsubsection{Workload partitioning}

\section{Code Generation and Execution}

\subsection{Interpretation}

\subsection{Imperative Targets}

Code generation to imperative target languages is done in two stages. The first is a pure $\K

\rightarrow \K$ transformation which produces an imperative embedding, more amenable to

translation into an imperative language. The second stage consists of the actual translation to

the backing language.

\subsubsection{Declaration Rules}

The declaration rules for the imperative transformation perform the following tasks:

\begin{itemize}

\item Rewrite triggers into functions of the corresponding type.

\end{itemize}

\begin{adjustwidth}{-0.5in}{-0.5in}\begin{align*}

\end{align*}\end{adjustwidth}

\subsubsection{Expression Rules}

The expression rules for the imperative transformation perform the following tasks:

\begin{itemize}

\item Inline anonymous function applications.

\end{itemize}

\begin{adjustwidth}{-0.5in}{-0.5in}\begin{align*}

\end{align*}\end{adjustwidth}

\subsection{\texttt{C++} Generation}

Following the imperative transformation, \texttt{C++} code generation takes place through

stringification.

\subsubsection{The Reification Problem}

When generating \texttt{C++} code for \K expressions, we must address the problem of

how to make use of intermediate storage for results. While most expressions can be inlined, some

(e.g.~\texttt{if-then-else}) require that their results be stored in an intermediate location

while others (e.g.~the left operand of a sequence operator) do not care about their results

whatsoever.

In this scenario, we can define four different ways in which the result of an expression might

be handled.

\begin{description}

\item[By Inlining:] The most common method is to inline the result of the sub-expression

into its position in the calling context. Most expressions follow this form.

\item[By Name:] Some expressions cannot provide their result inline, as the syntactic form

of the result might not be known until runtime (e.g.~\texttt{if-then-else}). In this

case, the expression must reify its result in a named variable, which it can pass up to

its calling context. The name of this variable can either be passed in from the calling

context, or generated in-situ.

\item[By Return:] If the result of an expression is the return value of a generated

function, its result need not be stored in an intermediate. Instead, the value can be

returned directly.

\sn{Return Reification}{Unless of course the expression requires that the result be

stored in an intermediate. (e.g.~$\gtSome$, $\gtInd$), in which case, how does

allocation work in the return context?}

\item[By Forgetting:] If the result is not used, it need not be stored at all (e.g.~the left

operand of a sequence operator).

\end{description}

The last three forms of reification share a similar structure in \texttt{C++}. Each form can be

expressed as an effect which reifies the result appropriately. To simplify the treatment of the

various reification forms in the code generation rules, we define the reification statement

$R_\delta$ as follows:

\begin{align*}

\end{align*}

\subsubsection{Expression Rules}

For the purposes of generating code, we define the family of derivation relations $\rwD$, where

$\delta \in \{\textsc{Inline}, \textsc{Named$(k)$}, \textsc{Return}, \textsc{Forget}\}$. Some

expressions lend themselves naturally to the inline form, and for such rules the reified form

can be derived mechanically. Alternately, other expressions lend themselves naturally to the

reified form, where the reverse is possible. These two canonical rules are as follows:

\begin{align*}

\end{align*}

Therefore it is generally only necessary to specify one of the rules (\textsc{Inline} or

otherwise) for each expression. These rules are as follows:

\begin{adjustwidth}{-0.5in}{-0.5in}\begin{align*}

\end{align*}\end{adjustwidth}

\subsubsection{Declaration Rules}

\begin{align*}

\end{align*}

\subsection{Haskell}

\tinysection{Effect embedding}

\section{Adaptive execution}

\subsection{Adaptive engine design:}

\begin{itemize}

\item need a common IR data representation accessible by all adaptive backends

\begin{itemize}

\item can we synthesize this from a K3 representation using a standard code generator?

\item that is, we metacompile our IR data as a tree with tagged variants?

\end{itemize}

\item code generation embeds initial K3 IR

\item each adaptive backend provides its own:

\begin{itemize}

\item JIT compiler from the IR to native code

\item compiled library loading facilities

\item adaptation algorithms on the IR

\end{itemize}

\end{itemize}

\subsection{Adaptation algorithm design}

\section{Deployment}

\subsection{Bootstrap}

\subsection{Docker}

\subsection{Mesos}

\section{Benchmarks}

\subsection{SQL Queries}

\subsection{Machine Learning Algorithms}

\subsection{Indexing Data Structures}

\end{document}