Library mcertikos.mcslock.INVLemmaQSLock

Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.

Require Import Values.
Require Import AsmX.
Require Import Integers.
Require Import liblayers.compat.CompatLayers.
Require Import GlobalOracle.
Require Import GlobalOracleProp.
Require Import CalMCSLock.
Require Import LogReplay.

Require Import QMCSLockOpGenDef.
Require Import HMCSLockOpGenDef.

Section ORACLE.

  Context `{waittime: WaitTime}.

  Local Transparent QS_CalLock.


  Lemma valid_MCS_log_pool_init:
    valid_MCS_log_pool (ZMap.init MultiUndef).
  Proof.
    unfold valid_MCS_log_pool; intros.
    rewrite ZMap.gi in Hdef.
    inv Hdef.
  Qed.
  Lemma valid_qslock_pool_init:
    valid_qslock_pool (ZMap.init MultiUndef).
  Proof.
    unfold valid_qslock_pool; intros.
    rewrite ZMap.gi in Hdef.
    inv Hdef.
  Qed.



  Lemma valid_MCS_log_pool_gss:
    ∀ t l p
           (Hvalid: valid_MCS_log_pool t)
           (Hlock: valid_MCS_log l),
      valid_MCS_log_pool (ZMap.set p (MultiDef l) t).
  Proof.
    unfold valid_MCS_log_pool; intros.
    destruct (zeq i p); subst.
    - rewrite ZMap.gss in Hdef.
      inv Hdef.
      trivial.
    - rewrite ZMap.gso in Hdef; eauto.
  Qed.

  Lemma valid_qslock_pool_gss:
    ∀ t l p
           (Hvalid: valid_qslock_pool t)
           (Hlock: valid_qslock l),
      valid_qslock_pool (ZMap.set p (MultiDef l) t).
  Proof.
    unfold valid_qslock_pool; intros.
    destruct (zeq p r); subst.
    - rewrite ZMap.gss in Hdef.
      inv Hdef.
      trivial.
    - rewrite ZMap.gso in Hdef; eauto.
  Qed.

  Lemma valid_qslock_pool_gss´:
    ∀ t l p x
           (Hvalid: valid_qslock_pool t)
           (Hlock: QS_CalLock l = Some x),
      valid_qslock_pool (ZMap.set p (MultiDef l) t).
  Proof.
    intros. eapply valid_qslock_pool_gss; eauto.
    unfold valid_qslock.
    destruct x.
    repeat destruct p0.
    eauto 20.
  Qed.
  Lemma correct_qslock_pool_status_gss´:
    ∀ l k c l´ z
           (HP: correct_qslock_pool_status l k c)
           (Hc: correct_qslock_status l´ (ZMap.get z k) c),
      correct_qslock_pool_status
        (ZMap.set z (MultiDef l´) l) k c.
  Proof.
    intros.
    unfold correct_qslock_pool_status in *; intros.
    destruct (zeq r z); subst.
    - rewrite ZMap.gss in ×.
      inv Hdef.
      trivial.
    - rewrite ZMap.gso in *; eauto.
  Qed.

  Lemma correct_qslock_pool_status_gss:
    ∀ l k c l´ k´ z
           (HP: correct_qslock_pool_status l k c)
           (Hc: correct_qslock_status l´ k´ c),
      correct_qslock_pool_status
        (ZMap.set z (MultiDef l´) l) (ZMap.set z k´ k) c.
  Proof.
    intros. unfold correct_qslock_pool_status in *; intros.
    destruct (zeq r z); subst.
    - rewrite ZMap.gss in ×. inv Hdef. trivial.
    - rewrite ZMap.gso in *; eauto.
  Qed.


  Require Import CalTicketLock.

  Lemma real_valid_MCS_log_pool_pb:
    ∀ n l
           (Hvalid: valid_MCS_log_pool l),
      valid_MCS_log_pool (real_multi_log_pb n l).
  Proof.
    induction n.
    - simpl; intros; trivial.
    - simpl; intros; eapply IHn in Hvalid.
      eapply valid_MCS_log_pool_gss; trivial.
      unfold valid_MCS_log; simpl.
      intros.
      Transparent CalMCSLock.
      simpl in H.
      inv H.
      unfold MCSCorrect_range.
      intros.
      inv Hmcs.
      unfold NULL; simpl.
      split; try omega.
      intros.
      rewrite ZMap.gi; simpl; omega.
  Qed.

  Lemma real_valid_MCS_log_pool:
    ∀ l
           (Hvalid:valid_MCS_log_pool l),
      valid_MCS_log_pool (real_multi_log l).
  Proof.
    unfold real_multi_log.
    eapply real_valid_MCS_log_pool_pb.
  Qed.

  Lemma real_valid_qslock_pool_pb:
    ∀ n l
           (Hvalid: valid_qslock_pool l),
      valid_qslock_pool (real_multi_log_pb n l).
  Proof.
    induction n.
    - simpl; intros; trivial.
    - simpl; intros; eapply IHn in Hvalid.
      eapply valid_qslock_pool_gss; trivial.
      unfold valid_qslock; simpl; eauto 10.
  Qed.

  Lemma real_valid_qslock_pool:
    ∀ l
           (Hvalid: valid_qslock_pool l),
      valid_qslock_pool (real_multi_log l).
  Proof.
    unfold real_multi_log.
    eapply real_valid_qslock_pool_pb.
  Qed.

  Lemma real_correct_qslock_pool_status_pb:
    ∀ n l d c
           (Hc: correct_qslock_pool_status l d c),
      correct_qslock_pool_status (real_multi_log_pb n l)
                                 (real_lock_pb n d) c.
  Proof.
    induction n; simpl; intros; trivial.
    eapply correct_qslock_pool_status_gss; eauto.
    unfold correct_qslock_status.
    intros; simpl in Hcal; inv Hcal.
    split; intro HF. intro HF´; inv HF´.
    intro HF´; inv HF´.
  Qed.

  Lemma real_correct_qslock_pool_status:
    ∀ l d c
           (HP: correct_qslock_pool_status l d c),
      correct_qslock_pool_status
        (real_multi_log l) (real_lock d) c.
  Proof.
    unfold real_multi_log.
    unfold real_lock.
    eapply real_correct_qslock_pool_status_pb.
  Qed.



End ORACLE.


Section QMCSLOCK_LAYER.

  Context `{wait_time:WaitTime}.

  Lemma relate_qs_mcs_log_pool_gss´:
    ∀ t l z
           (HP: relate_qs_mcs_log_pool t)
           (HR: relate_qs_mcs_log_type l),
      relate_qs_mcs_log_pool (ZMap.set z l t).
  Proof.
    intros.
    constructor; intros.
    inv HP.
    case_eq (zeq z0 z); intros; subst.
    - rewrite ZMap.gss; auto.
    - rewrite ZMap.gso; try eauto.
  Qed.

  Lemma relate_qs_mcs_log_pool_gss:
    ∀ t l z
           (HP: relate_qs_mcs_log_pool t)
           (HR: relate_qs_mcs_log l),
      relate_qs_mcs_log_pool (ZMap.set z (MultiDef l) t).
  Proof.
    intros.
    assert (relate_qs_mcs_log_type (MultiDef l)).
    { constructor; trivial. }
    eapply relate_qs_mcs_log_pool_gss´; assumption.
  Qed.

  Lemma real_relate_qs_mcs_log_pool_pb:
    ∀ n l
           (Hp: relate_qs_mcs_log_pool l),
      relate_qs_mcs_log_pool (real_multi_log_pb n l).
  Proof.
    induction n; intros; simpl; trivial.
    eapply relate_qs_mcs_log_pool_gss.
    eapply IHn; auto.
    econstructor; [econstructor | ].
    Transparent QS_CalLock.
    simpl.
    Opaque QS_CalLock.
    constructor; auto.
  Qed.

  Lemma real_relate_qs_mcs_log_pool:
    ∀ l
           (Hc: relate_qs_mcs_log_pool l),
      relate_qs_mcs_log_pool (real_multi_log l).
  Proof.
    intros; unfold real_multi_log.
    eapply real_relate_qs_mcs_log_pool_pb; auto.
  Qed.


End QMCSLOCK_LAYER.

Section HMCSLOCK_LAYER.

  Context `{wait_time:WaitTime}.

  Lemma relate_mcs_log_pool_gss´:
    ∀ t1 t2 l1 l2 z
           (HP: relate_mcs_log_pool t2 t1)
           (HR: relate_mcs_log_type l2 l1),
      relate_mcs_log_pool (ZMap.set z l2 t2) (ZMap.set z l1 t1).
  Proof.
    intros.
    constructor; intros.
    inv HP.
    case_eq (zeq z0 z); intros; subst.
    - repeat rewrite ZMap.gss; auto.
    - repeat rewrite ZMap.gso; try eauto.
  Qed.

  Lemma relate_mcs_log_pool_gss:
    ∀ t1 t2 l1 l2 tq z
           (HP: relate_mcs_log_pool t2 t1)
           (HR: relate_mcs_log l1 = Some (l2, tq)),
      relate_mcs_log_pool (ZMap.set z (MultiDef l2) t2) (ZMap.set z (MultiDef l1) t1).
  Proof.
    intros.
    assert (relate_mcs_log_type (MultiDef l2) (MultiDef l1)).
    { eapply RELATE_MCS_LOG_TYPE_DEF with (l := l1) (l´ := l2) (tq := tq); auto. }
    eapply relate_mcs_log_pool_gss´; assumption.
  Qed.

  Lemma real_relate_mcs_log_pool_pb:
    ∀ n l2 l1
           (Hp: relate_mcs_log_pool l2 l1),
      relate_mcs_log_pool (real_multi_log_pb n l2) (real_multi_log_pb n l1).
  Proof.
    induction n; intros; simpl; trivial.
    eapply relate_mcs_log_pool_gss.
    eapply IHn; auto.
    econstructor.
  Qed.

  Lemma real_relate_mcs_log_pool:
    ∀ l2 l1
           (Hc: relate_mcs_log_pool l2 l1),
      relate_mcs_log_pool (real_multi_log l2) (real_multi_log l1).
  Proof.
    intros; unfold real_multi_log.
    eapply real_relate_mcs_log_pool_pb; auto.
  Qed.

End HMCSLOCK_LAYER.