Add cost semantics for STG profiling.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

5 files changed, 450 insertions, 0 deletions

diff --git a/docs/stg-spec/.gitignore b/docs/stg-spec/.gitignore
new file mode 100644
index 0000000000..71279ccc3f
--- /dev/null
+++ b/docs/stg-spec/.gitignore
@@ -0,0 +1,5 @@
+*.aux
+*.log
+*.out
+StgOtt.tex
+stg-spec.tex
diff --git a/docs/stg-spec/CostSem.ott b/docs/stg-spec/CostSem.ott
new file mode 100644
index 0000000000..2cb5bbda79
--- /dev/null
+++ b/docs/stg-spec/CostSem.ott
@@ -0,0 +1,122 @@
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  Cost semantics  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+grammar
+
+heap :: 'Heap_' ::= {{ com Values on the heap }}
+  | cl                  :: :: HeapClosure {{ com Closure }}
+  | K args              :: :: HeapConstructor {{ com Data constructor }}
+  | x                   :: :: HeapIndirection {{ com Indirection }}
+
+cost :: 'cost_' ::=
+  | alloc K :: :: AllocateCon
+  | alloc cl :: :: AllocateClosure
+  | alloc PAP :: :: AllocatePAP
+
+t {{ tex \theta }} :: 't_' ::=
+  | {} :: :: empty
+  | { ccs |-> cost } :: :: inject
+  | t <> t' :: :: append
+
+G {{ tex \Gamma }}, D {{ tex \Delta }}, T {{ tex \Theta }} :: 'G_' ::= {{ com Heap }}
+  | G [ Gp ] :: :: vn {{ com Heap with assignment }}
+
+Gp :: 'Gp_' ::= {{ com Heap assignment }}
+  | x |- ccs -> heap :: :: prod
+    {{ tex [[x]] \overset{[[ccs]]}{\mapsto} [[heap]] }}
+
+formula :: 'formula_' ::=
+  | judgement :: :: judgement
+  % all the random extra stuff we didn't want to gunk up the inductive
+  % types with...
+  | alt' = alt :: :: Galt
+  | ccs' /= ccs :: :: Gccsneq
+  | Gp in G :: :: Gin
+  | x fresh :: :: Gfresh
+
+v :: 'v_' ::=
+  | cl                :: :: HClosureReentrant
+  | K args            :: :: HConstructor
+
+ret :: 'ret_' ::= {{ com Return values }}
+  | a      :: :: Return {{ com Normal return }}
+  | { x args } :: :: LetNoEscape {{ com Jump to let-no-escape }}
+
+subrules
+  v <:: heap
+
+defns
+
+Jcost :: '' ::=
+
+defn
+    ccs , G : e  >- t ->  D : ret , ccs' :: :: cost :: ''
+        {{tex [[ccs]] [[,]] [[G]] [[:]] [[e]]\ \Downarrow_{[[t]]}\ [[D]] [[:]] [[ret]] [[,]] [[ccs']] }}
+        by
+
+    --------------------------------------- :: Lit
+    ccs, G : lit  >-{}->  G : lit, ccs
+
+    x |- ccs0 -> v in G
+    --------------------------------------- :: Whnf
+    ccs, G : x nil  >-{}->  G : x, ccs
+
+    ccs0, G : e  >-t->  D : z, ccs'
+    --------------------------------------- :: Thunk
+    ccs, G [ x |- ccs0 -> \ u _ nil . e ] : x nil  >-t->  D [ x |- ccs0 -> z ] : z, ccs'
+
+    f |- ccs0 -> \ r ccs1 </ yi // i /> </ xj // j /> . e in G
+    z fresh
+    --------------------------------------- :: AppUnder
+    ccs, G : f </ ai // i /> >- { ccs |-> alloc PAP } -> G [ z |- ccs -> \ r _ </ xj // j /> . f </ ai // i /> </ xj // j /> ] : z, ccs
+    % NB: PAPs not charged!
+
+    ccs ^ ccs0, G : e >-t-> D : z, ccs'
+    ------------------------------------------------- :: App
+    ccs, G [ f |- ccs0 -> \ r CCCS </ xi // i /> . e ] : f </ ai // i /> >-t->  D : z, ccs'
+
+    ccs, G : e >-t-> D : z, ccs'
+    ccs1 /= CCCS
+    ------------------------------------------------- :: AppTop
+    ccs, G [ f |- _ -> \ r ccs1 </ xi // i /> . e ] : f </ ai // i /> >-t->  D : z, ccs'
+
+    ccs, G : f </ ai // i /> >-t-> D : f', ccs'
+    ccs, D : f' </ bj // j /> >-t'-> T : z, ccs''
+    ---------------------------------------- :: AppOver
+    ccs, G : f </ ai // i /> </ bj // j /> >-t <> t'->  T : z, ccs''
+
+    z fresh
+    ---------------------------------------- :: ConApp
+    ccs, G : K </ ai // i />  >- { ccs |-> alloc K } ->  G [ z |- ccs -> K </ ai // i /> ] : z, ccs
+
+    altj = Kk </ xi // i /> -> e'
+    ccs, G : e >- t -> D [ y |- _ -> Kk </ ai // i /> ] : y, ccs'
+    ccs, D [ y |- _ -> Kk </ ai // i /> ] : e' [ y / x ] </ [ ai / xi ] // i /> >- t' -> T : z, ccs''
+    --------------------------------------------------------------- :: Case
+    ccs, G : case e as x of </ altj // j /> >- t <> t' -> T : z, ccs''
+
+    y fresh
+    ccs, G [ y |- ccs -> cl ] : e [ x / y ] >- t -> D : z, ccs'
+    ------------------------------------------------------------ :: LetClosure
+    ccs, G : let x = cl in e  >- { ccs |-> alloc cl } <> t ->  D : z, ccs'
+
+    y fresh
+    ccs, G [ y |- ccs -> K </ ai // i /> ] : e [ x / y ] >- t -> D : z, ccs'
+    ------------------------------------------------------------ :: LetCon
+    ccs, G : let x = K CCCS </ ai // i /> in e  >- { ccs |-> alloc K } <> t ->  D : z, ccs'
+
+    ccs, G : e >- t -> D : { f </ ai // i /> } , ccs'
+    ccs, D : e' </ [ ai / xi ] // i /> >- t' -> T : z, ccs''
+    ------------------------------------------------------------ :: LneClosure
+    ccs, G : lne f = \ upd _ </ x // i /> . e' in e  >- t <> t' ->  T : z, ccs''
+
+    ccs, G : e >- t -> D : x , ccs'
+    ccs, D : K </ ai // i /> >- t' -> T : z, ccs''
+    --------------------------------------------------------------- :: LneCon
+    ccs, G : lne x = K _ </ ai // i /> in e  >- t <> t' ->  T : z, ccs''
+
+    ccs # cc, G : e >- t -> D : z, ccs'
+    --------------------------------------- :: SCC
+    ccs, G : scc cc e >- t -> D : z, ccs'
diff --git a/docs/stg-spec/Makefile b/docs/stg-spec/Makefile
new file mode 100644
index 0000000000..4ac134f4fd
--- /dev/null
+++ b/docs/stg-spec/Makefile
@@ -0,0 +1,18 @@
+OTT_FILES = StgSyn.ott CostSem.ott
+OTT_TEX   = StgOtt.tex
+OTT_OPTS  = -tex_show_meta false
+TARGET    = stg-spec
+
+$(TARGET).pdf: $(TARGET).tex $(OTT_TEX)
+	latex -output-format=pdf $<
+	latex -output-format=pdf $<
+
+$(TARGET).tex: $(TARGET).mng $(OTT_FILES)
+	ott $(OTT_OPTS) -tex_filter $< $@ $(OTT_FILES)
+
+$(OTT_TEX): $(OTT_FILES)
+	ott -tex_wrap false $(OTT_OPTS) -o $@ $^
+
+.PHONY: clean
+clean:
+	rm -f $(TARGET).pdf $(TARGET).tex $(OTT_TEX) *.aux *.fdb_latexmk *.log
diff --git a/docs/stg-spec/StgSyn.ott b/docs/stg-spec/StgSyn.ott
new file mode 100644
index 0000000000..b53c91de8e
--- /dev/null
+++ b/docs/stg-spec/StgSyn.ott
@@ -0,0 +1,105 @@
+%%
+%% CoreSyn.ott
+%%
+%% defines formal version of core syntax
+%%
+%% See accompanying README file
+
+embed {{ tex-preamble
+  \newcommand{\coderef}[2]{\ghcfile{#1}:\texttt{#2}%
+}
+  \newcommand{\keyword}[1]{\textbf{#1} }
+  \newcommand{\labeledjudge}[1]{\vdash_{\!\!\mathsf{#1} } }
+}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  Metavariables  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+metavar f, x, y, z ::=   {{ com Variable names }}
+metavar K ::=   {{ com Data constructor names }}
+
+indexvar i, j, k, n ::= {{ com Indices to be used in lists }}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  Syntax  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+grammar
+
+lit {{ tex \textsf{lit} }} :: 'Literal_' ::=
+  {{ com Literals, \coderef{basicTypes/Literal.lhs}{Literal} }}
+
+op {{ tex \textsf{op} }} :: 'StgOp_' ::=
+  {{ com Primitive operation or foreign call, \coderef{stgSyn/StgSyn.lhs}{StgOp} }}
+
+cc {{ tex \textsf{cc} }} :: 'CostCentre_' ::=
+  {{ com Cost-centre, \coderef{profiling/CostCentre.lhs}{CostCentre} }}
+
+ccs {{ tex \textsf{ccs} }} :: 'CostCentreStack_' ::=
+  | CCCS :: :: CurrentCCS {{ com Current cost-centre stack }}
+    {{ tex \bullet }}
+  | _    :: :: DontCareCCS {{ com Don't care cost-centre stack }}
+  | ccs ^ ccs' :: :: EnterFunCCS {{ com Function entry, \coderef{rts/Profiling.c}{enterFunCCS} }}
+  | ccs # cc   :: :: PushCC {{ com Push a cost-centre, \coderef{rts/Profiling.c}{pushCostCentre} }}
+  {{ com Cost-centre stack, \coderef{profiling/CostCentre.lhs}{CostCentreStack} }}
+
+a, b, c :: 'StgArg_' ::= {{ com Arguments, \coderef{stgSyn/StgSyn.lhs}{StgArg} }}
+  | x   ::   :: StgVarArg {{ com Variable }}
+  | lit ::   :: StgLitArg {{ com Literal }}
+
+args :: 'StgArgs_' ::= {{ com List of arguments }}
+  | </ ai // , // i /> :: :: List
+  | args args' :: :: Append
+  | xs :: :: CastVariables
+  | nil :: :: EmptyList
+
+xs :: 'Ids_' ::= {{ com List of variables }}
+  | </ xi // , // i /> :: :: List
+  | nil :: :: EmptyList
+  | xs xs' :: :: Append
+
+e :: 'StgExpr_' ::= {{ com Expressions, \coderef{stgSyn/StgSyn.lhs}{StgExpr} }}
+  | lit                                  ::   :: StgLit {{ com Literal }}
+  | x args                               ::   :: StgApp {{ com Function application (or variable) }}
+  | K args                               ::   :: StgConApp {{ com Saturated constructor application }}
+  | op args                              ::   :: StgOpApp {{ com Saturated primitive application }}
+  | case e as x of </ alti // | // i />  ::   :: StgCase {{ com Pattern match }}
+  | let binding in e                     ::   :: StgLet  {{ com Let binding }}
+  | lne binding in e                     ::   :: StgLetNoEscape  {{ com Let-no-escape binding }}
+  | scc cc e                             ::   :: StgSCC {{ com Set cost-centre }}
+  | ( e )                                :: M :: Parens {{ com Parenthesized expression }}
+  | e' subst                             :: M :: Tsub
+
+subst :: 'Subst_' ::= {{ com List of substitutions }}
+  | [ a / x ]         ::   :: Mapping
+  | </ substi // i /> ::   :: List
+
+binding :: 'StgBind_' ::= {{ com Let-bindings, \coderef{stgSyn/StgSyn.lhs}{StgBind} }}
+  | x = rhs                         ::   :: StgNonRec  {{ com Non-recursive binding }}
+  | rec </ xi = rhsi // and // i /> ::   :: StgRec     {{ com Recursive binding }}
+
+upd :: 'UpdateFlag_' ::= {{ com Update flag, \coderef{stgSyn/StgSyn.lhs}{UpdateFlag} }}
+  | r :: :: ReEntrant {{ com Function (re-entrant closure) }}
+  | u :: :: Updatable {{ com Thunk (updatable closure) }}
+
+cl :: 'StgRhsClosure_' ::= {{ com StgRhsClosure }}
+  | \ upd ccs xs . e  :: :: StgRhsClosure
+
+rhs :: 'StgRhs_' ::= {{ com Right-hand sides, \coderef{stgSyn/StgSyn.lhs}{StgRhs} }}
+  | cl                :: :: StgRhsClosure {{ com Closure }}
+  | K ccs args        :: :: StgRhsCon {{ com Constructor }}
+  | x                 :: :: StgRhsIndirection {{ com Indirection (runtime only) }}
+
+alt :: 'StgAlt_' ::= {{ com Case alternative, \coderef{stgSyn/StgSyn.lhs}{StgAlt} }}
+  | K </ xi // i /> -> e    ::   :: StgAlt  {{ com Constructor applied to fresh names }}
+
+terminals :: 'terminals_' ::=
+  | \                   ::   :: lambda     {{ tex \lambda }}
+  | ->                  ::   :: arrow      {{ tex \rightarrow }}
+  | |->                 ::   :: mapsto     {{ tex \mapsto }}
+  | <>                  ::   :: union      {{ tex \mathbin{\mathaccent\cdot\cup} }}
+  | nil                 ::   :: empty      {{ tex \cdot }}
+  | /=                  ::   :: neq        {{ tex \neq }}
+  | ^                   ::   :: enterFun   {{ tex \bowtie }}
+  | #                   ::   :: push       {{ tex \triangleright }}
diff --git a/docs/stg-spec/stg-spec.mng b/docs/stg-spec/stg-spec.mng
new file mode 100644
index 0000000000..cf8a71672d
--- /dev/null
+++ b/docs/stg-spec/stg-spec.mng
@@ -0,0 +1,200 @@
+\documentclass{article}
+
+\usepackage{supertabular}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{stmaryrd}
+\usepackage{xcolor}
+\usepackage{fullpage}
+\usepackage{multirow}
+\usepackage{url}
+
+\newcommand{\ghcfile}[1]{\textsl{#1}}
+\newcommand{\arraylabel}[1]{\multicolumn{2}{l}{\!\!\!\!\!\!\!\!\!\text{\underline{#1}:}}}
+
+\input{StgOtt}
+
+% increase spacing between rules for ease of reading:
+\renewcommand{\ottusedrule}[1]{\[#1\]\\[1ex]}
+
+\setlength{\parindent}{0in}
+\setlength{\parskip}{1ex}
+
+\newcommand{\gram}[1]{\ottgrammartabular{#1\ottafterlastrule}}
+
+\title{The Spineless Tagless G-Machine, as implemented by GHC}
+
+\begin{document}
+
+\maketitle
+
+\section{Introduction}
+
+This document presents the syntax of STG, and the cost semantics utilized
+for profiling.  While this document will be primarily useful for people
+looking to work on profiling in GHC, the hope is that this will eventually
+expanded to also have operational semantics for modern STG.
+
+While care has been taken to adhere to the behavior in GHC, these rules
+have not yet been used to perform any proofs.  There is some sloppiness
+in here that probably would have to be cleaned up, especially with
+respect to let-no-escape.  Some details are elided from this
+presentation, especially extra annotated data in the STG data type
+itself which is useful for code generation but not strictly necessary.
+
+\section{Grammar}
+
+\subsection{Metavariables}
+
+We will use the following metavariables:
+
+\ottmetavars{}\\
+
+\subsection{Preliminaries}
+
+Literals do not play a big role, so they are kept abstract:
+
+\gram{\ottlit}
+
+Primitive operations and foreign calls can influence the costs of
+an application, but because their behavior depends on the specific
+operation in question, they are kept abstract for simplicity's sake.
+
+\gram{\ottop}
+
+\subsection{Arguments}
+
+Arguments in STG are restricted to be literals or variables:
+
+\gram{\otta}
+
+\subsection{Cost centres}
+
+Cost centres are abstract labels to which costs can be attributed.  They
+are collected into cost centre stacks.  Entering a
+function requires us to combine two cost-centre stacks ($\bowtie$),
+while entering a SCC pushes a cost-centre onto a cost-centre stack
+($\triangleright$); both of these functions are kept abstract in this
+presentation.  The special current cost-centre stack ($\bullet$) occurs
+only in STG and not at runtime and indicates that the lexically current
+cost-centre should be used at runtime (see the cost semantics for details).
+Some times we do not care about the choice of cost centre stack, in which case
+we will use the don't care cost centre stack.
+
+\gram{\ottcc}
+
+\gram{\ottccs}
+
+\subsection{Expressions}
+
+The STG datatype that represents expressions:
+
+\gram{\otte}\\
+
+STG is a lot like Core, but with some differences:
+
+\begin{itemize}
+\item Function arguments must be literals or variables (thus, function application does not allocate),
+\item Constructor and primitive applications are saturated,
+\item Let-bindings can only have constructor applications or closures on the right-hand-side, and
+\item Lambdas are forbidden outside of let-bindings.
+\end{itemize}
+
+The details of bindings for let statements:
+
+\gram{\ottbinding}
+
+\gram{\ottrhs}
+
+\gram{\ottcl}
+
+Closures have an update flag, which indicates whether or not they are
+functions or thunks:
+
+\gram{\ottupd}
+
+Details for case alternatives:
+
+\gram{\ottalt}
+
+\section{Runtime productions}
+
+In our cost semantics, we will explicitly model the heap:
+
+\gram{\ottG}
+
+Assignments on the heap are from names to heap values with an associated
+cost-centre stack.  In our model, allocation produces a fresh name which
+acts as a pointer to the value on the heap.
+
+\gram{\ottGp}
+
+\gram{\ottheap}
+
+Execution procedes until a return value (a literal or a variable, i.e.
+pointer to the heap) is produced.  To accomodate for let-no-escape
+bindings, we also allow execution to terminate with a jump to a function
+application of a let-no-escape variable.
+
+\gram{\ottret}
+
+Values $v$ are functions (re-entrant closures) and constructors; thunks
+are not considered vaules.  Evaluation guarantees that a value will be
+produced.
+
+Profiling also records allocation costs for creating objects on the heap:
+
+\gram{\ottt}
+
+\gram{\ottcost}
+
+\section{Cost semantics}
+
+The judgment can be read as follows: with current cost centre $\textsf{ccs}$
+and current heap $\Gamma$, the expression $e$ evaluates to $ret$, producing
+a new heap $\Delta$ and a new current cost centre $\textsf{ccs'}$, performing
+$\theta$ allocations.
+
+\ottdefncost{}
+
+\subsection{Notes}
+
+\begin{itemize}
+\item These semantics disagree with the executable semantics presented
+by Simon Marlow at the Haskell Implementor's Workshop 2012.  (ToDo:
+explain what the difference is.)
+\item In the \textsc{Thunk} rule, while the indirection is attributed to
+$\textsf{ccs}_0$, the result of the thunk itself ($y$) may be attributed
+to someone else.
+\item \textsc{AppUnder} and \textsc{AppOver} deal with under-saturated
+and over-saturated function application.
+The implementations of \textsc{App} rules are spread across two
+different calling conventions for functions: slow calls and
+direct calls.  Direct calls handle saturated and over-applied
+cases (\coderef{codeGen/StgCmmLayout.hs}{slowArgs}), while slow
+calls handle all cases (\textit{utils/genapply/GenApply.hs});
+in particular, these cases ensure that the current cost-center
+reverts to the one originally at the call site.
+\item The \textsc{App} rule demonstrates that modern GHC
+profiling uses neither evaluation scoping or lexical scoping; rather,
+it uses a hybrid of the two (though with an appropriate definition
+of $\bowtie$, either can be recovered.)  The presence of cost centre stacks is one of the primary
+differences between modern GHC and Sansom'95.
+\item The \textsc{AppTop} rule utilizes $\bullet$ to notate when a
+function should influence the current cost centre stack.  The data type
+used here could probably be simplified, since we never actually take
+advantage of the fact that it is a cost centre.
+\item As it turns out, the state of the current cost centre after
+evaluation is never utilized.  In the original Sansom'95, this information
+was necessary to allow for the implementation of lexical scoping; in
+this presentation, all closures must live on the heap, and the cost centre
+is thus recorded there.
+\item \textsc{LneClosure} must explicitly save and reset the $\textsf{ccs}$ when the
+binding is evaluated, whereas \textsc{LetClosure} takes advantage of the
+fact that when the closure is allocated on the heap the $\text{ccs}$ is saved.
+(ToDo: But isn't there a behavior difference when the closure is re-entrant?
+Note that re-entrant/updatable is indistinguishable to a let-no-escape.)
+\item Recursive bindings have been omitted but they work in the way you would expect.
+\end{itemize}
+
+\end{document}