Examples

Require Import Vbase Varith Vlistbase Vlist extralib.
Require Import c11 exps rslassn rslassnlemmas rslmodel rsl.
Open Scope string_scope.

Set Implicit Arguments.

Generic lemmas

Lemma Arel_split1 x v PP :
  implies (Arel x PP)
          (Astar (Arel x PP) (Arel x (mupd (fun _ ⇒ Afalse) v (PP v)))).
Proof.
  unfold mupd; red; ins; desf; repeat eexists; ins.
  rewrite hplus_unfold; desf; f_equal; ins; [|destruct n].
    by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
       extensionality z; unfold Remp; desf; desf;
       eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
  ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
Qed.

Lemma Arainit_split1 x :
  implies (Arainit x)
          (Astar (Arainit x) (Arainit x)).
Proof.
  unfold mupd; red; ins; desf; repeat eexists; ins.
  rewrite hplus_unfold; desf; f_equal; ins; [|destruct n].
    by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
       extensionality z; unfold Remp; desf; desf;
       eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
  ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
Qed.

Lemma Arainit_split2 x :
  implies (Astar (Arainit x) (Arainit x)) (Arainit x).
Proof.
  unfold mupd; red; ins; desf; repeat eexists; ins.
  rewrite hplus_unfold; desf; f_equal; ins; [|destruct n].
    by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
       extensionality z; unfold Remp; desf; desf;
       eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
  ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
Qed.

Lemma Arel_split11 x PP :
  implies (Arel x PP)
          (Astar (Arel x PP) (Arel x PP)).
Proof.
  unfold mupd; red; ins; desf; repeat eexists; ins.
  rewrite hplus_unfold; desf; f_equal; ins; [|destruct n].
    by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
       extensionality z; unfold Remp; desf; desf;
       eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
  ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
Qed.

Lemma Armw_acq_split1 x PP QQ :
  (∀ v, QQ v = Aemp ∨ PP v = Afalse ∧ QQ v = Afalse ) →
  implies (Armwacq x PP) (Astar (Armwacq x PP) (Aacq x QQ)).
Proof.
  unfold mupd; red; ins; desf; repeat eexists; ins.
  rewrite hplus_unfold; desf; f_equal; ins; [|destruct n].
    by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
       extensionality z; unfold Remp; desf; desf;
       eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
  ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
  destruct (H v) as [->|[->->]]; vauto.
Qed.

Lemma Armw_acq_split2 x PP QQ :
  (∀ v, QQ v = Aemp ∨ PP v = Afalse ∧ QQ v = Afalse ) →
  implies (Astar (Armwacq x PP) (Aacq x QQ)) (Armwacq x PP).
Proof.
  unfold mupd; red; ins; desf; repeat eexists; ins.
  rewrite hplus_unfold; desf; f_equal; ins; [|destruct n].
    by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
       extensionality z; unfold Remp; desf; desf;
       eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
  ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
  destruct (H v) as [->|[->->]]; vauto.
Qed.

Lemma implies_refl P : implies P P.
Proof. done. Qed.

Lemma implies_star_l P Q R : implies P Q → implies (Astar P R) (Astar Q R).
Proof.
  red; ins; desf; repeat eexists; eauto.
Qed.

Lemma implies_star_r P Q R : implies P Q → implies (Astar R P) (Astar R Q).
Proof.
  red; ins; desf; repeat eexists; eauto.
Qed.

Lemma rule_store_rel2 mt typ E E' QQ :
  release_typ typ →
  triple mt
    (Astar (Arel E QQ) (QQ E'))
    (Estore typ E E')
    (fun _ ⇒ Astar (Arel E QQ) (Arainit E)).
Proof.
  intros; eapply rule_conseq.
    by eapply rule_frame with (F := Arel E QQ), rule_store_rel; vauto.
  intros ? D; eapply implies_star_l in D; [|by apply (Arel_split1 E')].
    eapply sim_assn_sem, D; clear D.
    eapply Asim_trans, Asim_sym, Asim_starA.
    eapply Asim_sym.
    eapply Asim_trans, Asim_sym, Asim_starC.
    by eauto using Asim.
  intros ? ? D; eapply sim_assn_sem, D; eauto using Asim.
Qed.

Lemma rule_load_rlx3 E QQ :
  triple Model_hb_rf_acyclic (Astar (Armwacq E QQ) (Arainit E))
  (Eload ATrlx E)
  (fun v ⇒ if QQ v == Afalse then Afalse else Astar (Armwacq E QQ) (Arainit E)).
Proof.
  eapply rule_conseq.
    by apply rule_frame with (F := Armwacq E QQ), rule_load_rlx2.
  {
    pose (myQQ := (fun v ⇒ if QQ v == Afalse then Afalse else Aemp)).
    intros ? D; eapply implies_star_l in D; [|apply Armw_acq_split1 with (QQ:=myQQ)].
      by eapply sim_assn_sem, D; clear D; eauto using Asim.
     by subst myQQ; ins; desf; vauto.
  }
  ins; desf; desf; intros ? D; try solve[ins; desf].
  eapply implies_star_l; [apply Armw_acq_split2|eapply sim_assn_sem, D]; clear D;
  [|by eauto using Asim]; instantiate; ins; desf; vauto.
Qed.

Lemma rule_repeat2 mt P E QQ QQ' :
  triple mt P E QQ' →
  implies (QQ' 0) P →
  (∀ x (NZ: x ≠ 0), implies (QQ' x) (QQ x)) →
  triple mt P (Erepeat E) QQ.
Proof.
  ins; eapply rule_conseq; [eby apply rule_repeat|done|].
  ins; desf; ins; eauto.
Qed.

Lemma implies_sim P Q : Asim P Q → implies P Q.
Proof. by red; ins; apply (sim_assn_sem H). Qed.

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

Notation " 'LET' x <- E 'IN' F " :=
  (Elet E (fun x ⇒ F))
  (at level 200, x ident).
Notation " 'REPEAT' E 'END' " := (Erepeat E).
Notation " 'PAR_BEGIN' E 'PAR' F 'END' " := (Epar E F).
Notation " [[ E ]]_ A " := (Eload A E) (at level 198, A ident).
Notation " [[ E ]]_ A <- V " := (Estore A E V) (at level 198, A ident).
Notation " E ;; F " := (Elet E (fun _ ⇒ F)) (at level 199).

Mutual exclusion locks

The first example is a mutual exclusion lock module. The lock is implemented as a location storing 0 whenever the lock is held and 1 whenever it is free.

Definition new_lock :=
  LET x <- Ealloc IN
  [[ x ]]_ ATrel <- 1 ;;
  Evalue x.

Definition spin x :=
  REPEAT [[ x ]]_ ATrlx END.

Definition lock x :=
  REPEAT spin x ;; Ecas ATacq ATrlx x 1 0 END.

Definition unlock x :=
  [[ x ]]_ ATrel <- 1.

Further, we show that an invariant J may be attached to a lock so that we get the same specifications as in concurrent separation logic.

Definition LockQQ J v :=
  if v == 0 then Aemp
  else if v == 1 then J
  else Afalse.

Definition LockPred x J :=
  Astar (Arel x (LockQQ J)) (Astar (Armwacq x (LockQQ J)) (Arainit x)).

Lemma new_lock_spec mt J :
  triple mt J new_lock (fun x ⇒ LockPred x J).
Proof.
  eapply rule_let; ins.
    eapply rule_conseq_pre; [by apply rule_frame with (F:=J),
                                  rule_alloc_atom_rmwacq|].
      by intros ? H; eapply sim_assn_sem, H; Asim_simpl.
  eapply rule_let; ins.
    eapply rule_conseq_pre; [
    by apply rule_frame with (F:=(Armwacq x (LockQQ J)));
       apply rule_store_rel2; ins; vauto |].
    instantiate (1 := (LockQQ J)); instantiate (1 := (LockQQ J)).
    unfold LockQQ at 4; simpl.
    intros ? D; eapply sim_assn_sem, D; clear D.
    by eauto using Asim.
  eapply rule_conseq_pre; [apply rule_value|].
  by intros ? D; eapply sim_assn_sem, D; clear; unfold LockPred;
     eauto using Asim.
Qed.

Lemma unlock_spec mt x J :
  triple mt (Astar (LockPred x J) J) (unlock x) (fun _ ⇒ LockPred x J).
Proof.
  eapply rule_conseq;
    [by apply rule_frame with (F := LockPred x J), rule_store_rel; vauto| |];
  unfold LockPred; ins; intros ? D.
    instantiate (1 := J).
    eapply implies_star_l in D; [|by apply implies_star_l, (Arel_split1 1)].
    eapply sim_assn_sem, D; clear D.
    unfold LockQQ at 4; simpl.
    eapply Asim_trans, Asim_sym, Asim_starA.
    eapply Asim_trans, Asim_sym, Asim_starA.
    eapply Asim_sym.
    eapply Asim_trans, Asim_sym, Asim_starC.
    eapply Asim_trans, Asim_sym, Asim_starA.
    by eapply Asim_star; eauto using Asim.
  eapply implies_star_r; [by apply implies_star_r, Arainit_split2|].
  eapply sim_assn_sem, D; clear D.
  eapply Asim_trans, Asim_sym, Asim_starC.
  repeat (eapply Asim_trans, Asim_sym, Asim_starA).
  eauto using Asim.
Qed.

Lemma spin_spec mt x J :
  triple mt (LockPred x J) (spin x) (fun _ ⇒ LockPred x J).
Proof.
  eapply rule_conseq; [
    by eapply rule_repeat; [apply rule_frame with (F := LockPred x J),
                                  rule_load_rlx |]
    | |]; ins; unfold LockPred; intros ? D; desf; try done.

    eapply implies_star_r in D; [|by apply implies_star_r, Arainit_split1].
    eapply sim_assn_sem, D; clear D.
    eapply Asim_sym, Asim_trans, Asim_sym, Asim_starC.
    repeat (eapply Asim_trans, Asim_sym, Asim_starA).
    by eauto using Asim.

  eapply implies_star_r; [by apply implies_star_r, Arainit_split2|].
  eapply sim_assn_sem, D; clear D.
  eapply Asim_trans, Asim_sym, Asim_starC.
  repeat (eapply Asim_trans, Asim_sym, Asim_starA).
  eauto using Asim.
Qed.

Lemma lock_spec x J :
  triple Model_hb_rf_acyclic
         (LockPred x J) (lock x) (fun _ ⇒ Astar (LockPred x J) J).
Proof.
  eapply rule_repeat2.
    eapply rule_let; [apply spin_spec with (J := J)|]; ins.
    eapply rule_cas with (QQ := LockQQ J) (QQ' := LockQQ J)
      (RR := fun v ⇒ if v == 0 then LockPred x J else Astar (LockPred x J) J);
    ins; desf.
    4: by ins.
    4: by ins; desf; ins.
    unfold LockPred; intros ? D; apply (sim_assn_sem (Asim_starC _ _)).
    by eapply implies_star_l, D; clear D; red; ins; subst.
  unfold LockQQ at 1 3; ins; unfold LockPred.
  intros ? D.
  eapply implies_star_r in D; [|by apply implies_star_l, Arel_split11].
  eapply sim_assn_sem, D; clear D.
  eapply Asim_trans, Asim_sym, Asim_starC.
  repeat (eapply Asim_trans, Asim_sym, Asim_starA).
  eauto using Asim.
  eapply rule_conseq.
    by apply rule_frame, rule_load_rlx3.
    by eapply implies_sim; unfold LockPred; eauto using Asim.
  unfold LockPred; ins; unfold LockQQ at 1; desf; desf;
    try solve[intros ? D; ins; desf]; eauto using implies_sim, Asim.
Qed.

Lemma precise_pt a b : precise (Apt a b).
Proof.
  red; ins; subst; split; ins.
  destruct hF, hF'; ins; f_equal.
  rewrite !hplus_unfold in *; desf; ins.
  extensionality y; apply (f_equal (fun f ⇒ f y)) in H0; ins.
  specialize (h y); specialize (h0 y).
  unfold hupd in *; desf; desf; ins; desf.
Qed.

Fixpoint has_no_rlx_writes E :=
  match E with
    | Evalue _ | Ealloc | Eload _ _ ⇒ True
    | Estore typ _ _ | Ecas typ _ _ _ _ ⇒ typ ≠ ATrlx ∧ typ ≠ ATacq
    | Elet E1 E2 ⇒ has_no_rlx_writes E1 ∧ ∀ v, has_no_rlx_writes (E2 v)
    | Epar E1 E2 ⇒ has_no_rlx_writes E1 ∧ has_no_rlx_writes E2
    | Erepeat E ⇒ has_no_rlx_writes E
  end.

Lemma triple_false mt E QQ :
  mt = Model_hb_rf_acyclic ∨ has_no_rlx_writes E →
  triple mt Afalse E QQ.
Proof.
  split; ins; desf; destruct mt; ins.
  repeat red; induction[res acts_cmd fst lst SEM] E; ins; desf; ins; desf;
  rewrite ?In_app in *; ins; desf; eauto;
  try match goal with H: lab _ = _ |- _ ⇒ rewrite H in *; ins; desf end.

  by rewrite In_flatten in *; desf; rewrite In_map in *; desf;
     destruct x0 as [ [ [] ] ]; ins; eauto.
Qed.

Message passing

The second example is a two-thread message passing program. The first thread initializes location a and performs a release write to channel c signalling that a is initialized. The second thread waits in a busy loop performing acquire reads from c until it notices the first thread's signal. It then accesses and updates the value of a.

Lemma mp_example mt :
  triple mt Aemp
    (LET a <- Ealloc IN
     LET c <- Ealloc IN
     [[c]]_ATrel <- 0 ;;
     PAR_BEGIN
         [[a]]_ATna <- 7 ;;
         [[c]]_ATrel <- 1
     PAR
         REPEAT [[c]]_ATacq END ;;
         LET v <- [[a]]_ATna IN
         [[a]]_ATna <- v + 1
     END ;;
     [[a]]_ATna)
    (fun v ⇒ if v == 8 then Atrue else Afalse).
Proof.
  pose (msgQQ a v := if v == 0 then Aemp else Apt a 7).
  eapply rule_let; [apply rule_alloc_na|intro a].
  eapply rule_let; [|intro c].
    eapply rule_conseq_pre; [apply rule_frame, rule_alloc_atom_acq|].
    instantiate (1 := Aptu a).
    by intros ? D; ins; subst; repeat eexists; eauto using hplus_emp_l.
  instantiate (1 := msgQQ a).
  eapply rule_let.
    eapply rule_let.
      do 2 apply rule_frame.
      eapply rule_conseq_pre; [by apply rule_store_rel2 with (QQ:=msgQQ a); vauto|].
      by apply implies_sim; Asim_simpl.
    ins.
    eapply rule_conseq_pre with
      (P := Astar (Astar (Arel c (msgQQ a)) (Aptu a))
                  (Astar (Aacq c (msgQQ a)) (Arainit c))); cycle 1.
     eapply implies_sim; repeat (eapply Asim_trans, Asim_sym, Asim_starA).
     apply Asim_sym; repeat (eapply Asim_trans, Asim_sym, Asim_starA).
     by apply Asim_star; eauto using Asim.
  apply rule_par.

  Case "Left thread".
  eapply rule_let.
    eapply rule_conseq; [| |eby ins].
      by apply rule_frame, rule_store_na2 with (typ := ATna); destruct mt; ins.
    by eauto using implies_sim, Asim.
  ins; eapply rule_conseq_pre; [by eapply rule_store_rel2; vauto|].
  by eauto using implies_sim, Asim.

  Case "Right thread".
  eapply rule_let.
    eapply rule_repeat.
    eapply rule_load_acq; vauto.
      by unfold msgQQ; ins; desf; eauto using precise_emp, precise_pt.
    ins; replace (hupd (msgQQ a) 0 Aemp) with (msgQQ a).
      by eauto using implies_sim, Asim.
    by extensionality v; unfold msgQQ, hupd; ins; desf.
  instantiate (1 := Astar (Apt a 8) Atrue).
  ins; unfold msgQQ at 2; desf.
   by eapply triple_false; vauto.
   eapply rule_conseq.
   eapply rule_frame with (P := Apt a 7).
    eapply rule_let.
      by apply rule_load_na; destruct mt; ins.
      ins; desf; desf.
        apply rule_store_na1; destruct mt; ins.
   by eapply triple_false; vauto.
  by eauto using implies_sim, Asim.
  by red; ins; desf; repeat eexists; ins.

  Case "Join".
  ins; eapply rule_conseq.
    by apply rule_frame, rule_load_na; destruct mt; ins.
    by eauto using implies_sim, Asim.
  by ins; desf; red; ins; desf.
Qed.

This page has been generated by coqdoc Imprint | Data protection