From 2e39ecb491bbd001ecdfba73115bc76e3f53f517 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Wed, 29 Jul 2020 09:17:26 +0200
Subject: Improving the coqdoc

---
 doc/index-kvx.html       |  10 +--
 kvx/Asm.v                |  10 ++-
 kvx/Asmblockdeps.v       |  23 +++--
 kvx/Asmgenproof.v        |   7 +-
 kvx/Asmvliw.v            | 218 +++++++++++++++++++----------------------------
 kvx/PostpassScheduling.v |  19 ++---
 kvx/lib/Machblock.v      |  15 +++-
 kvx/lib/Machblockgen.v   |  13 ++-
 8 files changed, 145 insertions(+), 170 deletions(-)

diff --git a/doc/index-kvx.html b/doc/index-kvx.html
index 95fdb6de..ff3fbc17 100644
--- a/doc/index-kvx.html
+++ b/doc/index-kvx.html
@@ -60,7 +60,7 @@ 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.
@@ -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>
diff --git a/kvx/Asm.v b/kvx/Asm.v
index 69d0ecf6..30aafc55 100644
--- a/kvx/Asm.v
+++ b/kvx/Asm.v
@@ -13,7 +13,7 @@
 (*                                                             *)
 (* *************************************************************)
 
-(** * Abstract syntax for KVX textual assembly language.
+(** Abstract syntax for KVX textual assembly language.
 
     Each emittable instruction is defined here. ';;' is also defined as an instruction.
     The goal of this representation is to stay compatible with the rest of the generic backend of CompCert
@@ -49,7 +49,7 @@ Inductive addressing : Type :=
   | ARegXS (ro: ireg)
 .
 
-(** Syntax *)
+(** * Syntax *)
 Inductive instruction : Type :=
   (** pseudo instructions *)
   | Pallocframe (sz: Z) (pos: ptrofs)               (**r allocate new stack frame *)
@@ -104,7 +104,7 @@ Inductive instruction : Type :=
   | Pclzll (rd rs: ireg)
   | Pstsud (rd rs1 rs2: ireg)
             
-  (** Loads **)
+  (** Loads *)
   | Plb     (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing)     (**r load byte *)
   | Plbu    (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing)     (**r load byte unsigned *)
   | Plh     (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing)     (**r load half word *)
@@ -118,7 +118,7 @@ Inductive instruction : Type :=
   | Plq     (rs: gpreg_q) (ra: ireg) (ofs: addressing)  (**r load 2*64-bit *)
   | Plo     (rs: gpreg_o) (ra: ireg) (ofs: addressing)  (**r load 4*64-bit *)
 
-  (** Stores **)
+  (** Stores *)
   | Psb     (rs: ireg) (ra: ireg) (ofs: addressing)     (**r store byte *)
   | Psh     (rs: ireg) (ra: ireg) (ofs: addressing)     (**r store half byte *)
   | Psw     (rs: ireg) (ra: ireg) (ofs: addressing)     (**r store int32 *)
@@ -547,6 +547,8 @@ Definition basic_to_instruction (b: basic) :=
   | PStoreORRO qrs ra ofs => Pso qrs ra (AOff ofs)
   end.
 
+(** * Semantics (given through the existence of well-formed VLIW program) *)
+
 Section RELSEM.
 
 Definition code := list instruction.
diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v
index 1881e7e9..3d981100 100644
--- a/kvx/Asmblockdeps.v
+++ b/kvx/Asmblockdeps.v
@@ -12,12 +12,14 @@
 (*                                                             *)
 (* *************************************************************)
 
-(** * Translation from Asmblock to AbstractBB 
+(** * Translation from [Asmvliw] to [AbstractBB] *)
 
-    We define a specific instance of AbstractBB, named L, translate bblocks from Asmblock into this instance
-    AbstractBB will then define two semantics for L : a sequential, and a semantic one
-    We prove a bisimulation between the parallel semantics of L and AsmVLIW
-    From this, we also deduce a bisimulation between the sequential semantics of L and Asmblock *)
+(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmvliw] into [L].
+    [AbstractBB] will then define two semantics for [L]: a sequential and a parallel one.
+    We prove a bisimulation between the parallel semantics of [L] and [AsmVLIW].
+    We also prove a bisimulation between the sequential semantics of [L] and [Asmblock].
+    Then, the checkers on [Asmblock] and [Asmvliw] are deduced from those of [L].
+ *)
 
 Require Import AST.
 Require Import Asmblock.
@@ -40,7 +42,7 @@ Require Import Lia.
 
 Open Scope impure.
 
-(** Definition of L *)
+(** Definition of [L] *)
 
 Module P<: ImpParam.
 Module R := Pos.
@@ -660,7 +662,7 @@ Module IST := ImpSimu L ImpPosDict.
 Import L.
 Import P.
 
-(** Compilation from Asmblock to L *)
+(** Compilation from [Asmvliw] to [L] *)
 
 Local Open Scope positive_scope.
 
@@ -748,6 +750,8 @@ Definition inv_ppos (p: R.t) : option preg :=
 
 Notation "a @ b" := (Econs a b) (at level 102, right associativity).
 
+(** Translations of instructions *)
+
 Definition trans_control (ctl: control) : inst :=
   match ctl with
   | Pret => [(#PC, PReg(#RA))]
@@ -859,6 +863,8 @@ Proof.
   intros. destruct bb as [hdr bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity.
 Qed.
 
+(** Lemmas on the translation *)
+
 Definition state := L.mem.
 Definition exec := L.run.
 
@@ -1800,6 +1806,7 @@ Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool :=
 
 Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp.
 
+(** Main simulation (Impure) theorem *) 
 Theorem bblock_simu_test_correct verb p1 p2 :
   WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockprops.bblock_simu ge fn p1 p2.
 Proof.
@@ -1807,7 +1814,7 @@ Proof.
 Qed.
 Hint Resolve bblock_simu_test_correct: wlp.
 
-(* Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *)
+(** ** Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *)
 
 Import UnsafeImpure.
 
diff --git a/kvx/Asmgenproof.v b/kvx/Asmgenproof.v
index f43acd37..9e35e268 100644
--- a/kvx/Asmgenproof.v
+++ b/kvx/Asmgenproof.v
@@ -13,7 +13,7 @@
 (*                                                             *)
 (* *************************************************************)
 
-(** Correctness proof for Asmgen *)
+(** Composing all passes from Mach to KVX Asm *)
 
 Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
@@ -46,7 +46,7 @@ Proof.
   exists tp; split. apply Asm.transf_program_match; auto. auto.
 Qed.
 
-(** Return Address Offset *)
+(** Return Address Offset for Mach *)
 
 Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop :=
   Mach_return_address_offset Asmblockgenproof.return_address_offset.
@@ -59,6 +59,7 @@ Proof.
   intros; eapply Asmblockgenproof.return_address_exists; eauto.
 Qed.
 
+(** Main preservation theorem: from Mach to KVX Asm *)
 
 Section PRESERVATION.
 
@@ -86,7 +87,7 @@ End PRESERVATION.
 Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes).
 
 (*******************************************)
-(* Stub actually needed by driver/Compiler *)
+(** Stub actually needed by driver/Compiler *)
 
 Module Asmgenproof0.
 
diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v
index 301ee69a..296963a7 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -41,7 +41,7 @@ Require Import Chunks.
     this view induces our sequential semantics of bundles defined in [Asmblock].
 *)
 
-(** General Purpose registers. *)
+(** ** General Purpose registers. *)
 
 Inductive gpreg: Type :=
   | GPR0:  gpreg | GPR1:  gpreg | GPR2:  gpreg | GPR3:  gpreg | GPR4:  gpreg
@@ -165,7 +165,7 @@ End PregEq.
 
 Module Pregmap := EMap(PregEq).
 
-(** Conventional names for stack pointer ([SP]), return address ([RA]), frame pointer ([FP]) and other temporaries used *)
+(** ** Conventional names for stack pointer ([SP]), return address ([RA]), frame pointer ([FP]) and other temporaries used *)
 
 Notation "'SP'" := GPR12 (only parsing) : asm.
 Notation "'FP'" := GPR17 (only parsing) : asm.
@@ -173,6 +173,8 @@ Notation "'MFP'" := R17 (only parsing) : asm.
 Notation "'GPRA'" := GPR16 (only parsing) : asm.
 Notation "'RTMP'" := GPR32 (only parsing) : asm.
 
+(** ** Names of tests in comparisons *)
+
 Inductive btest: Type :=
   | BTdnez                              (**r Double Not Equal to Zero *)
   | BTdeqz                              (**r Double Equal to Zero *)
@@ -214,55 +216,47 @@ Inductive ftest: Type :=
   | FTult                               (**r Unordered or Less Than *)
   .
 
-(** Offsets for load and store instructions.  An offset is either an
-  immediate integer or the low part of a symbol. *)
+(** *** Offsets for load and store instructions. *)
 
 Definition offset : Type := ptrofs.
 
-(** We model a subset of the KVX instruction set. In particular, we do not
-  support floats yet.
+(** *** Labels for goto (in the current function) *)
 
-  Although it is possible to use the 32-bits mode, for now we don't support it.
+Definition label := positive.
 
-  We follow a design close to the one used for the Risc-V port: one set of
-  pseudo-instructions for 32-bit integer arithmetic, with suffix W, another
-  set for 64-bit integer arithmetic, with suffix L.
+(** ** Instructions *)
+
+(** We model a subset of the KVX instruction set.
 
-  When mapping to actual instructions, the OCaml code in TargetPrinter.ml
+-  Although it is possible to use the 32-bits mode, for now we don't support it. When mapping to actual instructions, the OCaml code in TargetPrinter.ml
   throws an error if we are not in 64-bits mode.
-*)
 
-(** * Instructions *)
+- We follow a design close to the one used for the Risc-V port: one set of
+  pseudo-instructions for 32-bit integer arithmetic, with suffix W, another
+  set for 64-bit integer arithmetic, with suffix L.
 
-Definition label := positive.
+- With respect to other CompCert assemblies, we define a type hierarchy of instructions (instead of a flat type).
+  This helps us to factorize similar cases for the scheduling verifier.
+
+*)
 
-(** Instructions to be expanded in control-flow *)
+(** *** Instructions to be expanded in control-flow *)
 Inductive ex_instruction : Type :=
   (* Pseudo-instructions *)
   | Pbuiltin: external_function -> list (builtin_arg preg)
               -> builtin_res preg -> ex_instruction   (**r built-in function (pseudo) *)
 .
 
-(** FIXME: comment not up to date !
-
-
- The pseudo-instructions are the following:
+(** Similarly to other CompCert assembly languages, the pseudo-instructions are the following:
 
 - [Ploadsymbol]: load the address of a symbol in an integer register.
-  Expands to the [la] assembler pseudo-instruction, which does the right
-  thing even if we are in PIC mode.
 
 - [Pallocframe sz pos]: in the formal semantics, this
   pseudo-instruction allocates a memory block with bounds [0] and
   [sz], stores the value of the stack pointer at offset [pos] in this
   block, and sets the stack pointer to the address of the bottom of
   this block.
-  In the printed ASM assembly code, this allocation is:
-<<
-        mv      x30, sp
-        sub     sp,  sp, #sz
-        sw      x30, #pos(sp)
->>
+
   This cannot be expressed in our memory model, which does not reflect
   the fact that stack frames are adjacent and allocated/freed
   following a stack discipline.
@@ -270,25 +264,13 @@ Inductive ex_instruction : Type :=
 - [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction
   reads the word at [pos] of the block pointed by the stack pointer,
   frees this block, and sets the stack pointer to the value read.
-  In the printed ASM assembly code, this freeing is just an increment of [sp]:
-<<
-        add     sp,  sp, #sz
->>
   Again, our memory model cannot comprehend that this operation
   frees (logically) the current stack frame.
 
 - [Pbtbl reg table]: this is a N-way branch, implemented via a jump table
-  as follows:
-<<
-        la      x31, table
-        add     x31, x31, reg
-        jr      x31
-table:  .long   table[0], table[1], ...
->>
-  Note that [reg] contains 4 times the index of the desired table entry.
 *)
 
-(** Control Flow instructions *)
+(** *** Control Flow instructions *)
 Inductive cf_instruction : Type :=
   | Pret                                            (**r return *)
   | Pcall   (l: label)                              (**r function call *)
@@ -305,7 +287,7 @@ Inductive cf_instruction : Type :=
   | Pcbu    (bt: btest) (r: ireg) (l: label)        (**r branch based on btest with unsigned semantics *)
 .
 
-(** Loads **)
+(** *** Loads *)
 Definition concrete_default_notrap_load_value (chunk : memory_chunk) :=
   match chunk with
   | Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned
@@ -337,7 +319,7 @@ Inductive ld_instruction : Type :=
   | PLoadORRO  (rd: gpreg_o) (ra: ireg) (ofs: offset)
 .
 
-(** Stores **)
+(** *** Stores *)
 Inductive store_name : Type :=
   | Psb                                             (**r store byte *)
   | Psh                                             (**r store half byte *)
@@ -357,7 +339,7 @@ Inductive st_instruction : Type :=
   | PStoreORRO (rs: gpreg_o) (ra: ireg) (ofs: offset)
 .
 
-(** Arithmetic instructions **)
+(** *** Arithmetic instructions *)
 Inductive arith_name_r : Type :=
   | Ploadsymbol (id: ident) (ofs: ptrofs)           (**r load the address of a symbol *)
 .
@@ -571,6 +553,8 @@ Coercion PArithARRI64:   arith_name_arri64    >-> Funclass.
 
 End PArithCoercions.
 
+(** ** Basic instructions *)
+
 Inductive basic : Type :=
   | PArith          (i: ar_instruction)
   | PLoad           (i: ld_instruction)
@@ -586,6 +570,7 @@ Coercion PLoad:         ld_instruction >-> basic.
 Coercion PStore:        st_instruction >-> basic.
 Coercion PArith:        ar_instruction >-> basic.
 
+(** ** Control-flow instructions *)
 
 Inductive control : Type :=
   | PExpand         (i: ex_instruction)
@@ -596,9 +581,9 @@ Coercion PExpand:   ex_instruction >-> control.
 Coercion PCtlFlow:  cf_instruction >-> control.
 
 
-(** * Definition of a bblock (ie a bundle)
+(** * Definition of a bblock (ie a bundle) *)
 
-A bundle/bblock must contain at least one instruction.
+(** A bundle/bblock must contain at least one instruction.
 
 This choice simplifies the definition of [find_bblock] below:
 indeed, each address of a code block identifies at most one bundle
@@ -621,9 +606,8 @@ Definition non_empty_exit (exit: option control): bool :=
 Definition non_empty_bblockb (body: list basic) (exit: option control): bool := non_empty_body body || non_empty_exit exit.
 
 
-(** TODO
- * For now, we consider a builtin is alone in a bundle (and a basic block).
- * Is there a way to avoid that ?
+(** For now, we consider a builtin is alone in a bundle (and a basic block).
+    Is there a way to avoid that ? (TODO)
  *)
 Definition builtin_aloneb (body: list basic) (exit: option control) :=
   match exit with
@@ -655,12 +639,12 @@ Definition length_opt {A} (o: option A) : nat :=
   | None => 0
   end.
 
-(* WARNING: the notion of size is not the same than in Machblock !
-   We ignore labels here...
+(** The notion of size induces the notion of "valid" code address given by [find_bblock]
+    The result is in Z to be compatible with operations on PC. 
 
-   This notion of size induces the notion of "valid" code address given by [find_bblock]
+    WARNING: this notion of size is not the same than in Machblock !
+    We ignore labels here...
 
-   The result is in Z to be compatible with operations on PC.
 *)
 Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)).
 
@@ -678,7 +662,7 @@ Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
 Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
 
-(** * Operational semantics *)
+(** * Parallel Semantics of bundles *)
 
 (** The semantics operates over a single mapping from registers
   (type [preg]) to values.  We maintain
@@ -695,7 +679,7 @@ Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm
 
 Open Scope asm.
 
-(** Undefining some registers *)
+(** *** Undefining some registers *)
 
 Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
   match l with
@@ -704,7 +688,7 @@ Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
   end.
 
 
-(** Assigning a register pair *)
+(** *** Assigning a register pair *)
 Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
   match p with
   | One r => rs#r <- v
@@ -712,7 +696,7 @@ Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
   end.
 
 
-(** Assigning the result of a builtin *)
+(** *** Assigning the result of a builtin *)
 
 Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   match res with
@@ -723,12 +707,8 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
 
 Local Open Scope asm.
 
-(** * Parallel Semantics of bundles *)
-
 Section RELSEM.
 
-(** Execution of arith instructions *)
-
 Variable ge: genv.
 
 (** The parallel semantics on bundles is purely small-step and defined as a relation
@@ -753,7 +733,7 @@ Inductive outcome: Type :=
   | Stuck
 .
 
-(** ** Arithmetic Expressions (including comparisons) *)
+(** *** Arithmetic Expressions (including comparisons) *)
 
 Inductive signedness: Type := Signed | Unsigned.
 
@@ -800,7 +780,7 @@ Definition notftest_for_cmp (c: comparison) :=
   | Cge => Normal FTult
   end.
 
-(* CoMPare Signed Words to Zero *)
+(* **** CoMPare Signed Words to Zero *)
 Definition btest_for_cmpswz (c: comparison) :=
   match c with
   | Cne => BTwnez
@@ -811,7 +791,7 @@ Definition btest_for_cmpswz (c: comparison) :=
   | Cgt => BTwgtz
   end.
 
-(* CoMPare Signed Doubles to Zero *)
+(* **** CoMPare Signed Doubles to Zero *)
 Definition btest_for_cmpsdz (c: comparison) :=
   match c with
   | Cne => BTdnez
@@ -849,7 +829,7 @@ Definition cmpu_for_btest (bt: btest) :=
   end.
 
 
-(* a few lemma on comparisons of unsigned (e.g. pointers) *)
+(* **** a few lemma on comparisons of unsigned (e.g. pointers) *)
 
 Definition Val_cmpu_bool cmp v1 v2: option bool :=
   Val.cmpu_bool (fun _ _ => true) cmp v1 v2.
@@ -901,7 +881,7 @@ Qed.
 
 
 
-(** Comparing integers *)
+(** **** Comparing integers *)
 Definition compare_int (t: itest) (v1 v2: val): val :=
   match t with
   | ITne  => Val.cmp Cne v1 v2
@@ -961,6 +941,8 @@ Definition compare_float (t: ftest) (v1 v2: val): val :=
   | FTult => Val.notbool (Val.cmpf Cge v1 v2)
   end.
 
+(** **** Arithmetic evaluators *)
+
 Definition arith_eval_r n :=
   match n with
   | Ploadsymbol s ofs => Genv.symbol_address ge s ofs
@@ -1212,7 +1194,7 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
 
 Definition eval_offset (ofs: offset) : res ptrofs := OK ofs.
 
-(** * load/store *)
+(** *** load/store instructions *)
 
 Definition parexec_incorrect_load trap chunk d rsw mw :=
   match trap with
@@ -1361,7 +1343,7 @@ Definition store_chunk n :=
   | Pfsd => Mfloat64
   end.
 
-(** * basic instructions *)
+(** ** Basic (instruction) step *)
 
 Definition bstep (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
   match bi with
@@ -1417,7 +1399,7 @@ Definition bstep (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
   | Pnop => Next rsw mw
 end.
 
-(* parexec with writes-in-order *)
+(** *** parexec with writes-in-order *)
 Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) :=
   match body with
   | nil => Next rsw mw
@@ -1428,7 +1410,7 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) :=
      end
   end.
 
-(** TODO: redundant w.r.t Machblock ?? *)
+(* TODO: redundant w.r.t Machblock ?? *)
 Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
 Proof.
   apply List.in_dec.
@@ -1437,7 +1419,7 @@ Qed.
 
 
 
-(** Note: copy-paste from Machblock *)
+(* Note: copy-paste from Machblock *)
 Definition is_label (lbl: label) (bb: bblock) : bool :=
   if in_dec lbl (header bb) then true else false.
 
@@ -1455,7 +1437,7 @@ Qed.
 
 
 
-(** convert a label into a position in the code *)
+(** **** convert a label into a position in the code *)
 Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z :=
   match lb with
   | nil => None
@@ -1472,11 +1454,9 @@ Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem)
       end
   end.
 
-(** Evaluating a branch 
+(** **** Parallel Evaluation of a branch *)
 
-Warning: in m PC is assumed to be already pointing on the next instruction !
-
-*)
+(** Warning: PC is assumed to be already pointing on the next bundle ! *)
 
 Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) (res: option bool) :=
   match res with
@@ -1486,72 +1466,54 @@ Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem)
   end.
 
 
-(* FIXME: comment not up-to-date for parallel semantics *)
-
-(** Execution of a single control-flow instruction [i] in initial state [rs] and
-    [m].  Return updated state.
-
-    As above: PC is assumed to be incremented on the next block before the control-flow instruction
-
-    For instructions that correspond tobuiltin
-    actual RISC-V instructions, the cases are straightforward
-    transliterations of the informal descriptions given in the RISC-V
-    user-mode specification.  For pseudo-instructions, refer to the
-    informal descriptions given above.
+(** **** Parallel execution of a control-flow instruction  *)
 
-    Note that we set to [Vundef] the registers used as temporaries by
-    the expansions of the pseudo-instructions, so that the RISC-V code
-    we generate cannot use those registers to hold values that must
-    survive the execution of the pseudo-instruction. *)
+(**  As above: PC is assumed to be incremented on the next block before the control-flow instruction
+*)
 
 Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) (mw: mem) :=
   match oc with
-  | Some ic =>
-(** Get/Set system registers *)
-  match ic with
-
-
-(** Branch Control Unit instructions *)
-  | Pret =>
+  | None => Next (rsw#PC <- (rsr#PC)) mw
+  | Some ic => (**r Branch Control Unit instructions *)
+    match ic with
+    | Pret =>
       Next (rsw#PC <- (rsr#RA)) mw
-  | Pcall s =>
+    | Pcall s =>
       Next (rsw#RA <- (rsr#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw
-  | Picall r =>
+    | Picall r =>
       Next (rsw#RA <- (rsr#PC) #PC <- (rsr#r)) mw
-  | Pjumptable r tbl =>
+    | Pjumptable r tbl =>
       match rsr#r with
       | Vint n =>
-          match list_nth_z tbl (Int.unsigned n) with
-          | None => Stuck
-          | Some lbl => par_goto_label f lbl rsr (rsw #GPR62 <- Vundef #GPR63 <- Vundef) mw
-          end
+        match list_nth_z tbl (Int.unsigned n) with
+        | None => Stuck
+        | Some lbl => par_goto_label f lbl rsr (rsw #GPR62 <- Vundef #GPR63 <- Vundef) mw
+        end
       | _ => Stuck
       end
-  | Pgoto s =>
+    | Pgoto s =>
       Next (rsw#PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw
-  | Pigoto r =>
+    | Pigoto r =>
       Next (rsw#PC <- (rsr#r)) mw
-  | Pj_l l =>
+    | Pj_l l =>
       par_goto_label f l rsr rsw mw
-  | Pcb bt r l =>
+    | Pcb bt r l =>
       match cmp_for_btest bt with
       | (Some c, Int)  => par_eval_branch f l rsr rsw mw (Val.cmp_bool c rsr#r (Vint (Int.repr 0)))
       | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val.cmpl_bool c rsr#r (Vlong (Int64.repr 0)))
       | (None, _) => Stuck
       end
-  | Pcbu bt r l => 
+    | Pcbu bt r l => 
       match cmpu_for_btest bt with
       | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val_cmpu_bool c rsr#r (Vint (Int.repr 0)))
       | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val_cmplu_bool c rsr#r (Vlong (Int64.repr 0)))
       | (None, _) => Stuck
       end
-
-(** Pseudo-instructions *)
-  | Pbuiltin ef args res =>
+    (**r Pseudo-instructions *)
+    | Pbuiltin ef args res =>
       Stuck (**r treated specially below *)
-  end
-  | None => Next (rsw#PC <- (rsr#PC)) mw
-end.
+    end
+  end.
 
 
 Definition incrPC size_b (rs: regset) :=
@@ -1567,7 +1529,7 @@ Definition parexec_wio f bdy ext size_b (rs: regset) (m: mem): outcome :=
   | Stuck => Stuck
   end.
 
-(** non-deterministic (out-of-order writes) parallel execution of bundles *)
+(** *** non-deterministic (out-of-order writes) parallel execution of bundles *)
 Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (o: outcome): Prop :=
    exists bdy1 bdy2, Permutation (bdy1++bdy2) (body bundle) /\ 
       o=match parexec_wio f bdy1 (exit bundle) (Ptrofs.repr (size bundle)) rs m with
@@ -1575,14 +1537,13 @@ Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (
       | Stuck => Stuck
       end.
 
-(** deterministic parallel (out-of-order writes) execution of bundles *)
+(** *** deterministic parallel (out-of-order writes) execution of bundles *)
 Definition det_parexec (f: function) (bundle: bblock) (rs: regset) (m: mem) rs' m': Prop :=
    forall o, parexec_bblock f bundle rs m o -> o = Next rs' m'.
 
 
-(* FIXME: comment not up-to-date *)
-(** Translation of the LTL/Linear/Mach view of machine registers to
-  the RISC-V view.  Note that no LTL register maps to [X31].  This
+(** *** Translation of the LTL/Linear/Mach view of machine registers to
+  the assembly view.  Note that no LTL register maps to [X31].  This
   register is reserved as temporary, to be used by the generated RV32G
   code.  *)
 
@@ -1605,7 +1566,7 @@ Definition preg_of (r: mreg) : preg :=
   | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63
   end.
 
-(** Undefine all registers except SP and callee-save registers *)
+(** **** Undefine all registers except SP and callee-save registers *)
 
 Definition undef_caller_save_regs (rs: regset) : regset :=
   fun r =>
@@ -1614,10 +1575,9 @@ Definition undef_caller_save_regs (rs: regset) : regset :=
     then rs r
     else Vundef.
 
-(* FIXME: comment not up-to-date *)
-(** Extract the values of the arguments of an external call.
+(** **** Extract the values of the arguments of an external call.
     We exploit the calling conventions from module [Conventions], except that
-    we use RISC-V registers instead of locations. *)
+    we use assembly registers instead of locations. *)
 
 Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
   | extcall_arg_reg: forall r,
@@ -1646,12 +1606,12 @@ Definition loc_external_result (sg: signature) : rpair preg :=
   map_rpair preg_of (loc_result sg).
 
 
-(** Looking up bblocks in a code sequence by position. *)
+(** ** Looking up bblocks in a code sequence by position. *)
 Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock :=
   match lb with
   | nil => None
   | b :: il => 
-    if zlt pos 0 then None  (* NOTE: It is impossible to branch inside a block *)
+    if zlt pos 0 then None  (*r NOTE: It is impossible to branch inside a block *)
     else if zeq pos 0 then Some b
     else find_bblock (pos - (size b)) il
   end.
@@ -1721,9 +1681,7 @@ Qed.
 
 End RELSEM.
 
-(** Execution of whole programs. *)
-
-(** Execution of whole programs. *)
+(** ** Execution of whole programs. *)
 
 Inductive initial_state (p: program): state -> Prop :=
   | initial_state_intro: forall m0,
diff --git a/kvx/PostpassScheduling.v b/kvx/PostpassScheduling.v
index 7518866d..1f1f238a 100644
--- a/kvx/PostpassScheduling.v
+++ b/kvx/PostpassScheduling.v
@@ -12,6 +12,8 @@
 (*                                                             *)
 (* *************************************************************)
 
+(** Implementation (and basic properties) of the verified postpass scheduler *)
+
 Require Import Coqlib Errors AST Integers.
 Require Import Asmblock Axioms Memory Globalenvs.
 Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops.
@@ -19,20 +21,13 @@ Require Peephole.
 
 Local Open Scope error_monad_scope.
 
-(** Oracle taking as input a basic block,
-    returns a schedule expressed as a list of bundles *)
+(** * Oracle taking as input a basic block,
+    returns a scheduled list of bundles *)
 Axiom schedule: bblock -> (list (list basic)) * option control.
 
 Extract Constant schedule => "PostpassSchedulingOracle.schedule".
 
-Definition state' := L.mem.
-Definition outcome' := option state'.
-
-Definition bblock' := L.bblock.
-
-Definition exec' := L.run.
-
-Definition exec := exec_bblock.
+(** * Concat all bundles into one big basic block *)
 
 (* Lemmas necessary for defining concat_all *)
 Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil.
@@ -49,8 +44,6 @@ Proof.
   - intros. rewrite <- app_comm_cons. discriminate.
 Qed.
 
-
-
 Definition check_size bb :=
   if zlt Ptrofs.max_unsigned (size bb)
     then Error (msg "PostpassSchedulingproof.check_size")
@@ -213,6 +206,8 @@ Qed.
 Inductive is_concat : bblock -> list bblock -> Prop :=
   | mk_is_concat: forall tbb lbb, concat_all lbb = OK tbb -> is_concat tbb lbb.
 
+(** * Remainder of the verified scheduler *)
+
 Definition verify_schedule (bb bb' : bblock) : res unit :=
   match bblock_simub bb bb' with
   | true => OK tt
diff --git a/kvx/lib/Machblock.v b/kvx/lib/Machblock.v
index 08e0eba2..edae0ed4 100644
--- a/kvx/lib/Machblock.v
+++ b/kvx/lib/Machblock.v
@@ -12,6 +12,8 @@
 (*                                                             *)
 (* *************************************************************)
 
+(** Abstract syntax and semantics of a Mach variant, structured with basic-blocks. *)
+
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
@@ -28,7 +30,9 @@ Require Stacklayout.
 Require Import Mach.
 Require Import Linking.
 
-(** basic instructions (ie no control-flow) *)
+(** * Abstract Syntax *)
+
+(** ** basic instructions (ie no control-flow) *)
 Inductive basic_inst: Type :=
   | MBgetstack: ptrofs -> typ -> mreg -> basic_inst
   | MBsetstack: mreg -> ptrofs -> typ -> basic_inst
@@ -40,7 +44,7 @@ Inductive basic_inst: Type :=
 
 Definition bblock_body := list basic_inst.
 
-(** control flow instructions *)
+(** ** control flow instructions *)
 Inductive control_flow_inst: Type :=
   | MBcall: signature -> mreg + ident -> control_flow_inst
   | MBtailcall: signature -> mreg + ident -> control_flow_inst
@@ -51,6 +55,7 @@ Inductive control_flow_inst: Type :=
   | MBreturn: control_flow_inst
   .
 
+(** ** basic block *)
 Record bblock := mk_bblock {
   header: list label;
   body:   bblock_body;
@@ -91,6 +96,8 @@ Proof.
   destruct e; try (simpl in He; discriminate); auto.
 Qed.
 
+(** ** programs *)
+
 Definition code := list bblock.
 
 Record function: Type := mkfunction
@@ -106,7 +113,7 @@ Definition program := AST.program fundef unit.
 
 Definition genv := Genv.t fundef unit.
 
-(*** sémantique ***)
+(** * Operational (blockstep) semantics ***)
 
 Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
 Proof.
@@ -155,7 +162,7 @@ Definition find_function_ptr
       Genv.find_symbol ge symb
   end.
 
-(** Machblock execution states. *)
+(** ** Machblock execution states. *)
 
 Inductive stackframe: Type :=
   | Stackframe:
diff --git a/kvx/lib/Machblockgen.v b/kvx/lib/Machblockgen.v
index 287e4f7b..ab186083 100644
--- a/kvx/lib/Machblockgen.v
+++ b/kvx/lib/Machblockgen.v
@@ -29,6 +29,8 @@ Require Import Mach.
 Require Import Linking.
 Require Import Machblock.
 
+(** * Tail-recursive (greedy) translation from Mach code to Machblock code *)
+
 Inductive Machblock_inst: Type :=
 | MB_label (lbl: label) 
 | MB_basic (bi: basic_inst)
@@ -71,9 +73,12 @@ Definition add_to_new_bblock (i:Machblock_inst) : bblock :=
   | MB_cfi i => cfi_bblock i
   end.
 
-(** Adding an instruction to the beginning of a bblock list
-  * Either adding the instruction to the head of the list,
-  * or create a new bblock with the instruction *)
+(** Adding an instruction to the beginning of a bblock list by
+
+- either adding the instruction to the head of the list,
+
+- or creating a new bblock with the instruction 
+*)
 Definition add_to_code (i:Machblock_inst) (bl:code) : code :=
   match bl with
   | bh::bl0 => match i with
@@ -112,7 +117,7 @@ Definition transf_program (src: Mach.program) : program :=
   transform_program transf_fundef src.
 
 
-(** Abstracting trans_code *)
+(** * Abstracting trans_code with a simpler inductive relation *)
 
 Inductive is_end_block: Machblock_inst -> code -> Prop :=
   | End_empty mbi: is_end_block mbi nil
-- 
cgit