diff options
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> |