Library mcertikos.conlib.conmtlib.SingleOracle

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.
Require Import RealParams.
Require Import Values.
Require Import Maps.
Require Import Constant.
Require Import Maps.
Require Import ASTExtra.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import Globalenvs.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import LAsm.
Require Import GlobIdent.

Require Import AbstractDataType.
Require Import AuxStateDataType.
Require Import FlatMemory.

Require Import SingleAbstractDataType.
Require Import AlgebraicMem.
Require Export SingleOracleDef.

Require Import GlobalOracleProp.

Thread identifiers

The ThreadsConfiguration class defines how thread IDs are organized among processors, and which threads are main threads.
We consider one high-level thread, the current_thread, which is executed by the high-level LAsm machine and the intermediate TAsm machine. We show that this TAsm machine is refined by a single-thread EAsm machine (AsmT2E), and that in turn this single-thread EAsm machine is refined by a complete EAsm machine that has all the threads of the CPU we're looking at (EAsmCompose). Finally, we show that this complete EAsm machine is refined by the low-level LAsm machine (AsmE2L).
BE AWARE:
current_thread should not be used in AsmE2L and other relate files (the places which are considering multithreads)

Section THREADS_CONF_OPS.

  Class ThreadsConfigurationOps :=
    {
      
      

      
The ID for the CPU we're looking at. (necessary?)
      current_CPU_ID: Z;

      
The thread we're looking at in high-level machines
      current_thread: Z;

      dev_handling_cid : Z;

      vm_handling_cid : Z;

      
The other threads on this CPU
      non_current_thread_list: list Z;

      
The full list
      full_thread_list := current_thread :: non_current_thread_list;

      
The main thread on this CPU
      main_thread: Z;

      
A log look-back limit used in TAsm
      limit: nat

    }.

End THREADS_CONF_OPS.

Section SINGLE_ORACLE_OPS.

  Class SingleOracleOps :=
    {
      init_log: Log;
      Single_Oracle : Log → LogEvent;
      init_nb : positive
    }.

  Section WITH_OPS.

    Context `{sops: SingleOracleOps}.

    Fixpoint last_nb (l: Log) :=
      match l with
      | nil ⇒ init_nb
      | a :: l´ ⇒
        match getLogEventNB a with
        | Some nb ⇒ nb
        | _ ⇒ last_nb l´
        end
      end.

  End WITH_OPS.

End SINGLE_ORACLE_OPS.

Section With_Oracle.

  Class SingleOracle `{single_data: SingleData} `{single_oracle_ops : SingleOracleOps}
        `{threads_conf_ops : ThreadsConfigurationOps} :=
    {
      update : dshare → Log → dshare;

      has_event: ident → bool;
      
      uRData (l: Log) : dshare := update (init_dshare) l;
      
      
      state_check: ident → list lval → Log → dproc → Prop;
      
      
      choice_check: ident → list lval → dshare → dproc → Z;

      
      sync_chpool_check: ident → list lval → dshare → dproc → option SyncChanPool;
      snap_func : dproc → privDataSnap;
      snap_rev_func : privDataSnap → dproc;

      thread_init_dproc : Z → dproc;
 
      
      state_checks (name : ident) (largs: list lval) (l : Log) (pdp: ZMap.t (option dproc)) :=
        match ZMap.get (proc_id (uRData l)) pdp with
          | Some pd ⇒ state_check name largs l pd
          | _ ⇒ True
        end;

      
      PHThread2TCompose : option KContext → dshare → dproc → RData;
      
      thread_init_rdata (tid: Z) :=
        PHThread2TCompose
          None
          (uRData init_log)
          (thread_init_dproc tid);

      
      prim_thread_init_pc {F V} (ge: Genv.t F V): ident → list lval → option val
    }.

End With_Oracle.

Section THREADS_CONF.

  Class ThreadsConfiguration `{s_oracle : SingleOracle}: Prop :=
    {
      
      CPU_ID_valid:
        ∀ l, processor_id (uRData l) = current_CPU_ID;
      main_valid:
        In main_thread full_thread_list;
      null_log_proc_id:
        proc_id (uRData nil) = main_thread;
      
      main_thread_val:
        main_thread = current_CPU_ID + 1;
      current_CPU_ID_range:
        0 ≤ current_CPU_ID < Constant.TOTAL_CPU;
      
      dev_handling_cid_constraint:
        dev_handling_cid = main_thread;

      
      init_log_proc_id:
        proc_id (uRData init_log) = current_thread;
      valid_thread_list:
        ∀ i, In i full_thread_list → Constant.TOTAL_CPU < i < Constant.num_proc ∨ i = main_thread;

      
      all_cid_in_full_thread_list :
        ∀ l, In (proc_id (uRData l)) full_thread_list;

      
      full_thread_list_prop: NoDup full_thread_list
    }.

  Lemma current_valid `{ThreadsConfiguration}:
    In current_thread full_thread_list.
  Proof.
    left.
    reflexivity.
  Qed.

End THREADS_CONF.

Require Import INVLemmaThreadContainer.
Require Import DeviceStateDataType.

Module PHThreadInvariant.
**Definition of the invariants at MPTNew layer 0th page map is reserved for the kernel thread

  Record high_level_invariant (abd: RData) :=
    mkInvariant {
        valid_nps: pg abd = true → kern_low ≤ nps abd ≤ maxpage;
        
        valid_kern: ikern abd = false → pg abd = true;
        valid_iptt: ipt abd = true → ikern abd = true;
        valid_iptf: ikern abd = false → ipt abd = false;
        valid_ihost: ihost abd = false → pg abd = true ∧ ikern abd = true;
        valid_container: Thread_Container_valid (AC abd);
        
        init_pperm: pg abd = false → (pperm abd) = ZMap.init PGUndef;
        valid_PMap: pg abd = true →
                    (∀ i, 0≤ i < num_proc →
                               PMap_valid (ZMap.get i (ptpool abd)));
        
        valid_PT_kern: pg abd = true → ikern abd = true → (PT abd) = 0;
        valid_PMap_kern: pg abd = true → PMap_kern (ZMap.get 0 (ptpool abd));
        valid_PT: pg abd = true → 0≤ PT abd < num_proc;
        valid_dirty: dirty_ppage´ (pperm abd) (HP abd);

        valid_idpde: pg abd = true → IDPDE_init (idpde abd);
        

        

        
        valid_init_PT_cid: ikern abd = false → PT abd = ZMap.get (CPU_ID abd) (cid abd);
        valid_ikern_ipt: ikern abd = ipt abd;

        valid_cons_buf_rpos: 0 ≤ rpos (console abd) < CONSOLE_BUFFER_SIZE;
        valid_cons_buf_length: 0 ≤ Zlength (cons_buf (console abd)) < CONSOLE_BUFFER_SIZE;

        CPU_ID_range: 0 ≤ (CPU_ID abd) < TOTAL_CPU;
        valid_curid: 0 ≤ ZMap.get (CPU_ID abd) (cid abd) < num_proc
      }.

End PHThreadInvariant.

Module PIPCIntroInvariant.
**Definition of the invariants at MPTNew layer 0th page map is reserved for the kernel thread

  Record high_level_invariant (abd: RData) :=
    mkInvariant {
        valid_nps: pg abd = true → kern_low ≤ nps abd ≤ maxpage;
        
        valid_kern: ikern abd = false → pg abd = true;
        valid_iptt: ipt abd = true → ikern abd = true;
        valid_iptf: ikern abd = false → ipt abd = false;
        valid_ihost: ihost abd = false → pg abd = true ∧ ikern abd = true;
        valid_container: Thread_Container_valid (AC abd);
        
        init_pperm: pg abd = false → (pperm abd) = ZMap.init PGUndef;
        valid_PMap: pg abd = true →
                    (∀ i, 0≤ i < num_proc →
                               PMap_valid (ZMap.get i (ptpool abd)));
        
        valid_PT_kern: pg abd = true → ikern abd = true → (PT abd) = 0;
        valid_PMap_kern: pg abd = true → PMap_kern (ZMap.get 0 (ptpool abd));
        valid_PT: pg abd = true → 0≤ PT abd < num_proc;
        valid_dirty: dirty_ppage´ (pperm abd) (HP abd);

        valid_idpde: pg abd = true → IDPDE_init (idpde abd);
        

        

        
        valid_init_PT_cid: ikern abd = false → PT abd = ZMap.get (CPU_ID abd) (cid abd);
        valid_ikern_ipt: ikern abd = ipt abd;

        valid_cons_buf_rpos: 0 ≤ rpos (console abd) < CONSOLE_BUFFER_SIZE;
        valid_cons_buf_length: 0 ≤ Zlength (cons_buf (console abd)) < CONSOLE_BUFFER_SIZE;

        CPU_ID_range: 0 ≤ (CPU_ID abd) < TOTAL_CPU;
        valid_curid: 0 ≤ ZMap.get (CPU_ID abd) (cid abd) < num_proc
      }.

End PIPCIntroInvariant.

Section With_OracleProp.

  Class SingleOracleProp `{thread_conf_prf: ThreadsConfiguration}:=
    {

      
      update_proc_id:
        ∀ d d´ d´´ l a,
          update d l = d´ →
          getLogEventType a = LogOtherTy →
          update d (a :: l) = d´´ →
          proc_id d´´ = proc_id d´;

      update_processor_id:
        ∀ d d´ d´´ l a,
          update d l = d´ →
          update d (a::l) = d´´ →
          processor_id d´´ = processor_id d´;

    
This checks whether the given primitive call initializes any thread. If so, returns the thread's id and initial register state.

      init_data_low_level_invariant n:
        low_level_invariant n (thread_init_rdata current_thread);

      init_data_phthread_high_level_invariant:
        PHThreadInvariant.high_level_invariant (thread_init_rdata current_thread);
       
      init_data_pipcintro_high_level_invariant:
        PIPCIntroInvariant.high_level_invariant (thread_init_rdata current_thread);

      prim_thread_init_pc_global:
        ∀ {F V} (ge: Genv.t F V) f vargs v,
          prim_thread_init_pc ge f vargs = Some v →
          (∃ id ofs, symbol_offset ge id ofs = v);

      prim_thread_init_pc_symbols_preserved:
        ∀ {F V} (ge1 ge2: Genv.t F V) f vargs v,
          (∀ i, Genv.find_symbol ge1 i = Genv.find_symbol ge2 i) →
          prim_thread_init_pc ge1 f vargs = Some v →
          prim_thread_init_pc ge2 f vargs = Some v
    }.

  Context `{s_oracle_prop : SingleOracleProp}.

  Lemma uRData_proc_id_eq:
    ∀ l a ,
      getLogEventType a = LogOtherTy →
      proc_id (uRData (a :: l)) = proc_id (uRData l).
  Proof.
    intros. unfold uRData.
    eapply update_proc_id; eauto.
  Qed.

End With_OracleProp.

Section With_OracleLinkProp.

  Class SingleOracleLinkProp `{thread_conf_prf: ThreadsConfiguration}:=
    {
      Oracle_le_nb:
        ∀ l,
          (last_nb l ≤ last_nb (Single_Oracle l :: l)) % positive;

      oracle_event_yield_back:
        ∀ l,
          lastEvType l = Some LogYieldTy →
          ∃ i, Single_Oracle l = LEvent i LogYieldBack;

      
In TAsm, we start with the init_log for our initial state. But the init_log is not compositional, so in EAsm we start from an empty log and make environment steps by querying the oracle until the first LogYieldBack event to one of our threads. The following constraint ensures that the two are consistent.

      oracle_init_log:
        ∀ (l´: Log) (e: LogEvent) (l: Log),
          init_log = l´ ++ e :: l →
          Single_Oracle l = e;
      
      init_log_structure:
        init_log = nil ∨
        ∃ l e,
          init_log = LEvent (proc_id (uRData l)) LogYieldBack :: l ∧
          proc_id (uRData l) ≠ proc_id (uRData nil) ∧
          last_op l = Some e ∧
          getLogEventNB e ≠ None ∧
          ∀ e l1 l2,
            l = l1 ++ e :: l2 →
            proc_id (uRData l2) ≠
            proc_id (uRData init_log)
    }.

  Context `{s_oracle_link_prop : SingleOracleLinkProp}.

  Lemma oracle_event_yield:
    ∀ l,
      getLogEventType (Single_Oracle l) = LogYieldTy →
      lastEvType l ≠ Some LogYieldTy.
  Proof.
    intros. intro HF.
    eapply oracle_event_yield_back in HF.
    destruct HF as (i & Heq).
    rewrite Heq in H. simpl in H. congruence.
  Qed.

End With_OracleLinkProp.

Ltac Thread_PrimInvariants_simpl_auto :=
  constructor; intros until d´; intros Hspec Hinv; functional inversion Hspec;
  functional inversion H; inv Hinv; try subst; constructor; auto; simpl in *;
  intros; congruence.