Require Import Vbase.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple fsltriple2.
Require Import fslassnlemmas2.
Require Import fsl load store rmw ghosts.
Require Import Omega.

Set Implicit Arguments.

Derived FSL rules


Lemma triple_false PS PSg E QQ :
  triple (@Afalse PS PSg) E QQ.
Proof.
  done.
Qed.

Lemma rule_conseq_pre PS PSg:
   (P : assn PS PSg) (E : cexp) (QQ : nat assn PS PSg),
    triple P E QQ
     P' : assn PS PSg,
      implies P' P
      triple P' E QQ.
Proof.
  ins; eapply rule_conseq; eauto using implies_refl.
Qed.

Lemma rule_conseq_post PS PSg:
   (P : assn PS PSg) (E : cexp) (QQ : nat assn PS PSg),
    triple P E QQ
     QQ' : val assn PS PSg,
      ( y, implies (QQ y) (QQ' y))
      triple P E QQ'.
Proof.
  ins; eapply rule_conseq; eauto using implies_refl.
Qed.

Lemma rule_repeat2 PS PSg (P: assn PS PSg) E QQ QQ' :
  triple P E QQ'
  implies (QQ' 0%nat) P
  ( x (NZ: x 0%nat), implies (QQ' x) (QQ x))
  triple P (Erepeat E) QQ.
Proof.
  ins; eapply rule_conseq; [eby apply rule_repeat|done|].
  ins; desf; ins; eauto.
Qed.

Lemma rule_value_simple PS PSg (P: assn PS PSg) v:
  triple P (Evalue v) (fun xif (x == v)%bool then P else Afalse).
Proof.
  eapply rule_conseq_pre.
    by apply rule_value.
  desf; desf.
Qed.

Lemma rule_alloc_atom_rmwacq_frame PS PSg (P: assn PS PSg) QQ :
  triple P (Ealloc) (fun xArel x QQ &*& Armwacq x QQ &*& P).
Proof.
  eapply rule_conseq_pre.
    2: by apply star_emp_l.
  eapply rule_conseq.
  2: by apply implies_refl.
  by apply rule_frame, rule_alloc_atom_rmwacq.
  by ins; apply equivalent_starA.
Qed.

Theorem rule_store_rlx_rmw PS PSg E E' (QQ: val assn PS PSg) :
  triple (Arel E QQ &*& Armwacq E QQ &*& Atriangle (QQ E'))
         (Estore ATrlx E E')
         (fun _RMW E QQ).
Proof.
  eapply rule_conseq.
    2: by apply implies_star_l, Arel_split1.

  eapply rule_conseq_pre.
  Focus 2.
    rewrite equivalent_starA.
    rewrite equivalent_starAC.
    apply implies_star_r.
    eby rewrite <- equivalent_starA, equivalent_starC.
  eapply rule_conseq_pre.
    2: eby rewrite <- equivalent_starA.

  by apply rule_frame, rule_store_rlx.

  by ins; rewrite equivalent_starC, equivalent_starA.
Qed.

Lemma rule_load_rlx_rmw PS PSg typ (P: assn PS PSg) E QQrel QQacq:
  typ ATna triple (rmw_precondition P E QQrel QQacq)
                        (Eload typ E)
                        (fun _rmw_precondition P E QQrel QQacq).
Proof.
  ins; eapply rule_conseq.

  Focus 2.
    unfold rmw_precondition.
    rewrite Armw_acq_split with (QQ := fun _Aemp); eauto.
    rewrite equivalent_starA, !(equivalent_starAC (Arainit _)), !(equivalent_starAC (Aacq _ _)),
            <- equivalent_starA.
    by apply implies_refl.

  by apply rule_frame, rule_load_rlx.

  ins; rewrite nabla_emp, <- star_emp_r, equivalent_starA, !(equivalent_starAC (Armwacq _ _)),
        <- equivalent_starA, <- Armw_acq_split.
  by rewrite !(equivalent_starAC (Arel _ _)); apply implies_refl.
  by ins; unfold hupd; desf; desf; eauto.
Qed.

Theorem rule_cas_ar_simple PS PSg:
   rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT (phi : val Prop)
    (NORM: normalizable P)
    (IMPacq: implies (QQacq E') (Aexists (fun zAstar (AA z) (TT z))))
    (IMPrel: z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (AR: acquire_release_typ rmw_typ) (ATL: load_typ ATna),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun xif (x == E' )%bool
                   then Aexists (satisfying phi AA)
                   else rmw_precondition P E QQrel QQacq).
Proof.
  ins; eapply rule_cas_ar; try edone.
  eapply rule_conseq_post.
    by apply rule_load_rlx_rmw.
  ins; desf; desf.
  apply implies_true.
Qed.

Theorem rule_cas_rel_simple PS PSg :
   rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT (phi: val Prop)
    (NORM: normalizable P)
    (IMPacq: implies (QQacq E') (Aexists (fun zAstar (AA z) (TT z))))
    (IMPrel: z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (REL: release_typ rmw_typ) (ATL: load_typ ATna),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun xif (x == E')%bool
                   then Aexists (satisfying phi (fun yAnabla (AA y)))
                   else rmw_precondition P E QQrel QQacq).
Proof.
  ins; eapply rule_cas_rel; try edone.
  eapply rule_conseq_post.
    by apply rule_load_rlx_rmw.
  ins; desf; desf.
  apply implies_true.
Qed.

Theorem rule_cas_acq_simple PS PSg :
   rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT (phi : val Prop)
    (IMPacq: implies (QQacq E') (Aexists (fun zAstar (AA z) (TT z))))
    (IMPrel: z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (ACQ: acquire_typ rmw_typ) (ATL: load_typ ATna),
  triple (rmw_precondition (Atriangle P) E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun xif (x == E' )%bool
                   then Aexists (satisfying phi AA)
                   else rmw_precondition (Atriangle P) E QQrel QQacq).
Proof.
  ins; eapply rule_cas_acq; try edone.
  eapply rule_conseq_post.
    by apply rule_load_rlx_rmw.
  ins; desf; desf.
  apply implies_true.
Qed.

Theorem rule_cas_rlx_simple PS PSg :
   rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT (phi : val Prop)
    (IMPacq: implies (QQacq E') (Aexists (fun zAstar (AA z) (TT z))))
    (IMPrel: z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (AT: rmw_typ ATna) (ATL: load_typ ATna),
  triple (rmw_precondition (Atriangle P) E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun xif (x == E')%bool
                   then Aexists (satisfying phi (fun yAnabla (AA y)))
                   else rmw_precondition (Atriangle P) E QQrel QQacq).
Proof.
  ins; eapply rule_cas_rlx; try edone.
  eapply rule_conseq_post.
    by apply rule_load_rlx_rmw.
  ins; desf; desf.
  apply implies_true.
Qed.

Theorem rule_cas_shortcut_simple PS PSg:
   rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq
    (UNSAT: implies (Astar (QQacq E') P) Afalse)
    (ATL: load_typ ATna),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun xif (x == E')%bool then Afalse else rmw_precondition P E QQrel QQacq).
Proof.
  ins; eapply rule_cas_shortcut; try edone.
  eapply rule_conseq_post.
    by apply rule_load_rlx_rmw.
  ins; desf; desf.
  apply implies_true.
Qed.

Fetch and modify

Definition fetch_and_modify rmw_typ load_typ l (f: val val) :=
 LET r <- REPEAT
            LET t <- {{ l }}_ ATrlx in
            LET u <- Ecas rmw_typ load_typ l t (f t) in
            Evalue (if (u == t)%bool then u + 1 else 0)
          END
 in Evalue (Peano.pred r).

Definition increment rmw_typ l := fetch_and_modify rmw_typ ATrlx l (fun x ⇒ (x + 1)%nat).

Definition decrement rmw_typ l := fetch_and_modify rmw_typ ATrlx l (fun xPeano.pred x).

Lemma rmw_precondition_star_split PS PSg (P Psend Pkeep: assn PS PSg) E QQrel QQacq:
  equivalent P (Psend &*& Pkeep)
  equivalent (rmw_precondition P E QQrel QQacq) (rmw_precondition Psend E QQrel QQacq &*& Pkeep).
Proof.
  ins; unfold rmw_precondition; rewrite H, !equivalent_starA; apply equivalent_refl.
Qed.

Theorem rule_fetch_and_modify PS PSg:
   (P: assn PS PSg) Psend Pkeep E rmw_typ load_typ QQacq QQrel RR f
    (SPLIT: v, equivalent P (Psend v &*& Pkeep v))
    (CAS: t, triple (rmw_precondition (Psend t) E QQrel QQacq)
                           (Ecas rmw_typ load_typ E t (f t))
                           (fun xif (x == t)%bool then RR t else rmw_precondition (Psend t) E QQrel QQacq)),
    triple (rmw_precondition P E QQrel QQacq)
           (fetch_and_modify rmw_typ load_typ E f)
           (fun xRR x &*& Pkeep x).
Proof.
  ins; apply rule_let with (QQ := fun xRR (Peano.pred x) &*& Pkeep (Peano.pred x)).
    2: by ins; eapply rule_conseq_pre; [apply rule_value |].
  eapply rule_repeat2.
  instantiate (1 := fun xif ((x == 0%nat)%bool)
                             then rmw_precondition P E QQrel QQacq
                             else RR (Peano.pred x) &*& Pkeep (Peano.pred x)).
    2: done.
    2: by ins; desf; desf.
  eapply rule_let.
    by apply rule_load_rlx_rmw.
  intro t; ins.
  eapply rule_let.
  eapply rule_conseq_pre.
    2: by apply rmw_precondition_star_split, (SPLIT t).
    by apply rule_frame, CAS.
  intro u; ins.
  eapply rule_conseq_pre; [by apply rule_value |].
  desf; desf; try omega.
  by rewrite Plus.plus_comm.
  eby rewrite <- rmw_precondition_star_split.
Qed.

Makes RMW permission actually usable by translating it into the rmw_precondition
Lemma rmw_permission_rmw_precondition PS PSg x QQ (P: assn PS PSg):
  equivalent (RMW x QQ &*& P) (rmw_precondition P x QQ QQ).
Proof.
  unfold RMW, rmw_precondition; rewrite !equivalent_starA; apply equivalent_refl.
Qed.


This page has been generated by coqdoc