Merge remote-tracking branch 'origin/kvx-work' into kvx-work-velus

18 files changed, 290 insertions, 255 deletions

diff --git a/config_kvx_elf.sh b/config_kvx_elf.sh
new file mode 100755
index 00000000..f1430417
--- /dev/null
+++ b/config_kvx_elf.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh kvx-elf "$@"
diff --git a/doc/index-kvx.html b/doc/index-kvx.html
index 95fdb6de..97eefc24 100644
--- a/doc/index-kvx.html
+++ b/doc/index-kvx.html
@@ -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>
 
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/InstructionScheduler.ml b/kvx/InstructionScheduler.ml
index e4dc3f97..eab0b21a 100644
--- a/kvx/InstructionScheduler.ml
+++ b/kvx/InstructionScheduler.ml
@@ -12,6 +12,16 @@
 (*                                                             *)
 (* *************************************************************)
 
+let with_destructor dtor stuff f =
+  try let ret = f stuff in
+      dtor stuff;
+      ret
+  with exn -> dtor stuff;
+              raise exn;;
+
+let with_out_channel chan f = with_destructor close_out chan f;;
+let with_in_channel chan f = with_destructor close_in chan f;;
+
 (** Schedule instructions on a synchronized pipeline
 @author David Monniaux, CNRS, VERIMAG *)
 
@@ -844,16 +854,15 @@ let pseudo_boolean_solver = ref "pb_solver"
 
 let pseudo_boolean_scheduler pb_type problem =
   try
-    let filename_in = "problem.opb"
-    (* needed only if not using stdout and filename_out = "problem.sol" *) in
-    let opb_problem = open_out filename_in in
-    let mapper = pseudo_boolean_print_problem opb_problem problem pb_type in
-    close_out opb_problem;
-    
-    let opb_solution = Unix.open_process_in (!pseudo_boolean_solver ^ " " ^ filename_in) in
-    let ret = adjust_check_solution mapper (pseudo_boolean_read_solution mapper opb_solution) in
-    close_in opb_solution;
-    Some ret
+    let filename_in = "problem.opb" in
+    (* needed only if not using stdout and filename_out = "problem.sol" *)
+    let mapper =
+      with_out_channel (open_out filename_in)
+        (fun opb_problem ->
+          pseudo_boolean_print_problem opb_problem problem pb_type) in
+    Some (with_in_channel
+      (Unix.open_process_in (!pseudo_boolean_solver ^ " " ^ filename_in))
+      (fun opb_solution -> adjust_check_solution mapper (pseudo_boolean_read_solution mapper opb_solution)))
   with
   | Unschedulable -> None;;
 				 
@@ -1193,23 +1202,23 @@ let ilp_read_solution mapper channel =
 let ilp_solver = ref "ilp_solver"
 
 let problem_nr = ref 0
-                             
+
 let ilp_scheduler pb_type problem =
   try
     let filename_in = Printf.sprintf  "problem%05d.lp" !problem_nr
     and filename_out = Printf.sprintf "problem%05d.sol" !problem_nr in
     incr problem_nr;
-    let opb_problem = open_out filename_in in
-    let mapper = ilp_print_problem opb_problem problem pb_type in
-    close_out opb_problem;
+    let mapper = with_out_channel (open_out filename_in)
+      (fun opb_problem -> ilp_print_problem opb_problem problem pb_type) in
 
     begin
       match Unix.system (!ilp_solver ^ " " ^ filename_in ^ " " ^ filename_out) with
       | Unix.WEXITED 0 ->
-         let opb_solution = open_in filename_out in
-         let ret = adjust_check_solution mapper (ilp_read_solution mapper opb_solution) in
-         close_in opb_solution;
-         Some ret
+         Some (with_in_channel
+                 (open_in filename_out)
+                 (fun opb_solution ->
+                   adjust_check_solution mapper
+                     (ilp_read_solution mapper opb_solution)))
       | Unix.WEXITED _ -> failwith "failed to start ilp solver"
       | _ -> None
     end
@@ -1245,3 +1254,10 @@ let cascaded_scheduler (problem : problem) =
      end;
      Some solution;;
 
+let scheduler_by_name name =
+  match name with
+  | "ilp" -> validated_scheduler cascaded_scheduler
+  | "list" -> validated_scheduler list_scheduler
+  | "revlist" -> validated_scheduler reverse_list_scheduler
+  | "greedy" -> greedy_scheduler
+  | s -> failwith ("unknown scheduler: " ^ s);;
diff --git a/kvx/InstructionScheduler.mli b/kvx/InstructionScheduler.mli
index f91c2d06..85e2a5c6 100644
--- a/kvx/InstructionScheduler.mli
+++ b/kvx/InstructionScheduler.mli
@@ -108,3 +108,6 @@ val smt_print_problem : out_channel -> problem -> unit;;
 val ilp_print_problem : out_channel -> problem -> pseudo_boolean_problem_type -> pseudo_boolean_mapper;;
 
 val ilp_scheduler : pseudo_boolean_problem_type -> problem -> solution option;;
+
+(** Schedule a problem using a scheduler given by a string name *)
+val scheduler_by_name : string -> problem -> int array option;;
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/PostpassSchedulingOracle.ml b/kvx/PostpassSchedulingOracle.ml
index 822c0dc0..2107ce22 100644
--- a/kvx/PostpassSchedulingOracle.ml
+++ b/kvx/PostpassSchedulingOracle.ml
@@ -504,8 +504,7 @@ let alu_lite_y : int array = let resmap = fun r -> match r with
   | Rissue -> 3 | Rtiny -> 1 | Rlite -> 1 |  _ -> 0
   in Array.of_list (List.map resmap resource_names)
 
-let alu_nop : int array = let resmap = fun r -> match r with 
-  | Rissue -> 1 | Rnop -> 1 | _ -> 0
+let alu_nop : int array = let resmap = fun r -> 0
   in Array.of_list (List.map resmap resource_names)
 
 let alu_tiny : int array = let resmap = fun r -> match r with
@@ -627,16 +626,16 @@ let rec_to_usage r =
                           | Some U27L5 | Some U27L10 -> alu_tiny_x 
                           | Some E27U27L10 -> alu_tiny_y 
                           | _ -> raise InvalidEncoding)
-  | Maddw -> (match encoding with None -> mau_auxr
+  | Maddw | Msbfw -> (match encoding with None -> mau_auxr
                 | Some U6 | Some S10 | Some U27L5 -> mau_auxr_x
                 | _ -> raise InvalidEncoding)
-  | Maddd -> (match encoding with None | Some U6 | Some S10 -> mau_auxr
+  | Maddd | Msbfd -> (match encoding with None | Some U6 | Some S10 -> mau_auxr
                 | Some U27L5 | Some U27L10 -> mau_auxr_x
                 | Some E27U27L10 -> mau_auxr_y)
-  | Mulw| Msbfw -> (match encoding with None -> mau
+  | Mulw -> (match encoding with None -> mau
                                 | Some U6 | Some S10 | Some U27L5 -> mau_x
                                 | _ -> raise InvalidEncoding)
-  | Muld | Msbfd -> (match encoding with None | Some U6 | Some S10 -> mau
+  | Muld -> (match encoding with None | Some U6 | Some S10 -> mau
                                 | Some U27L5 | Some U27L10 -> mau_x
                                 | Some E27U27L10 -> mau_y)
   | Nop -> alu_nop
@@ -914,19 +913,20 @@ let print_bb oc bb =
   let asm_instructions = Asm.unfold_bblock bb
   in List.iter (print_inst oc) asm_instructions
 
+let print_schedule sched =
+  print_string "[ ";
+  Array.iter (fun x -> Printf.printf "%d; " x) sched;
+  print_endline "]";;
+
 let do_schedule bb =
-  let problem = build_problem bb
-  in let solution = (if !Clflags.option_fpostpass_sched = "ilp" then
-                      validated_scheduler cascaded_scheduler
-                    else if !Clflags.option_fpostpass_sched = "list" then
-                      validated_scheduler list_scheduler
-                    else if !Clflags.option_fpostpass_sched = "revlist" then
-                      validated_scheduler reverse_list_scheduler
-                    else if !Clflags.option_fpostpass_sched = "greedy" then
-                      greedy_scheduler else failwith ("Invalid scheduler:" ^ !Clflags.option_fpostpass_sched)) problem
+  let problem = build_problem bb in
+  (if debug then print_problem stdout problem);
+  let solution = scheduler_by_name (!Clflags.option_fpostpass_sched) problem
   in match solution with
   | None -> failwith "Could not find a valid schedule"
-  | Some sol -> let bundles = bundlize_solution bb sol in 
+  | Some sol ->
+     ((if debug then print_schedule sol);
+     let bundles = bundlize_solution bb sol in 
       (if debug then
       begin
         Printf.eprintf "Scheduling the following group of instructions:\n";
@@ -935,7 +935,7 @@ let do_schedule bb =
         List.iter (print_bb stderr) bundles;
         Printf.eprintf "--------------------------------\n"
       end;
-      bundles)
+      bundles))
 
 (**
  * Dumb schedule if the above doesn't work
diff --git a/kvx/abstractbb/AbstractBasicBlocksDef.v b/kvx/abstractbb/AbstractBasicBlocksDef.v
index 0b1c502d..948ed660 100644
--- a/kvx/abstractbb/AbstractBasicBlocksDef.v
+++ b/kvx/abstractbb/AbstractBasicBlocksDef.v
@@ -45,7 +45,7 @@ End LangParam.
 
 
 
-(** * Syntax and (sequential) semantics of "basic blocks" *)
+(** * Syntax and (sequential) semantics of "abstract basic blocks" *)
 Module MkSeqLanguage(P: LangParam).
 
 Export P.
@@ -62,12 +62,12 @@ Definition assign (m: mem) (x:R.t) (v: value): mem
   := fun y => if R.eq_dec x y then v else m y.
 
 
-(** expressions *)
+(** Expressions *)
 
 Inductive exp :=
-  | PReg (x:R.t)
-  | Op (o:op) (le: list_exp)
-  | Old (e: exp)
+  | PReg (x:R.t)              (**r pseudo-register *)
+  | Op (o:op) (le: list_exp)  (**r operation *)
+  | Old (e: exp)              (**r evaluation of [e] in the initial state of the instruction (see [inst] below) *)
 with list_exp :=
   | Enil
   | Econs (e:exp) (le:list_exp)
@@ -95,7 +95,8 @@ with list_exp_eval (le: list_exp) (m old: mem): option (list value) :=
   | LOld le => list_exp_eval le old old
   end.
 
-Definition inst := list (R.t * exp). (* = a sequence of assignments *) 
+(** An instruction represents a sequence of assignments where [Old] refers to the initial state of the sequence. *) 
+Definition inst := list (R.t * exp). 
 
 Fixpoint inst_run (i: inst) (m old: mem): option mem :=
   match i with
@@ -107,6 +108,7 @@ Fixpoint inst_run (i: inst) (m old: mem): option mem :=
      end
   end.
 
+(** A basic block is a sequence of instructions. *) 
 Definition bblock := list inst.
 
 Fixpoint run (p: bblock) (m: mem): option mem :=
@@ -250,12 +252,16 @@ Qed.
 
 End SEQLANG.
 
-Module Terms.
 
-(** terms in the symbolic evaluation 
-NB: such a term represents the successive computations in one given pseudo-register
+(** * Terms in the symbolic execution *)
+
+(** Such a term represents the successive computations in one given pseudo-register. 
+The [hid] has no formal semantics: it is only used by the hash-consing oracle (itself dynamically checked to behave like an identity function).
+
 *)
 
+Module Terms.
+
 Inductive term :=
   | Input (x:R.t) (hid:hashcode)
   | App (o: op) (l: list_term) (hid:hashcode)
@@ -334,11 +340,21 @@ Proof.
   - rewrite IHl; clear IHl. intuition (congruence || eauto).
 Qed.
 
+(** * Rewriting rules in the symbolic execution *)
+
+(** The symbolic execution is parametrized by rewriting rules on pseudo-terms. *)
+
 Record pseudo_term: Type := intro_fail {
   mayfail: list term;
   effect: term
 }.
 
+(** Simulation relation between a term and a pseudo-term *)
+
+Definition match_pt (t: term) (pt: pseudo_term) :=
+      (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m)
+   /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1).
+
 Lemma inf_option_equivalence (A:Type) (o1 o2: option A):
   (o1 <> None -> o1 = o2) <-> (forall m1, o1 = Some m1 -> o2 = Some m1).
 Proof.
@@ -346,10 +362,6 @@ Proof.
   symmetry; eauto.
 Qed.
 
-Definition match_pt (t: term) (pt: pseudo_term) :=
-      (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m)
-   /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1).
-
 Lemma intro_fail_correct (l: list term) (t: term) :
    (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t).
 Proof.
@@ -357,6 +369,7 @@ Proof.
 Qed.
 Hint Resolve intro_fail_correct: wlp.
 
+(** The default reduction of a term to a pseudo-term *) 
 Definition identity_fail (t: term):= intro_fail [t] t.
 
 Lemma identity_fail_correct (t: term): match_pt t (identity_fail t).
@@ -366,6 +379,7 @@ Qed.
 Global Opaque identity_fail.
 Hint Resolve identity_fail_correct: wlp.
 
+(** The reduction for constant term *) 
 Definition nofail (is_constant: op -> bool) (t: term):=
     match t with
     | Input x _ => intro_fail ([])%list t
@@ -385,6 +399,7 @@ Qed.
 Global Opaque nofail.
 Hint Resolve nofail_correct: wlp.
 
+(** Term equivalence preserve the simulation by pseudo-terms *)
 Definition term_equiv t1 t2:= forall ge m, term_eval ge t1 m = term_eval ge t2 m.
 
 Global Instance term_equiv_Equivalence : Equivalence term_equiv.
@@ -401,6 +416,7 @@ Proof.
 Qed.
 Hint Resolve match_pt_term_equiv: wlp.
 
+(** Other generic reductions *)
 Definition app_fail (l: list term) (pt: pseudo_term): pseudo_term :=
   {| mayfail := List.rev_append l pt.(mayfail); effect := pt.(effect) |}.
 
@@ -431,6 +447,8 @@ Extraction Inline app_fail.
 Import ImpCore.Notations.
 Local Open Scope impure_scope.
 
+(** Specification of rewriting functions in parameter of the symbolic execution: in the impure monad, because the rewriting functions produce hash-consed terms (wrapped in pseudo-terms).
+*)
 Record reduction:= {
   result:> term -> ?? pseudo_term;
   result_correct: forall t, WHEN result t ~> pt THEN match_pt t pt;
diff --git a/kvx/abstractbb/ImpSimuTest.v b/kvx/abstractbb/ImpSimuTest.v
index c914eee1..89260ddb 100644
--- a/kvx/abstractbb/ImpSimuTest.v
+++ b/kvx/abstractbb/ImpSimuTest.v
@@ -10,13 +10,16 @@
 (*                                                             *)
 (* *************************************************************)
 
-(** Implementation of a symbolic execution of sequential semantics of Abstract Basic Blocks
+(** Implementation of a simulation test (ie a "scheduling verifier") for the sequential semantics of Abstract Basic Blocks.
+
+It is based on a symbolic execution procedure of Abstract Basic Blocks with imperative hash-consing and rewriting.
+
+It also provides debugging information when the test fails.
 
-with imperative hash-consing, and rewriting.
 
 *)
 
-Require Export Impure.ImpHCons.
+Require Export Impure.ImpHCons. (**r Import the Impure library. See https://github.com/boulme/ImpureDemo *)
 Export Notations.
 Import HConsing.
 
@@ -32,6 +35,7 @@ Import ListNotations.
 Local Open Scope list_scope.
 
 
+(** * Interface of (impure) equality tests for operators *)
 Module Type ImpParam.
 
 Include LangParam.
@@ -54,6 +58,8 @@ Include MkSeqLanguage LP.
 End ISeqLanguage.
 
 
+(** * A generic dictinary on PseudoRegisters with an impure equality test  *)
+
 Module Type ImpDict.
 
 Declare Module R: PseudoRegisters.
@@ -91,26 +97,27 @@ Parameter eq_test_correct: forall A (d1 d2: t A),
 
 (* NB: we could also take an eq_test on R.t (but not really useful with "pure" dictionaries  *)
 
-
-(* only for debugging *)
+(** only for debugging *)
 Parameter not_eq_witness: forall {A}, t A -> t A -> ?? option R.t.
 
 End ImpDict.
 
 
+(** * Specification of the provided tests *)
 Module Type ImpSimuInterface.
 
 Declare Module CoreL: ISeqLanguage.
 Import CoreL.
 Import Terms.
 
+(** the silent test (without debugging informations) *)
 Parameter bblock_simu_test: reduction -> bblock -> bblock -> ?? bool.
 
 Parameter bblock_simu_test_correct: forall reduce (p1 p2 : bblock),
     WHEN bblock_simu_test reduce p1 p2 ~> b
     THEN b = true -> forall ge : genv, bblock_simu ge p1 p2.
 
-
+(** the verbose test extended with debugging informations *)
 Parameter verb_bblock_simu_test
      : reduction ->
        (R.t -> ?? pstring) ->
@@ -127,6 +134,7 @@ Parameter verb_bblock_simu_test_correct:
 End ImpSimuInterface.
 
 
+(** * Implementation of the provided tests *)
 
 Module ImpSimu (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R): ImpSimuInterface with Module CoreL := L.
 
@@ -168,7 +176,7 @@ Section SimuWithReduce.
 
 Variable reduce: reduction.
 
-Section CanonBuilding.
+Section CanonBuilding. (** Implementation of the symbolic execution (ie a "canonical form" representing the semantics of an abstract basic block) *)
 
 Variable hC_term: hashinfo term -> ?? term.
 Hypothesis hC_term_correct: forall t, WHEN hC_term t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m.
@@ -1117,9 +1125,9 @@ Extraction Inline lift.
 
 End ImpSimu.
 
-Require Import FMapPositive.
-
 
+(** * Implementation of the Dictionary (based on PositiveMap) *)
+Require Import FMapPositive.
 Require Import PArith.
 Require Import FMapPositive.
 
@@ -1206,7 +1214,7 @@ Proof.
 Qed.
 Global Opaque eq_test.
 
-(* ONLY FOR DEBUGGING INFO: get some key of a non-empty d *)
+(** ONLY FOR DEBUGGING INFO: get some key of a non-empty d *)
 Fixpoint pick {A} (d: t A): ?? R.t :=
   match d with
   | Leaf _ => FAILWITH "unexpected empty dictionary"
@@ -1219,7 +1227,7 @@ Fixpoint pick {A} (d: t A): ?? R.t :=
     RET (xO p)
   end.
 
-(* ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *)
+(** ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *)
 Fixpoint not_eq_witness {A} (d1 d2: t A): ?? option R.t :=
   match d1, d2 with
   | Leaf _, Leaf _ => RET None
diff --git a/kvx/abstractbb/Parallelizability.v b/kvx/abstractbb/Parallelizability.v
index feebeee5..79ec9038 100644
--- a/kvx/abstractbb/Parallelizability.v
+++ b/kvx/abstractbb/Parallelizability.v
@@ -26,7 +26,7 @@ Require Import Sorting.Permutation.
 Require Import Bool.
 Local Open Scope lazy_bool_scope.
 
-
+(** * Definition of the parallel semantics *)
 Module ParallelSemantics (L: SeqLanguage).
 
 Export L.
@@ -590,17 +590,17 @@ End PARALLELI.
 End ParallelizablityChecking.
 
 
-Module Type PseudoRegSet.
-
-Declare Module R: PseudoRegisters.
-
-(** We assume a datatype [t] refining (list R.t)
+(** * We assume a datatype [PseudoRegSet.t] refining [list R.t] *)
 
+(** 
 This data-refinement is given by an abstract "invariant" match_frame below, 
 preserved by the following operations.
-
 *)
 
+Module Type PseudoRegSet.
+
+Declare Module R: PseudoRegisters.
+
 Parameter t: Type.
 Parameter match_frame: t -> (list R.t) -> Prop.
 
@@ -716,6 +716,11 @@ End ParallelChecks.
 
 
 
+(** * Implementing the datatype [PosPseudoRegSet.t] refining [list R.t] *)
+
+(* This data-refinement is given by an abstract "invariant" match_frame below, 
+preserved by the following operations.
+*)
 
 Require Import PArith.
 Require Import MSets.MSetPositive.
@@ -724,12 +729,6 @@ Module PosPseudoRegSet <: PseudoRegSet with Module R:=Pos.
 
 Module R:=Pos.
 
-(** We assume a datatype [t] refining (list R.t)
-
-This data-refinement is given by an abstract "invariant" match_frame below, 
-preserved by the following operations.
-
-*)
 
 Definition t:=PositiveSet.t.
 
diff --git a/kvx/abstractbb/SeqSimuTheory.v b/kvx/abstractbb/SeqSimuTheory.v
index 61f8f2ec..a957c50a 100644
--- a/kvx/abstractbb/SeqSimuTheory.v
+++ b/kvx/abstractbb/SeqSimuTheory.v
@@ -55,13 +55,14 @@ with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) :
     end
   end.
 
-(* the symbolic memory:
-  - pre: pre-condition expressing that the computation has not yet abort on a None.
-  - post: the post-condition for each pseudo-register 
-*)
-Record smem:= {pre: genv -> mem -> Prop; post:> R.t -> term}.
-
-(** initial symbolic memory *)
+(** The (abstract) symbolic memory state *)
+Record smem :=
+{
+   pre: genv -> mem -> Prop; (**r pre-condition expressing that the computation has not yet abort on a None. *)
+   post:> R.t -> term (**r the output term computed on each pseudo-register *)
+}.
+
+(** Initial symbolic memory state *)
 Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}.
 
 Fixpoint exp_term (e: exp) (d old: smem) : term :=
@@ -78,11 +79,12 @@ with list_exp_term (le: list_exp) (d old: smem) : list_term :=
   end.
 
 
-(** assignment of the symbolic memory *)
+(** assignment of the symbolic memory state *)
 Definition smem_set (d:smem) x (t:term) := 
   {| pre:=(fun ge m => (term_eval ge (d x) m) <> None /\ (d.(pre) ge m));
      post:=fun y => if R.eq_dec x y then t else d y |}.
 
+(** Simulation theory: the theorem [bblock_smem_simu] ensures that the simulation between two abstract basic blocks is implied by the simulation between their symbolic execution. *)
 Section SIMU_THEORY.
 
 Variable ge: genv.
@@ -375,8 +377,7 @@ Qed.
 
 End SIMU_THEORY.
 
-(** REMARKS: more abstract formulation of the proof... 
-    but relying on functional_extensionality.
+(** REMARK: this theorem reformulates the lemma above in a more abstract way (but relies on functional_extensionality axiom).
 *)
 Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:=
    forall m', om=Some m' <-> (d.(pre) ge m /\ forall x, term_eval ge (d x) m = Some (m' x)).
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
diff --git a/test/monniaux/scheduling/mal_schedule.c b/test/monniaux/scheduling/mal_schedule.c
new file mode 100644
index 00000000..a6ba967f
--- /dev/null
+++ b/test/monniaux/scheduling/mal_schedule.c
@@ -0,0 +1,14 @@
+#include <stdint.h>
+int16_t meuh;
+extern int uv_encode(double, double, int);
+void f(int *ab, int e) {
+  uint32_t *ao = (uint32_t *)ab;
+  int16_t *aq = &meuh;
+  while (e) {
+    int ar, as;
+    ar = 1. / 2147483647;
+    as = uv_encode(5, *aq, *ab);
+    if (as)
+      *ao++ = ar;
+  }
+}
diff --git a/test/monniaux/yarpgen/Makefile b/test/monniaux/yarpgen/Makefile
index c790d6e9..24dd19c3 100644
--- a/test/monniaux/yarpgen/Makefile
+++ b/test/monniaux/yarpgen/Makefile
@@ -16,7 +16,7 @@ YARPGEN+=-m $(BITS)
 CFLAGS+=-m$(BITS)
 endif
 
-MAX=19 # AUXR bug should be 129
+MAX=129
 PREFIX=ran%06.f
 
 CCOMPOPTS=-static