Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fix the label for rewriting chapter

Browse Source
This commit is contained in:
Jip J. Dekker 2021-06-29 14:21:43 +10:00
parent d6ca88584c
commit fef9cdf90a
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 30 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
chapters/3_rewriting.tex
View File

@ -4,7 +4,7 @@
\input{chapters/3_rewriting_preamble}
\section{\glsentrytext{microzinc} and \glsentrytext{nanozinc}}\label{sec:4-micronano}
\section{\glsentrytext{microzinc} and \glsentrytext{nanozinc}}\label{sec:rew-micronano}
This section introduces the two sub-languages of \minizinc\ at the core of the new abstract machine model we have developed.
@ -15,7 +15,7 @@ Models written in \minizinc\ can be translated into \microzinc{}.
However, while all function calls in \flatzinc\ need to be solver-level primitives, \nanozinc\ calls can refer to functions implemented in \microzinc{}.
Furthermore, \nanozinc\ allows for constraints to be bound to a specific variable and constraints and variables declarations can be interleaved.
The core of the syntax of \microzinc\ is defined in \cref{fig:4-uzn-syntax}.
The core of the syntax of \microzinc\ is defined in \cref{fig:rew-uzn-syntax}.
We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which you can assume to be the same as the definition of \syntax{<type-inst>} and \syntax{<ident>} in the \minizinc\ grammar, see \cref{ch:minizinc-grammar}.
While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc\ programs, the conditions \syntax{<exp>} in if-then-else and where expressions have \mzninline{par} type.
@ -45,13 +45,13 @@ While we omit the typing rules here for space reasons, we will assume that in we
<gen-exp> ::= <ident> "in" <exp> ["," <ident> "in" <exp> ]*
\end{grammar}
\caption{\label{fig:4-uzn-syntax}Syntax of \microzinc{}.}
\caption{\label{fig:rew-uzn-syntax}Syntax of \microzinc{}.}
\end{figure}
\newcommand{\sep}{\rhd}
A \nanozinc\ program, defined in \cref{fig:4-nzn-syntax}, is simply a list of variable declaration and constraints in the form of calls.
The syntax ``\texttt{↳}'' will be used to track dependent constraints (this will be explained in detail in \cref{sec:4-nanozinc}, for now you can ignore them).
A \nanozinc\ program, defined in \cref{fig:rew-nzn-syntax}, is simply a list of variable declaration and constraints in the form of calls.
The syntax ``\texttt{↳}'' will be used to track dependent constraints (this will be explained in detail in \cref{sec:rew-nanozinc}, for now you can ignore them).
\begin{figure}
\begin{grammar}
@ -68,7 +68,7 @@ The syntax ``\texttt{↳}'' will be used to track dependent constraints (this wi
<nzn-bind> ::= "↳" <nzn-con>
\end{grammar}
\caption{\label{fig:4-nzn-syntax}Syntax of \nanozinc{}.}
\caption{\label{fig:rew-nzn-syntax}Syntax of \nanozinc{}.}
\end{figure}
\subsection{\glsentrytext{minizinc} to \glsentrytext{microzinc}/\glsentrytext{nanozinc}}
@ -198,7 +198,7 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
\end{example}
\subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:4-partial}
\subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:rew-partial}
Each call in a \nanozinc\ program is either a call to a solver-level predicate, or it has a corresponding \microzinc\ function definition.
The goal of partial evaluation is to transform the \nanozinc\ program into (essentially) \flatzinc{}, \ie\ a program where all calls are calls to solver-level predicates.
@ -209,7 +209,7 @@ Each non-primitive call in a \nanozinc\ program can then be replaced with the re
A key element of this rewriting process, then, is the transformation of functional expressions into relational form.
For this to happen, the rewriting process introduces fresh variables to represent intermediate expressions, and keeps track of constraints added during the rewriting.
\begin{example}\label{ex:4-abs}
\begin{example}\label{ex:rew-abs}
Consider the following (reasonably typical) \minizinc\ encoding for the absolute value function:
\begin{mzn}
@ -229,20 +229,20 @@ In this case, the constraint introduced in the \mzninline{let} expression may be
However, the introduced \mzninline{int_abs} constraint is only needed so long as any \emph{other} constraint refers to \mzninline{z}.
If \mzninline{z} is unused in the rest of the model, both \mzninline{z} and the \mzninline{int_abs} constraint can be removed.
As we shall see in \cref{sec:4-simplification}, certain optimisations and simplifications during the evaluation can lead to many expressions becoming unused.
As we shall see in \cref{sec:rew-simplification}, certain optimisations and simplifications during the evaluation can lead to many expressions becoming unused.
It is therefore important to track which constraints were merely introduced to define results of function calls.
In order to track these dependencies, \nanozinc\ attaches constraints that define a variable to the item that introduces the variable.
\subsection{\glsentrytext{nanozinc}}\label{sec:4-nanozinc}
\subsection{\glsentrytext{nanozinc}}\label{sec:rew-nanozinc}
A \nanozinc\ model (\cref{fig:4-nzn-syntax}) consists of a topologically-ordered list of variables declaration and constraints.
A \nanozinc\ model (\cref{fig:rew-nzn-syntax}) consists of a topologically-ordered list of variables declaration and constraints.
Variables are declared with an identifier, a domain, and it is associated with a list of identifiers of auxiliary constraints.
Constraints can also occur at the top-level of the \nanozinc\ model.
These are said to be the ``root-context'' constraints of the model, \ie\ those that have to hold globally and are not just used to define an auxiliary variable.
Only root-context constraints can effectively constrain the overall problem.
Constraints attached to variables originate from function calls, and since all functions are guaranteed to be total, attached constraints can only define the function result.
\begin{example}\label{ex:4-absnzn}
\begin{example}\label{ex:rew-absnzn}
Consider the \minizinc\ fragment
@ -270,7 +270,7 @@ Constraints attached to variables originate from function calls, and since all f
The core of the proposed \minizinc\ architecture is an abstract machine that performs the rewriting of \nanozinc\ items using the corresponding \microzinc\ function definitions.
We can now formally define the rewriting rules for this abstract machine.
The full set of rules appears in \cref{fig:4-rewrite-to-nzn-calls,fig:4-rewrite-to-nzn-let,fig:4-rewrite-to-nzn-other}.
The full set of rules appears in \cref{fig:rew-rewrite-to-nzn-calls,fig:rew-rewrite-to-nzn-let,fig:rew-rewrite-to-nzn-other}.
To simplify presentation, we assume that all rules that introduce new identifiers into the \nanozinc\ program do so in a way that ensures those identifiers are fresh (\ie\ not used in the rest of the \nanozinc\ program), by suitable alpha renaming.
\begin{figure*}
@ -291,11 +291,11 @@ To simplify presentation, we assume that all rules that introduce new identifier
\infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{}
\tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env}}}
\end{prooftree}
\caption{\label{fig:4-rewrite-to-nzn-calls} Rewriting rules for partial evaluation
\caption{\label{fig:rew-rewrite-to-nzn-calls} Rewriting rules for partial evaluation
of \microzinc\ calls to \nanozinc{}.}
\end{figure*}
The rules in \cref{fig:4-rewrite-to-nzn-calls} handle function calls.
The rules in \cref{fig:rew-rewrite-to-nzn-calls} handle function calls.
The first rule, (Call), evaluates a function call expression in the context of a \microzinc\ program \(\Prog{}\) and \nanozinc\ program \(\Env{}\).
The rule evaluates the function body \(\ptinline{E}\) where the formal parameters \(p_{i}\) are substituted by the call arguments \(a_{i}\).\footnote{We use \(E_{[a \mapsto b]}\) as a notation for the expression \(E\) where \(a\) is substituted by \(b\).} The result of this evaluation is the result of the function call.
@ -345,11 +345,11 @@ These are considered primitives, and as such simply need to be transferred into
\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env', \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\infer1[(ItemTupD)]{\Sem{\(\left(t_{1}\texttt{:}~x_{1}, \ldots, t_{k}\texttt{:}~x_{k}\right) = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\end{prooftree}
\caption{\label{fig:4-rewrite-to-nzn-let} Rewriting rules for partial evaluation
\caption{\label{fig:rew-rewrite-to-nzn-let} Rewriting rules for partial evaluation
of \microzinc\ let expressions to \nanozinc{}.}
\end{figure*}
The rules in \cref{fig:4-rewrite-to-nzn-let} considers let expressions.
The rules in \cref{fig:rew-rewrite-to-nzn-let} considers let expressions.
Starting from the main rule, (Let), the let items \textbf{I} are evaluated one at a time.
\Glspl{constraint} that follow from the evaluation of the let expression, by the (ItemC) rule, are captured in a third evaluation arguments.
When all inner items have been evaluated, the captured constraints are bound to the literal returned by the body of the let expression \textbf{X} in (Item0).
@ -405,11 +405,11 @@ We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) memb
\infer1[(ListG)]{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \Rightarrow{}
\tuple{\mbox{concat} [ A_v~|~v \in{} S ], \Env{} \cup{} \bigcup{}_{v \in{} S} \Env{}_{v}}}
\end{prooftree}
\caption{\label{fig:4-rewrite-to-nzn-other} Rewriting rules for partial evaluation
\caption{\label{fig:rew-rewrite-to-nzn-other} Rewriting rules for partial evaluation
of other \microzinc\ expressions to \nanozinc{}.}
\end{figure*}
Finally, the rules in \cref{fig:4-rewrite-to-nzn-other} handle the evaluation of variables, constants, conditionals and comprehensions.
Finally, the rules in \cref{fig:rew-rewrite-to-nzn-other} handle the evaluation of variables, constants, conditionals and comprehensions.
For completeness, we give the details here.
The (Ident) rule looks up a variable in the environment and return its bound value (for constants) or the variable itself.
@ -443,7 +443,7 @@ This topic is revisited in \cref{ch:incremental}.
The source code for the complete system will be made available under an open source license.
\section{NanoZinc Simplification}\label{sec:4-simplification}
\section{NanoZinc Simplification}\label{sec:rew-simplification}
The previous section introduced the basic evaluation model of \nanozinc: each call that has a corresponding \microzinc\ definition can be rewritten into a set of calls by evaluating the \microzinc\ code.
This section looks at further steps that the system can perform in order to produce better, more compact \nanozinc\ code.
@ -456,9 +456,9 @@ The model without the variable is therefore equisatisfiable with the original mo
Consider now the case where a variable in \nanozinc\ is only used in its own auxiliary definitions (the constraints directly succeeding the declaration prepended by \texttt{↳}).
\begin{example}\label{ex:4-absreif}
\begin{example}\label{ex:rew-absreif}
The following is a slight variation on the \minizinc\ fragment in \cref{ex:4-absnzn}:
The following is a slight variation on the \minizinc\ fragment in \cref{ex:rew-absnzn}:
\begin{mzn}
constraint abs(x) > y \/ c;
@ -468,7 +468,7 @@ Consider now the case where a variable in \nanozinc\ is only used in its own aux
The constraint \mzninline{abs(x) > y} is now used in a disjunction.
This means that instead of enforcing the constraint globally, the model needs to reason about whether the constraint holds or not.
This is called \gls{reification} (we will come back to this in \cref{sec:rew-cse}).
Following the rewriting rules, the generated \nanozinc\ code will look very similar to the code generated in \cref{ex:4-absnzn}, but with an additional \mzninline{bool_or} constraint for the disjunction, which uses a variable \mzninline{b} that will be introduced for \mzninline{abs(x) > y}:
Following the rewriting rules, the generated \nanozinc\ code will look very similar to the code generated in \cref{ex:rew-absnzn}, but with an additional \mzninline{bool_or} constraint for the disjunction, which uses a variable \mzninline{b} that will be introduced for \mzninline{abs(x) > y}:
\begin{nzn}
var true: c;
@ -718,10 +718,10 @@ In both cases we use the standard \minizinc\ library of global constraints (\ie\
We measured pure flattening time, \ie\ without time required to parse and type check in version 2.5.5, and without time required for compilation to \microzinc\ in the new system (compilation is usually very fast).
Times are averages of 10 runs.
\Cref{sfig:4-compareruntime} compares the flattening time for each of the 100 instances.
\Cref{sfig:rew-compareruntime} compares the flattening time for each of the 100 instances.
Points below the line indicate that the new system is faster.
On average, the new system achieves a speed-up of \(2.3\), with very few instances not achieving any speedup.
In terms of memory performance (\cref{sfig:4-comparemem}), version 2.4.3 can sometimes still outperform the new prototype.
In terms of memory performance (\cref{sfig:rew-comparemem}), version 2.4.3 can sometimes still outperform the new prototype.
We have identified that the main memory bottlenecks are our currently unoptimised implementations of \gls{cse} lookup tables and argument vectors.
These are very encouraging results, given that we are comparing a largely unoptimised prototype to a mature piece of software.
@ -731,15 +731,15 @@ These are very encouraging results, given that we are comparing a largely unopti
\begin{subfigure}[b]{.48\columnwidth}
\centering
\includegraphics[width=\columnwidth]{assets/img/rew_compare_runtime}
\caption{\label{sfig:4-compareruntime}Average run time (ms)}
\caption{\label{sfig:rew-compareruntime}Average run time (ms)}
\end{subfigure}%
\hspace{0.04\columnwidth}%
\begin{subfigure}[b]{.48\columnwidth}
\centering
\includegraphics[width=\columnwidth]{assets/img/rew_compare_memory}
\caption{\label{sfig:4-comparemem}Maximum resident set size (kbytes)}
\caption{\label{sfig:rew-comparemem}Maximum resident set size (kbytes)}
\end{subfigure}
\caption{\label{fig:4-runtime}Performance on flattening MiniZinc Challenge
\caption{\label{fig:rew-runtime}Performance on flattening MiniZinc Challenge
instances. \minizinc\ 2.5.5 (x-axis) vs new architecture (y-axis), log-log
plot. Dots below the line indicate the new system is better.}
\end{figure}

4
chapters/3_rewriting_preamble.tex
View File

@ -28,8 +28,8 @@ We have developed a prototype of this tool chain, and present experimental valid
The prototype is still very experimental, but preliminary results suggest the new tool chain can perform flattening much faster, and produce better models, than the current \minizinc\ compiler.
This chapter is organised as follows.
\Cref{sec:4-micronano} introduces the \microzinc\ and \nanozinc\ languages, the new intermediate representation we propose that enables more efficient flattening.
\Cref{sec:4-simplification} describes how we can perform various processing and simplification steps on this representation, and in \cref{sec:rew-experiments} we report on the experimental results of the prototype implementation.
\Cref{sec:rew-micronano} introduces the \microzinc\ and \nanozinc\ languages, the new intermediate representation we propose that enables more efficient flattening.
\Cref{sec:rew-simplification} describes how we can perform various processing and simplification steps on this representation, and in \cref{sec:rew-experiments} we report on the experimental results of the prototype implementation.
\begin{figure}
\centering