Module FinalTheorem

Require Import mathcomp.ssreflect.fintype mathcomp.ssreflect.ssrnat.

Require Import Coqlib Axioms Errors.

Require Import InteractionSemantics GAST GlobSemantics Blockset ReachClose DRF SeqCorrect.

Require Import Soundness.

Require Import LangProps ClightLang AsmIDTransCorrect CompCorrect.

Import Compositionality.

Final Theorem of SC compilation

This file defines the final theorem of the ClightSC compiler.
Which says if we have n cminor modules c_1,...,c_n and a module obj for object implementations, and the linked program P_s = Let (c_1, ..., c_n, obj) In (f_1 || ... || f_m) is safe and drf, then if we compile each c_i separately using compcert to t_i, the target program P_t = Let (t_1, ..., t_n, obj) In (f_1 || ... || f_m) refines P_s.

Case 1: Object is implemented in x86-SC assembly

Two languages: Clight and x86 ASM
Definition NL := 2%nat.

Program Definition id0 : 'I_NL := @Ordinal NL 0 _.
Program Definition id1 : 'I_NL := @Ordinal NL 1 _.

Program Definition L (i: 'I_NL): Language :=
  if eqn i 0 then Clight_IS_2
  else AsmLang.

Lemma L_sound_1: L id0 = Clight_IS_2.
Proof.
Lemma L_sound_2: L id1 = AsmLang.
Proof.
Lemma eq_ord: forall i:'I_NL,
    i = id0 \/ i = id1.
Proof.

Section ClightSC_Compilation_correctness.
  Variable (clight_units: @cunits NL L).
  Variable (compiled_units: @cunits NL L).
  Variable (asm_units: @cunits NL L).
  Let scunits:= clight_units ++ asm_units.
  Let tcunits:= compiled_units ++ asm_units.
  Variable e: @entries.
  Definition cm_comps : @gcomp NL L :=
    List.repeat (Build_seq_comp_i NL L id0 id1 clight_trans)
                (List.length clight_units).

  Definition asm_comps: @gcomp NL L :=
    List.repeat (Build_seq_comp_i NL L id1 id1 id_trans_asm)
                (List.length asm_units).
Hypothesis 1: modules are reach-closed
  Hypothesis Hrc : rc_cunits scunits.
Hypothesis 2: compilation units are compiled by comps
  Hypotheses (Hcomp_cminor: cunits_transf cm_comps clight_units compiled_units).
  Hypotheses (Hcomp_asm: cunits_transf asm_comps asm_units asm_units).
Hypothesis 3: whole source program is safe and data-race-free
  Hypothesis (Hdrf: drf (scunits, e)).
  Hypothesis (Hsafe: safe_prog (scunits, e)).
  
  Definition comps: @gcomp NL L := cm_comps ++ asm_comps.

  Lemma Hwd_src: wd_langs scunits.
Proof.
    
  Lemma Hwd_tgt: wd_langs tcunits.
Proof.
  
  Lemma Hdet_tgt: det_langs tcunits.
Proof.

  Lemma Hcomp: cunits_transf comps scunits tcunits.
Proof.
  
  Lemma Hcorrect: seqs_correct comps.
Proof.
  
  Theorem refinement:
    prog_refine (scunits, e) (tcunits, e).
Proof.
End ClightSC_Compilation_correctness.


Check refinement.
rc_cunits : source modules are reach-closed
cunits_transf (cm_comps clight_units) clight_units compiled_units : compiled_units are x86 assembly units that compiled from clight_units by CompCert passes
cunits_transf (asm_comps asm_units) asm_units asm_units: asm_units are identically translated
drf (clight_units ++ asm_units, e): source program is data-race free
safe_prog (clight_units ++ asm_unit, e): source program is safe
prog_refine (clight_units ++ asm_units, e) (compiled_units ++ asm_units, e): there is event trace refinement between source and target programs


Case 2: Object is implemented in CImp language (Thm. 14)

Require Import Languages SpecLangIDtrans.

Section ClightSC_Compilation_Correctness_with_Object.
M Clight modules, 1 object spec module, and N threads
  Variable (M: nat).
  Variable (cl_units: @cunits NL L).
  Variable (compiled_units: @cunits NL L).
  Variable (spec_unit: @cunit NL L).
construct source compilation units
  Let scunits:= spec_unit :: cl_units.
  Let tcunits:= spec_unit :: compiled_units.
  Variable e: @entries.
construct compilers using compcert and id
  Definition cl_comps : @gcomp NL L :=
    List.repeat (Build_seq_comp_i NL L id0 id1 clight_trans) M.
  Definition id_comp: @seq_comp_i NL L :=
    (Build_seq_comp_i NL L id2 id2 id_trans_speclang).

Hypothesis 1: modules are reach-closed
  Hypothesis Hrc : rc_cunits scunits.
Hypothesis 2: compilation units are compiled by comps
  Hypotheses (Hcomp_clight: cunits_transf cl_comps cl_units compiled_units).
  Hypotheses (Hcomp_spec: cunit_transf id_comp spec_unit spec_unit).
Hypothesis 3: whole source program is safe and data-race-free
  Hypothesis (Hdrf: drf (scunits, e)).
  Hypothesis (Hsafe: safe_prog (scunits, e)).

construct compilers
  Definition comps': @gcomp NL L := id_comp :: cl_comps.

  Lemma Hwd_src': wd_langs scunits.
Proof.
    
  Lemma Hwd_tgt': wd_langs tcunits.
Proof.
  
  Lemma Hdet_tgt': det_langs tcunits.
Proof.

  Lemma Hcomp': cunits_transf comps' scunits tcunits.
Proof.
  
compilers are correct w.r.t. seqcorrect
proved by compcert correctness and CImp id_trans correctness
  Lemma Hcorrect': seqs_correct comps'.
Proof.

The refinement theorem
  Theorem refinement_sc:
    prog_refine (scunits, e) (tcunits, e).
Proof.
  
End ClightSC_Compilation_Correctness_with_Object.

Lemma seq_comp_i_eq:
  forall NL L id1 id2 comp comp',
    @Build_seq_comp_i NL L id1 id2 comp =
    @Build_seq_comp_i NL L id1 id2 comp' ->
    comp = comp'.
Proof.




Theorem 14 in paper

i.e. CompCert along with identity transformation of CImp are correct as a whole for compiling concurrent programs. Note here we made number of Clight modules M explicit for the convenience of defining separated compilation of each module

Definition CompCert_CImpID (M: nat) : gcomp := id_comp :: cl_comps M.

Theorem GCorrect_compcert_CImpID:
  forall M, gcorrect (CompCert_CImpID M).
Proof.