diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 21:20:35 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 21:20:35 +0100 |
commit | b8e73be77abdef268594e747bdc6fc1ba503dc1f (patch) | |
tree | 4f018d9c0a64047b1c016d7ca06348e1779aed4a /doc | |
parent | 2d086fdfe0ee11204116f6bc442a35a00e77fe38 (diff) | |
download | compcert-kvx-b8e73be77abdef268594e747bdc6fc1ba503dc1f.tar.gz compcert-kvx-b8e73be77abdef268594e747bdc6fc1ba503dc1f.zip |
update index-kvx.html
Diffstat (limited to 'doc')
-rw-r--r-- | doc/index-kvx.html | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/index-kvx.html b/doc/index-kvx.html index dc646a67..6d56cbdb 100644 --- a/doc/index-kvx.html +++ b/doc/index-kvx.html @@ -65,9 +65,9 @@ inequations by fixpoint iteration. <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 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. +<LI> <A HREF="html/compcert.scheduling.abstractbb.AbstractBasicBlocksDef.html">AbstractBasicBlocksDef</A>: an IR for verifying some semantic properties on basic-blocks. +<LI> <A HREF="html/compcert.scheduling.abstractbb.Parallelizability.html">Parallelizability</A>: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block. +<LI> <A HREF="html/compcert.scheduling.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.scheduling.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> @@ -130,7 +130,7 @@ view of the activation record. <UL> <LI> <A HREF="html/compcert.scheduling.RTLpath.html">RTLpath</A>: extends RTL with annotations for delimitating superblocks (with possible liveness information). This IR is generic over the processor, and used for prepass scheduling. -<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). +<LI> <A HREF="html/compcert.scheduling.postpass_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 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. @@ -358,16 +358,16 @@ This IR is generic over the processor, even if currently, only used for KVX. <TR valign="top" style="color:#000000"> <TD>Reconstruction of basic-blocks at Mach level</TD> <TD>Mach to Machblock</TD> - <TD><A HREF="html/compcert.kvx.lib.Machblockgen.html">Machblockgen</A></TD> - <TD><A HREF="html/compcert.kvx.lib.ForwardSimulationBlock.html">ForwardSimulationBlock</A><BR> - <A HREF="html/compcert.kvx.lib.Machblockgenproof.html">Machblockgenproof</A></TD> + <TD><A HREF="html/compcert.scheduling.postpass_lib.Machblockgen.html">Machblockgen</A></TD> + <TD><A HREF="html/compcert.scheduling.postpass_lib.ForwardSimulationBlock.html">ForwardSimulationBlock</A><BR> + <A HREF="html/compcert.scheduling.postpass_lib.Machblockgenproof.html">Machblockgenproof</A></TD> </TR> <TR valign="top" style="color:#000000"> <TD>Emission of purely sequential assembly code</TD> <TD>Machblock to Asmblock</TD> <TD><A HREF="html/compcert.kvx.Asmblockgen.html"><I>Asmblockgen</I></A></TD> - <TD><A HREF="html/compcert.kvx.lib.Asmblockgenproof0.html"><I>Asmblockgenproof0</I></A><BR> + <TD><A HREF="html/compcert.kvx.Asmblockgenproof0.html"><I>Asmblockgenproof0</I></A><BR> <A HREF="html/compcert.kvx.Asmblockgenproof1.html"><I>Asmblockgenproof1</I></A><BR> <A HREF="html/compcert.kvx.Asmblockgenproof.html"><I>Asmblockgenproof</I></A></TD> </TR> |