Library mcertikos.ipc.PHThreadCode

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import PHThread.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import IPCIntroGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CalRealProcModule.
Require Import CLemmas.
Require Import TacticsForTesting.
Require Import CalRealProcModule.
Require Import AbstractDataType.
Require Import PHThreadCSource.
Require Import ObjSyncIPC.
Require Import CommonTactic.

Require Export ObjTMVMM.
Require Export ObjTMSCHED.
Require Export ObjTMINTELVIRT.
Require Export ObjTMIPCDEVPRIM.
Require Export ObjTMVMXINIT.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Module PIPCINTROCODE.

  Section WithPrimitives.

    Context `{single_oracle_prop: SingleOracleProp}.
    Context `{real_params : RealParams}.
    Context `{multi_oracle_prop: MultiOracleProp}.

    Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
    Context `{Hmwd: UseMemWithData memb}.

    Let mem := mwd (cdata RData).

    Context `{Hstencil: Stencil}.
    Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
    Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.

    Section SYNCSENDTOCHANPRE.

      Let L: compatlayer (cdata RData) :=
        acquire_lock_CHAN ↦ gensem big2_acquire_lock_SC_spec
                          ⊕ get_sync_chan_busy ↦ gensem thread_get_sync_chan_busy_spec
                          ⊕ set_sync_chan_busy ↦ gensem thread_set_sync_chan_busy_spec
                          ⊕ thread_sleep ↦ gensem big2_thread_sleep_spec.

      Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.

      Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.

      Section SyncSendToChanPreBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

        Variable (ge: genv)
                 (STENCIL_MATCHES: stencil_matches sc ge).

        Variable bacquire_lock_CHAN: block.

        Hypothesis hacquire_lock_CHAN1 : Genv.find_symbol ge acquire_lock_CHAN = Some bacquire_lock_CHAN.

        Hypothesis hacquire_lock_CHAN2 :
          Genv.find_funct_ptr ge bacquire_lock_CHAN
          = Some (External (EF_external acquire_lock_CHAN
                                        (signature_of_type (Tcons tint Tnil) tvoid cc_default))
                           (Tcons tint Tnil) tvoid cc_default).

        Variable bget_sync_chan_busy: block.

        Hypothesis hget_sync_chan_busy1 : Genv.find_symbol ge get_sync_chan_busy = Some bget_sync_chan_busy.

        Hypothesis hget_sync_chan_busy2 :
          Genv.find_funct_ptr ge bget_sync_chan_busy
          = Some (External (EF_external get_sync_chan_busy
                                        (signature_of_type (Tcons tint Tnil) tint cc_default))
                           (Tcons tint Tnil) tint cc_default).

        Variable bset_sync_chan_busy: block.

        Hypothesis hset_sync_chan_busy1 : Genv.find_symbol ge set_sync_chan_busy = Some bset_sync_chan_busy.

        Hypothesis hset_sync_chan_busy2 :
          Genv.find_funct_ptr ge bset_sync_chan_busy
          = Some (External (EF_external set_sync_chan_busy
                                        (signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
                           (Tcons tint (Tcons tint Tnil)) tvoid cc_default).

        Variable bthread_sleep: block.

        Hypothesis hthread_sleep1 : Genv.find_symbol ge thread_sleep = Some bthread_sleep.

        Hypothesis hthread_sleep2 :
          Genv.find_funct_ptr ge bthread_sleep
          = Some (External (EF_external thread_sleep
                                        (signature_of_type (Tcons tint Tnil) tvoid cc_default))
                           (Tcons tint Tnil) tvoid cc_default).

        Lemma big_acquire_lock_SC_spec_preserve:
          ∀ x d d´,
            ikern d = true →
            ihost d = true →
            ipt d = true →
            pg d = true →
            big2_acquire_lock_SC_spec x d = Some d´ →
            ikern d´ = true ∧
            ihost d´ = true ∧
            ipt d´ = true ∧
            pg d´ = true ∧
            CPU_ID d = CPU_ID d´ ∧
            init d = true ∧
            init d´ = true ∧
            
            BigLogThreadConfigFunction.B_inLock (CPU_ID d´) (big_log d´) = true.
        Proof.
          intros.
          unfold big2_acquire_lock_SC_spec in H3; subdestruct; inv H3; simpl in *; rewrite zeq_true; tauto.
        Qed.

        Lemma syncsendto_chan_pre_body_correct:
          ∀ m d d´ env le chid,
            env = PTree.empty _
            → PTree.get _chid le = Some (Vint chid)
            → high_level_invariant d
            → thread_syncsendto_chan_pre_spec (Int.unsigned chid) d = Some d´
            → ∃ le´,
                 exec_stmt ge env le ((m, d): mem) syncsendto_chan_pre_body E0 le´
                                      (m, d´) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syncsendto_chan_pre_body.
          functional inversion H2; subst.

          - unfold cpu, curid, chid0, slp_q_id in ×.
            generalize H9; intro tmp; eapply big_acquire_lock_SC_spec_preserve in tmp; eauto.
            destruct tmp as (ikern0 & ihost0 & ipt0 & pg0 & CPU_ID_eq0 & init_a & init_b & inlock0).
            Opaque Z.add Z.mul.
            esplit.
            repeat vcgen.
            unfold thread_get_sync_chan_busy_spec; simpl.
            unfold ObjCV.get_sync_chan_busy_spec.
            rewrite ikern0, ihost0, pg0, ipt0, H10, init_b, inlock0.

            simpl in ×.
            rewrite zle_lt_true by omega.
            reflexivity.
            discharge_cmp.
            repeat vcgen.
            unfold thread_set_sync_chan_busy_spec; simpl.
            unfold ObjCV.set_sync_chan_busy_spec; simpl.
            simpl in ×.
            rewrite ikern0, ihost0, pg0, ipt0, H10, init_b, inlock0.
            rewrite zle_lt_true by omega.
            reflexivity.

          - unfold cpu, curid, chid0, slp_q_id in ×.
            generalize H9; intro tmp; eapply big_acquire_lock_SC_spec_preserve in tmp; eauto.
            destruct tmp as (ikern0 & ihost0 & ipt0 & pg0 & CPU_ID_eq0 & init_a & init_b & inlock0).
            Opaque Z.add Z.mul.
            esplit.
            repeat vcgen.
            unfold thread_get_sync_chan_busy_spec; simpl.
            unfold ObjCV.get_sync_chan_busy_spec; simpl.
            simpl in ×.
            rewrite ikern0, ihost0, pg0, ipt0, H10, init_b, inlock0.
            rewrite zle_lt_true by omega.
            reflexivity.
            destruct (zeq (Int.unsigned c)).
            change 0 with (Int.unsigned Int.zero) in e.
            eapply unsigned_inj in e.
            congruence.
            discharge_cmp.
            repeat vcgen.
        Qed.

      End SyncSendToChanPreBody.

      Theorem syncsendto_chan_pre_code_correct:
        spec_le (syncsendto_chan_pre ↦ thread_syncsendto_chan_pre_spec_low) (〚syncsendto_chan_pre ↦ f_syncsendto_chan_pre 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (syncsendto_chan_pre_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp m´0 labd labd´ (PTree.empty _)
                                        (bind_parameter_temps´ (fn_params f_syncsendto_chan_pre)
                                                               (Vint chid :: nil)
                                                               (create_undef_temps (fn_temps f_syncsendto_chan_pre)))) H0.
      Qed.

    End SYNCSENDTOCHANPRE.

    Section TRYRECEIVECHAN.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
                                                    ⊕ ipc_receive_body ↦ gensem thread_ipc_receive_body_spec
                                                    ⊕ get_sync_chan_busy ↦ gensem thread_get_sync_chan_busy_spec
                                                    ⊕ set_sync_chan_busy ↦ gensem thread_set_sync_chan_busy_spec
                                                    ⊕ thread_wakeup ↦ gensem big2_thread_wakeup_spec.

      Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.

      Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.

        Section TryReceiveChanBody.

          Context `{Hwb: WritableBlockOps}.
          Variable (sc: stencil).
          Variables (ge: genv)
                  (STENCIL_MATCHES: stencil_matches sc ge).

          Variable bget_curid: block.
          Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.
          Hypothesis hget_curid2 : Genv.find_funct_ptr ge bget_curid = Some (External (EF_external get_curid (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable bget_sync_chan_busy: block.

        Hypothesis hget_sync_chan_busy1 : Genv.find_symbol ge get_sync_chan_busy = Some bget_sync_chan_busy.

        Hypothesis hget_sync_chan_busy2 : Genv.find_funct_ptr ge bget_sync_chan_busy = Some (External (EF_external get_sync_chan_busy (signature_of_type (Tcons tint Tnil) tint cc_default)) (Tcons tint Tnil) tint cc_default).

        Variable bset_sync_chan_busy: block.

        Hypothesis hset_sync_chan_busy1 : Genv.find_symbol ge set_sync_chan_busy = Some bset_sync_chan_busy.

        Hypothesis hset_sync_chan_busy2 : Genv.find_funct_ptr ge bset_sync_chan_busy
          = Some (External (EF_external set_sync_chan_busy (signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
                                                                            (Tcons tint (Tcons tint Tnil)) tvoid cc_default).

        Variable bthread_wakeup: block.

        Hypothesis hthread_wakeup1 : Genv.find_symbol ge thread_wakeup = Some bthread_wakeup.

        Hypothesis hthread_wakeup2 : Genv.find_funct_ptr ge bthread_wakeup = Some (External (EF_external thread_wakeup (signature_of_type (Tcons tint Tnil) tint cc_default)) (Tcons tint Tnil) tint cc_default).

        Variable bipc_receive_body: block.

        Hypothesis hipc_receive_body1 : Genv.find_symbol ge ipc_receive_body = Some bipc_receive_body.

        Hypothesis hipc_receive_body2 : Genv.find_funct_ptr ge bipc_receive_body = Some (External (EF_external ipc_receive_body (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).

        Lemma tryreceive_chan_body_correct:
          ∀ m d d´ env le chanid vaddr rcount val
                 (chanidle: PTree.get _chanid le = Some (Vint chanid)),
            env = PTree.empty _ →
            PTree.get _vaddr le = Some (Vint vaddr) →
            PTree.get _rcount le = Some (Vint rcount) →
            high_level_invariant d →
            thread_tryreceive_chan_spec (Int.unsigned chanid) (Int.unsigned vaddr) (Int.unsigned rcount) d
            = Some (d´, Int.unsigned val) →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) tryreceive_chan_body E0 le´ (m, d´) (Out_return (Some (Vint val, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold tryreceive_chan_body.
          functional inversion H3; unfold chid, cpu, slp_q_id in *; subst.

          - rewrite <- Int.repr_unsigned with val.
            rewrite <- H5.
            inv H2.
            Opaque Z.add Z.mul.
            esplit.
            repeat vcgen.
            unfold thread_get_sync_chan_busy_spec; simpl.
            unfold ObjCV.get_sync_chan_busy_spec; simpl.
            subrewrite´.
            rewrite <- H5, H13.
            rewrite zle_lt_true; auto.
            omega.
            change (Int.unsigned Int.zero) with 0.
            discharge_cmp.
            repeat vcgen.

          - inv H2.
            esplit.
            repeat vcgen.
            unfold thread_get_sync_chan_busy_spec; simpl.
            unfold ObjCV.get_sync_chan_busy_spec; simpl.
            subrewrite´.
            rewrite zle_lt_true.
            reflexivity.
            omega.
            destruct (zeq (Int.unsigned c)).
            change 0 with (Int.unsigned Int.zero) in e.
            eapply unsigned_inj in e.
            congruence.
            discharge_cmp.
            repeat vcgen.
            unfold thread_set_sync_chan_busy_spec; simpl.
            unfold ObjCV.set_sync_chan_busy_spec; simpl.
            assert(tmp: init adt1 = true ∧ ikern adt1 = true ∧ pg adt1 = true ∧ ihost adt1 = true ∧ ipt adt1 = true ∧
                        
                        BigLogThreadConfigFunction.B_inLock (CPU_ID adt1) (big_log adt1) = true).
            {
              functional inversion H16; functional inversion H15; simpl in *; eauto.
              inv H; refine_split; auto.
              unfold me; rewrite zeq_true; auto.
            }
            destruct tmp as (init0 & ikern0 & pg0 & ihost0 & ipt0 & B_inlock0).
            subrewrite´.
            rewrite zle_lt_true.
            reflexivity.
            omega.

          - inv H2.
            esplit.
            repeat vcgen.
            unfold thread_get_sync_chan_busy_spec; simpl.
            unfold ObjCV.get_sync_chan_busy_spec; simpl.
            subrewrite´.
            rewrite zle_lt_true.
            unfold sc_id in H6.
            reflexivity.
            omega.
            destruct (zeq (Int.unsigned c)).
            change 0 with (Int.unsigned Int.zero) in e.
            eapply unsigned_inj in e.
            congruence.
            discharge_cmp.
            repeat vcgen.
        Qed.

        End TryReceiveChanBody.

      Theorem tryreceive_chan_code_correct:
        spec_le (tryreceive_chan ↦ thread_tryreceive_chan_spec_low) (〚tryreceive_chan ↦ f_tryreceive_chan 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (tryreceive_chan_body_correct s (Genv.globalenv p) makeglobalenv b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp b4 Hb4fs Hb4fp b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
                                        (bind_parameter_temps´ (fn_params f_tryreceive_chan)
                                                               (Vint chanid :: Vint vaddr :: Vint rcount :: nil)
                                                               (create_undef_temps (fn_temps f_tryreceive_chan)))) H0.
      Qed.

    End TRYRECEIVECHAN.

  End WithPrimitives.

End PIPCINTROCODE.