diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-12-17 12:06:37 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-12-17 12:06:37 +0100 |
| commit | e21a56acc2d28995aef4586668f756806a53869b (patch) | |
| tree | e1d45dba883d13b64c31cbb08877ab08fe96b5ed /doc | |
| parent | 27dd728fd98adf43378f3cca7009aa6fcfc459ba (diff) | |
| download | compcert-kvx-e21a56acc2d28995aef4586668f756806a53869b.tar.gz compcert-kvx-e21a56acc2d28995aef4586668f756806a53869b.zip | |
add profiling entry-points in the htmldoc.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/index-kvx.html | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/doc/index-kvx.html b/doc/index-kvx.html index 39fdf799..dc646a67 100644 --- a/doc/index-kvx.html +++ b/doc/index-kvx.html @@ -254,6 +254,23 @@ This IR is generic over the processor, even if currently, only used for KVX. </TR> <TR valign="top" style="color:#000000"> + <TD colspan="4"><b>Passes introduced for profiling (for later use in trace selection)</b></TD> +</TR> +<TR valign="top" style="color:#000000"> + <TD>Insert profiling annotations (for recording experiments -- see PROFILE.md). + </TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/compcert.backend.Profiling.html">Profiling</A></TD> + <TD><A HREF="html/compcert.backend.Profilingproof.html">Profilingproof</A></TD> +</TR> +<TR valign="top" style="color:#000000"> + <TD>Update ICond nodes (from recorded experiments -- see PROFILE.md). + </TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/compcert.backend.ProfilingExploit.html">ProfilingExploit</A></TD> + <TD><A HREF="html/compcert.backend.ProfilingExploitproof.html">ProfilingExploitproof</A></TD> +</TR> +<TR valign="top" style="color:#000000"> <TD colspan="4"><b>Passes introduced for superblock prepass scheduling</b></TD> </TR> <TR valign="top" style="color:#000000"> @@ -372,12 +389,13 @@ This IR is generic over the processor, even if currently, only used for KVX. </TR> </TABLE> -<font color=gray> -<H3>All together</H3> +<H3>All together (there are many more RTL passes than on vanilla CompCert: their order is specified in Compiler)</H3> <UL> +</font> <LI> <A HREF="html/compcert.driver.Compiler.html">Compiler</A>: composing the passes together; whole-compiler semantic preservation theorems. +<font color=gray> <LI> <A HREF="html/compcert.driver.Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems. </UL> |