Update link to paper about demand analyser in user guide
[ghc.git] / docs / stg-spec / stg-spec.mng
1 \documentclass{article}
2
3 \usepackage{supertabular}
4 \usepackage{amsmath}
5 \usepackage{amssymb}
6 \usepackage{stmaryrd}
7 \usepackage{xcolor}
8 \usepackage{fullpage}
9 \usepackage{multirow}
10 \usepackage{url}
11
12 \newcommand{\ghcfile}[1]{\textsl{#1}}
13 \newcommand{\arraylabel}[1]{\multicolumn{2}{l}{\!\!\!\!\!\!\!\!\!\text{\underline{#1}:}}}
14
15 \input{StgOtt}
16
17 % increase spacing between rules for ease of reading:
18 \renewcommand{\ottusedrule}[1]{\[#1\]\\[1ex]}
19
20 \setlength{\parindent}{0in}
21 \setlength{\parskip}{1ex}
22
23 \newcommand{\gram}[1]{\ottgrammartabular{#1\ottafterlastrule}}
24
25 \title{The Spineless Tagless G-Machine, as implemented by GHC}
26
27 \begin{document}
28
29 \maketitle
30
31 \section{Introduction}
32
33 This document presents the syntax of STG, and the cost semantics utilized
34 for profiling.  While this document will be primarily useful for people
35 looking to work on profiling in GHC, the hope is that this will eventually
36 expanded to also have operational semantics for modern STG.
37
38 While care has been taken to adhere to the behavior in GHC, these rules
39 have not yet been used to perform any proofs.  There is some sloppiness
40 in here that probably would have to be cleaned up, especially with
41 respect to let-no-escape.  Some details are elided from this
42 presentation, especially extra annotated data in the STG data type
43 itself which is useful for code generation but not strictly necessary.
44
45 \section{Grammar}
46
47 \subsection{Metavariables}
48
49 We will use the following metavariables:
50
51 \ottmetavars{}\\
52
53 \subsection{Preliminaries}
54
55 Literals do not play a big role, so they are kept abstract:
56
57 \gram{\ottlit}
58
59 Primitive operations and foreign calls can influence the costs of
60 an application, but because their behavior depends on the specific
61 operation in question, they are kept abstract for simplicity's sake.
62
63 \gram{\ottop}
64
65 \subsection{Arguments}
66
67 Arguments in STG are restricted to be literals or variables:
68
69 \gram{\otta}
70
71 \subsection{Cost centres}
72
73 Cost centres are abstract labels to which costs can be attributed.  They
74 are collected into cost centre stacks.  Entering a
75 function requires us to combine two cost-centre stacks ($\bowtie$),
76 while entering a SCC pushes a cost-centre onto a cost-centre stack
77 ($\triangleright$); both of these functions are kept abstract in this
78 presentation.  The special current cost-centre stack ($\bullet$) occurs
79 only in STG and not at runtime and indicates that the lexically current
80 cost-centre should be used at runtime (see the cost semantics for details).
81 Some times we do not care about the choice of cost centre stack, in which case
82 we will use the don't care cost centre stack.
83
84 \gram{\ottcc}
85
86 \gram{\ottccs}
87
88 \subsection{Expressions}
89
90 The STG datatype that represents expressions:
91
92 \gram{\otte}\\
93
94 STG is a lot like Core, but with some differences:
95
96 \begin{itemize}
97 \item Function arguments must be literals or variables (thus, function application does not allocate),
98 \item Constructor and primitive applications are saturated,
99 \item Let-bindings can only have constructor applications or closures on the right-hand-side, and
100 \item Lambdas are forbidden outside of let-bindings.
101 \end{itemize}
102
103 The details of bindings for let statements:
104
105 \gram{\ottbinding}
106
107 \gram{\ottrhs}
108
109 \gram{\ottcl}
110
111 Closures have an update flag, which indicates whether or not they are
112 functions or thunks:
113
114 \gram{\ottupd}
115
116 Details for case alternatives:
117
118 \gram{\ottalt}
119
120 \section{Runtime productions}
121
122 In our cost semantics, we will explicitly model the heap:
123
124 \gram{\ottG}
125
126 Assignments on the heap are from names to heap values with an associated
127 cost-centre stack.  In our model, allocation produces a fresh name which
128 acts as a pointer to the value on the heap.
129
130 \gram{\ottGp}
131
132 \gram{\ottheap}
133
134 Execution procedes until a return value (a literal or a variable, i.e.
135 pointer to the heap) is produced.  To accommodate for let-no-escape
136 bindings, we also allow execution to terminate with a jump to a function
137 application of a let-no-escape variable.
138
139 \gram{\ottret}
140
141 Values $v$ are functions (re-entrant closures) and constructors; thunks
142 are not considered values.  Evaluation guarantees that a value will be
143 produced.
144
145 Profiling also records allocation costs for creating objects on the heap:
146
147 \gram{\ottt}
148
149 \gram{\ottcost}
150
151 \section{Cost semantics}
152
153 The judgment can be read as follows: with current cost centre $\textsf{ccs}$
154 and current heap $\Gamma$, the expression $e$ evaluates to $ret$, producing
155 a new heap $\Delta$ and a new current cost centre $\textsf{ccs'}$, performing
156 $\theta$ allocations.
157
158 \ottdefncost{}
159
160 \subsection{Notes}
161
162 \begin{itemize}
163 \item These semantics disagree with the executable semantics presented
164 by Simon Marlow at the Haskell Implementor's Workshop 2012.  (ToDo:
165 explain what the difference is.)
166 \item In the \textsc{Thunk} rule, while the indirection is attributed to
167 $\textsf{ccs}_0$, the result of the thunk itself ($y$) may be attributed
168 to someone else.
169 \item \textsc{AppUnder} and \textsc{AppOver} deal with under-saturated
170 and over-saturated function application.
171 The implementations of \textsc{App} rules are spread across two
172 different calling conventions for functions: slow calls and
173 direct calls.  Direct calls handle saturated and over-applied
174 cases (\coderef{codeGen/StgCmmLayout.hs}{slowArgs}), while slow
175 calls handle all cases (\textit{utils/genapply/GenApply.hs});
176 in particular, these cases ensure that the current cost-center
177 reverts to the one originally at the call site.
178 \item The \textsc{App} rule demonstrates that modern GHC
179 profiling uses neither evaluation scoping or lexical scoping; rather,
180 it uses a hybrid of the two (though with an appropriate definition
181 of $\bowtie$, either can be recovered.)  The presence of cost centre stacks is one of the primary
182 differences between modern GHC and Sansom'95.
183 \item The \textsc{AppTop} rule utilizes $\bullet$ to notate when a
184 function should influence the current cost centre stack.  The data type
185 used here could probably be simplified, since we never actually take
186 advantage of the fact that it is a cost centre.
187 \item As it turns out, the state of the current cost centre after
188 evaluation is never utilized.  In the original Sansom'95, this information
189 was necessary to allow for the implementation of lexical scoping; in
190 this presentation, all closures must live on the heap, and the cost centre
191 is thus recorded there.
192 \item \textsc{LneClosure} must explicitly save and reset the $\textsf{ccs}$ when the
193 binding is evaluated, whereas \textsc{LetClosure} takes advantage of the
194 fact that when the closure is allocated on the heap the $\text{ccs}$ is saved.
195 (ToDo: But isn't there a behavior difference when the closure is re-entrant?
196 Note that re-entrant/updatable is indistinguishable to a let-no-escape.)
197 \item Recursive bindings have been omitted but they work in the way you would expect.
198 \end{itemize}
199
200 \end{document}