Library mcertikos.multicore.semantics.SplitSemImpl

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Events.
Require Import Globalenvs.
Require Import Conventions.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import Smallstep.
Require Import CommonTactic.
Require Import Coq.Logic.FunctionalExtensionality.

Require Import AuxFunctions.
Require Import LAsm.
Require Import GlobalOracle.
Require Import liblayers.compat.CompatLayers.
Require Import MBoot.
Require Import RealParams.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Decision.
Require Import LAsmModuleSem.
Require Import Soundness.
Require Import CompatExternalCalls.
Require Import LinkTactic.
Require Import I64Layer.
Require Import StencilImpl.
Require Import MakeProgram.
Require Import MakeProgramImpl.
Require Import LAsmModuleSemAux.

Require Import Concurrent_Linking_Lib.
Require Import Concurrent_Linking_Def.
Require Import Concurrent_Linking_Prop.
Require Import HWSemImpl.
Require Import ConcurrentOracle.

Require Import Machregs.
Require Import DeviceStateDataType.
Require Import liblayers.compat.CompatGenSem.
Require Import FutureTactic.

Section SPLITSEM.

  Context `{Hmem: Mem.MemoryModelX}.
  Context `{Hmwd: UseMemWithData mem}.
  Context `{real_params: RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.

  Notation LDATA := RData.
  Notation LDATAOps := (cdata (cdata_ops := mboot_data_ops) LDATA).

  Local Open Scope Z_scope.

  Context `{pmap: PartialMap}.
  Context `{fair: Fairness}.
  Context `{zset_op: ZSet_operation}.

  Existing Instance hdseting.
  Existing Instance op_reorder.

  Context `{mc_oracle: !MCLinkOracle}.
  Context `{mc_oracle_cond: !MCLinkOracleCond}.

  Section WITH_GE.

    Variables (ge: genv) (sten: stencil) (M: module).
    Context {Hmakege: make_globalenv (module_ops:= LAsm.module_ops) (mkp_ops:= make_program_ops)
                                     sten M (mboot ⊕ L64) = ret ge}.

    Local Obligation Tactic := intros.

    Definition hdsem_instance := @hdsem mem memory_model_ops Hmem Hmwd real_params_ops oracle_ops0
                                        oracle_ops big_ops builtin_idents_norepet_prf ge sten M Hmakege.

    Definition single_split_step_aux :=
      @single_split_step zset_op hdseting op_general hdsem_instance
                         fair current_CPU_ID single_oracle.

    Inductive single_split_step_aux_ge : genv → srstate → trace → srstate → Prop :=
    | single_split_step_aux_ge_intro :
        ∀ s t s´,
          single_split_step_aux s t s´ → single_split_step_aux_ge ge s t s´.

    Inductive single_split_initial_state (p: AST.program fundef unit):
      (srstate (hdset := hdseting)) → Prop :=
    | initial_split_state_intro:
        ∀ (m0: mwd LDATAOps),
          Genv.init_mem p = Some m0 →
          let ge := Genv.globalenv p in
          let rs0 :=
              (Pregmap.init Vundef)
                # Asm.PC <- (symbol_offset ge p.(prog_main) Int.zero)
                # ESP <- Vzero in
          single_split_initial_state p (SRState (Asm.State rs0 m0) nil nil).

    Definition single_split_final_state (s : srstate (hdset := hdseting)) (i : int) : Prop :=
      False.

    Definition single_split_semantics (p: program) :=
      Smallstep.Semantics single_split_step_aux_ge (single_split_initial_state p)
                          single_split_final_state (Genv.globalenv p).

    Ltac subst_except v :=
      repeat match goal with
             | [ H: v = _ |- _ ] ⇒ generalize H; clear H
             | [ H: _ = v |- _ ] ⇒ generalize H; clear H
             end; subst; intros.

    Ltac clear_eq v :=
      repeat match goal with
             | [ H: v = _ |- _ ] ⇒ clear H
             | [ H: _ = v |- _ ] ⇒ clear H
             end.

    Lemma single_split_semantics_single_events:
      ∀ p, single_events (single_split_semantics p).
    Proof.
      intros p s t s´ Hstep; inversion Hstep; substx; auto.
      - inversion H.
        inversion Hlocal; simpl; omega.
        simpl; omega.
    Qed.

    Lemma single_split_semantics_receptive (pl: program):
      receptive (single_split_semantics pl).
    Proof.
      intros; constructor.
      - inversion 1.
        inversion H0.
        + substx; try solve [inversion 1; substx; eauto].
          intros.
          inversion H8; substx.
          ∃ s1.
          simpl.
          unfold single_split_step_aux.
          simpl in H1.
          rewrite <- H1.
          eapply single_split_step_aux_ge_intro.
          unfold single_split_step_aux.
          rewrite <- H7.
          eapply single_exec_step_progress_split_local; eauto.
        + substx; try solve [inversion 1; substx; eauto].
          intros.
          inversion H8; substx.
          ∃ s1.
          simpl.
          unfold single_split_step_aux.
          simpl in H1.
          rewrite <- H1.
          eapply single_split_step_aux_ge_intro.
          unfold single_split_step_aux.
          rewrite <- H7.
          eapply single_exec_step_progress_split_log; eauto.
      - eapply single_split_semantics_single_events.
    Qed.

    Lemma single_split_semantics_determinate (pl: program):
      determinate (single_split_semantics pl).
    Proof.
      econstructor.
      - simpl in ×.
        simpl.
        intros s t1 s1 t2 s2 Hs1 Hs2.
        inversion Hs1; inversion Hs2; subst_except ge; clear Hs1 Hs2.
        rename H into Hs1, H4 into Hs2; unfold single_split_step_aux in ×.
        assert (t1 = E0 ∧ t2 = E0 ∧ s1 = s2) as Hs.
        {
          eapply single_split_determ.
          + exact Hs1.
          + exact Hs2.
        }
        destruct Hs as (Ht1 & Ht2 & Hs).
        split; eauto.
        rewrite Ht1, Ht2.
        constructor.
      - eapply single_split_semantics_single_events.
      - intros.
        simpl in ×.
        inv H; inv H0.
        unfold ge0, rs0, ge1, rs1.
        simpl in ×.
        rewrite H1 in H; inv H.
        eauto.
      - intros; simpl in ×.
        inv H.
      - intros.
        simpl in ×.
        inv H.
    Qed.

  End WITH_GE.

End SPLITSEM.