diff options
Diffstat (limited to 'doc/index-kvx.html')
| -rw-r--r-- | doc/index-kvx.html | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/doc/index-kvx.html b/doc/index-kvx.html index 95fdb6de..b8850727 100644 --- a/doc/index-kvx.html +++ b/doc/index-kvx.html @@ -34,10 +34,10 @@ a:active {color : Red; text-decoration : underline; } The unmodified parts of this table appear in <font color=gray>gray</font>. <br> <br> - A high-level view of this backend of CompCert is provided by this HAL preprint of Six, Boulmé and Monniaux (2019): - <div><a href=https://hal.archives-ouvertes.fr/hal-02185883>Certified Compiler Backends for VLIW Processors (Highly Modular Postpass-Scheduling in the CompCert Certified Compiler)</a></div> + A high-level view of this CompCert backend is provided by this OOPSLA'20 paper (of Six, Boulmé and Monniaux): + <div><a href=https://hal.archives-ouvertes.fr/hal-02185883>Certified and Efficient Instruction Scheduling. Application to Interlocked VLIW Processors.</a></div> <br> - Our source code is available on our <a href=https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx>GitLab public repository</a> (see conditions in the LICENSE file). + See also the <tt>README.md</tt> of our <a href=https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx>GitLab public repository</a>. </p> <font color=gray><H2>Table of contents</H2> @@ -60,11 +60,11 @@ inequations by fixpoint iteration. <LI> <A HREF="html/compcert.lib.Postorder.html">Postorder</A>: postorder numbering of a directed graph. </UL></font> -<H4>The <tt>abstractbb</tt> library, introduced for MPPA-KVX</H4> +<H4>The <tt>abstractbb</tt> library, introduced for KVX core</H4> <UL> <LI> <A HREF="html/compcert.kvx.abstractbb.AbstractBasicBlocksDef.html">AbstractBasicBlocksDef</A>: an IR for verifying some semantic properties on basic-blocks. <LI> <A HREF="html/compcert.kvx.abstractbb.Parallelizability.html">Parallelizability</A>: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block. -<LI> <A HREF="html/compcert.kvx.abstractbb.ImpSimuTest.html">ImpSimuTest</A>: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines <A HREF="html/compcert.kvx.abstractbb.SeqSimuTheory.html">SeqSimuTheory</A> with hash-consing. +<LI> <A HREF="html/compcert.kvx.abstractbb.ImpSimuTest.html">ImpSimuTest</A>: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines <A HREF="html/compcert.kvx.abstractbb.SeqSimuTheory.html">SeqSimuTheory</A> with hash-consing and uses <A HREF=https://github.com/boulme/ImpureDemo>the Impure library</A> to reason on physical equality and handling of imperative code in Coq. </UL> <font color=gray> @@ -121,11 +121,11 @@ replaced by a linear list of instructions with explicit branches and labels. view of the activation record. </UL> </font> -<H4>Languages introduced for MPPA-KVX</H4> +<H4>Languages introduced for KVX core</H4> <UL> <LI> <A HREF="html/compcert.kvx.lib.Machblock.html">Machblock</A>: a variant of Mach, with a syntax for basic-blocks, and a block-step semantics (execute one basic-block in one step). -This IR is generic over the processor, even if currently, only used for MPPA_KVX. -<LI> <A HREF="html/compcert.kvx.Asmvliw.html"><I>Asmvliw</I></A>: abstract syntax and semantics for Mppa_KVX VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles. +This IR is generic over the processor, even if currently, only used for KVX. +<LI> <A HREF="html/compcert.kvx.Asmvliw.html"><I>Asmvliw</I></A>: abstract syntax and semantics for KVX VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles. <LI> <A HREF="html/compcert.kvx.Asmblock.html"><I>Asmblock</I></A>: a variant of Asmvliw, with a sequential semantics within bundles, which make them corresponds here to usual basic-blocks. This IR is an intermediate step between Machblock and Asmvliw. <LI> <A HREF="html/compcert.kvx.Asm.html"><I>Asm</I></A>: a variant of Asmvliw with a flat syntax for bundles, instead of a structured one (bundle termination is encoded as a pseudo-instruction). This IR is mainly a wrapper of <I>Asmvliw</I> for a smooth integration in CompCert (and an easier pretty-printing of the abstract syntax). @@ -294,7 +294,7 @@ This IR is generic over the processor, even if currently, only used for MPPA_KVX </TR> </TABLE> -<H4>Compilation passes introduced for MPPA-KVX</H4> +<H4>Compilation passes introduced for KVX VLIW</H4> <TABLE cellpadding="5%"> <TR valign="top"> <TD>Reconstruction of basic-blocks at Mach level</TD> @@ -325,7 +325,7 @@ This IR is generic over the processor, even if currently, only used for MPPA_KVX <TD>Flattening bundles (only a bureaucratic operation)</TD> <TD>Asmvliw to Asm</TD> <TD><A HREF="html/compcert.kvx.Asmgen.html"><I>Asmgen</I></A></TD> - <TD><A HREF="html/compcert.kvx.Asmgenproof.html"><I>Asmgenproof</I></A></TD> + <TD><A HREF="html/compcert.kvx.Asmgenproof.html"><I>Asmgenproof</I></A> (whole simulation proof from <tt>Mach</tt> to <tt>Asm</tt>)</TD> </TR> </TABLE> |