From 2e39ecb491bbd001ecdfba73115bc76e3f53f517 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 29 Jul 2020 09:17:26 +0200 Subject: Improving the coqdoc --- kvx/PostpassScheduling.v | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) (limited to 'kvx/PostpassScheduling.v') 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 -- cgit