Commit 0af1b73e authored by Edward Z. Yang's avatar Edward Z. Yang

Add cost semantics for STG profiling.

Signed-off-by: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>
parent b9063703
*.aux
*.log
*.out
StgOtt.tex
stg-spec.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% 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'
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
%%
%% 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 }}
\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}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment