Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import Constant.
Require Import GlobIdent.
Require Import AbstractDataType.
Require Import GlobalOracle.

Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatLayers.
Require Import AuxStateDataType.
Require Import RealParams.
Require Import CalMCSLock.

Section Refinement.

  Local Open Scope string_scope.
  Local Open Scope error_monad_scope.
  Local Open Scope Z_scope.

  Context `{real_params: RealParams}.

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.
    Context `{wait_time : WaitTime}.


    Fixpoint relate_mcs_log (l: MultiLog): option(MultiLog × list nat) :=
      match l with
        | nil ⇒ Some (nil, nil)
        | (TEVENT i e) :: l´ ⇒
          match relate_mcs_log l´ with
            | Some (ll, tq) ⇒
              match e with
                | TTICKET e´ ⇒
                  match e´ with
                    | SWAP_TAIL p true ⇒ Some ((TEVENT i (TTICKET (WAIT_LOCK p)))::ll, tq ++ (p::nil))
                    | SWAP_TAIL p false ⇒ Some (ll, tq ++ (p::nil))
                    | GET_NEXT ⇒ Some (ll,tq)
                    | SET_NEXT _ ⇒ Some (ll,tq)
                    | SET_BUSY ⇒
                      match tq with
                        | _::tq´ ⇒
                          Some ((TEVENT i (TTICKET REL_LOCK))::ll, tq´)
                        | _ ⇒ None
                      end
                    | GET_BUSY true ⇒ Some (ll,tq)
                    | GET_BUSY false ⇒
                      match tq with
                        | p:: tq´ ⇒
                          Some ((TEVENT i (TTICKET (WAIT_LOCK p))) :: ll, tq)
                        | _ ⇒ None
                      end
                    | CAS_TAIL false ⇒ Some (ll,tq)
                    | CAS_TAIL true ⇒ Some ((TEVENT i (TTICKET REL_LOCK))::ll, nil)
                    | _ ⇒ None
                  end
                | TSHARED _ ⇒
                  Some ((TEVENT i e) :: ll, tq)
              end
            | _ ⇒ None
          end
      end.

    Inductive relate_mcs_log_type: MultiLogType → MultiLogType → Prop :=
    | RELATE_MCS_LOG_TYPE_UNDEF:
        relate_mcs_log_type MultiUndef MultiUndef
    | RELATE_MCS_LOG_TYPE_DEF:
        ∀ l l´ tq
               (Hrelate_mcs_log: relate_mcs_log l = Some (l´, tq)),
          relate_mcs_log_type (MultiDef l´) (MultiDef l).

    Inductive relate_mcs_log_pool: MultiLogPool → MultiLogPool → Prop :=
    | RELATE_MCS_LOG_POOL:
        ∀ l l´
               (Hrelate_mcs_log_type:
                  ∀ index ofs z
                         (Hrange: index2Z index ofs = Some z),
                    relate_mcs_log_type (ZMap.get z l) (ZMap.get z l´)),
          relate_mcs_log_pool l l´.

    Inductive relate_mcs_oracle: MultiOracle → MultiOracle → Prop :=
      | RELATE_MCS_ORACLE:
          ∀ o1 o2
                 (Hrelate_mcs_oracle_res:
                    
                    (∀ i l1 l2 tq bound mcs
                            (Hrelate_log: relate_mcs_log l2 = Some (l1, tq))
                            (HQS_CalLock_Valid: QS_CalLock ((TEVENT i (TTICKET (SWAP_TAIL bound true))) :: o2 i l2 ++ l2)
                                                = Some mcs),
                     ∃ tq´, relate_mcs_log (o2 i l2 ++ l2) = Some (o1 i l1 ++ l1, tq´)) ∧
                    
                    (∀ i l1 l2 tq bound prev_id
                            (Hrelate_log: relate_mcs_log l2 = Some (l1, tq)),
                       let l20 := (TEVENT i (TTICKET (SWAP_TAIL bound false))) :: o2 i l2 ++ l2 in
                       let l21 := (TEVENT i (TTICKET (SET_NEXT prev_id))) :: o2 i l20 ++ l20 in
                       ∀ self_c rel_c b q slow tq0 mcs´ l2´ l2´_tl
                              (HCal1: QS_CalLock l20 = Some (self_c, rel_c, b, q, slow, tq0 ++ bound :: nil))
                              (HCal2: QS_CalLock l21 = Some mcs´)
                              (HWait: QS_CalWaitGet (CalWaitLockTime tq0) i l21 o2 = Some l2´)
                              (Hl2´: l2´ = (TEVENT i (TTICKET (GET_BUSY false))) :: l2´_tl),
                       ∃ tq´, relate_mcs_log l2´_tl = Some (o1 i l1 ++ l1, tq´))),
            relate_mcs_oracle o1 o2.


    Inductive relate_mcs_oracle_pool: MultiOraclePool → MultiOraclePool → Prop :=
    | RELATE_MCS_ORACLE_POOL:
        ∀ o1 o2
               (Hrelate_mcs_oracle:
                  ∀ index ofs z
                         (Hrange: index2Z index ofs = Some z),
                    relate_mcs_oracle (ZMap.get z o1) (ZMap.get z o2)),
          relate_mcs_oracle_pool o1 o2.

  End WITHMEM.

End Refinement.