first commit

.gitignore

+*.vo
+*.vio
+*.v.d
+*.glob
+*.cache
+*.aux
+\#*\#
+.\#*
+*~
+*.bak
+.coq-native/
+Makefile.coq

_CoqProject

+-Q . iris
+incr.v
+sync.v
+pair_cas.v

incr.v

+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import invariants tactics.
+From iris.heap_lang Require Import proofmode notation.
+From iris.tests Require Import atomic sync.
+From iris.heap_lang Require Import spin_lock.
+
+Section sync_incr.
+  Context `{!heapG Σ, !lockG Σ} (N : namespace).
+
+  Definition α (l: val) (v: Z) := (∃ l': loc, l = #l' ∧ l' ↦ #v)%I.
+  Definition β (l: val) (v: Z) ret := (∃ l': loc, l = #l' ∧ ret = #v ★ l' ↦ #(v + 1))%I.
+  Variable R: val → iProp Σ.
+  
+  Definition incr_seq: val :=
+    λ: "l",
+       let: "v" := !"l" in
+       "l" <- "v" + #1;;
+       "v".
+
+  Lemma incr_seq_spec:
+    ∀ (l: val) (x: Z) (Φ: val → iProp Σ),
+      heapN ⊥ N →
+      heap_ctx ★ α l x ★ (∀ v, β l x v -★ Φ v)
+      ⊢ WP incr_seq l {{ Φ }}.
+  Proof.
+    rewrite /α /β.
+    iIntros (l x Φ HN) "(#Hh & Hl & HΦ)".
+    wp_let. iDestruct "Hl" as (l') "[% Hl]". subst.
+    wp_load. wp_let. wp_op. wp_store.
+    iSpecialize ("HΦ" $! #x with "[Hl]"); first by eauto.
+    by iApply "HΦ".
+  Qed.
+
+  Local Opaque incr_seq.
+
+  Definition cons: val := λ: <>, ref #0.
+
+  Definition cons_spec :=
+    ∀ (Φ: val → iProp Σ),
+      heapN ⊥ N →
+      heap_ctx ★ (∀ v, R v -★ Φ v)%I
+      ⊢ WP cons #() {{ Φ }}.
+  
+  Lemma mk_increr_spec:
+    ∀ (Φ: val → iProp Σ),
+      heapN ⊥ N →
+      cons_spec →
+      heap_ctx ★
+      (∀ obj: val, conc_obj_triple α β (nclose heapN) ⊤ (obj #()) -★ Φ obj)
+      ⊢ WP mk_whatever cons incr_seq #() {{ Φ }}.
+  Proof.
+    iIntros (Φ HN Hcons) "[#Hh HΦ]".
+    iApply mk_whatever_spec=>//.
+    - rewrite /whatever_seq_spec. apply incr_seq_spec.
+    - by iFrame.
+ Qed.
+End sync_incr.

pair_cas.v

+From iris.program_logic Require Export weakestpre hoare.
+From iris.proofmode Require Import invariants ghost_ownership.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang.lib Require Import spin_lock.
+From iris.algebra Require Import excl.
+From iris.tests Require Import sync.
+Import uPred.
+
+(* CAS, load and store to pair of locations *)
+(* TODO: Make it mroe realistic by taking two parameters rather than sharing one for both locations*)
+(* TODO: Eliminate the duplication of spec code *)
+(* TODO: release spec of lock user *)
+
+Definition casp_seq' (l1 l2: loc) : val :=
+  λ: "vp",
+     let: "oldv" := Fst "vp" in
+     let: "newv" := Snd "vp" in
+     if: !(Fst (#l1, #l2)) = "oldv"
+       then if: !(Snd (#l1, #l2)) = "oldv"
+              then (Fst (#l1, #l2)) <- "newv";; (Snd (#l1, #l2)) <- "newv";; #true
+              else #false
+       else #false.
+
+Definition casp_seq: val :=
+    λ: "lp" "vp",
+       let: "oldv" := Fst "vp" in
+       let: "newv" := Snd "vp" in
+       if: !(Fst "lp") = "oldv"
+         then if: !(Snd "lp") = "oldv"
+                then (Fst "lp") <- "newv";; (Snd "lp") <- "newv";; #true
+                else #false
+         else #false.
+
+Definition loadp_seq' (l1 l2: loc) : val := λ: "x", (!(Fst (#l1, #l2)), !(Snd (#l1, #l2))).
+
+Definition loadp_seq: val := λ: "lp" "x", (!(Fst "lp"), !(Snd "lp")).
+
+Definition storep_seq: val :=
+  λ: "lp" "x",
+     Fst "lp" <- "x";;
+     Snd "lp" <- "x".
+
+Definition storep_seq' (l1 l2: loc) : val :=
+  λ: "x",
+     Fst (#l1, #l2) <- "x";;
+     Snd (#l1, #l2) <- "x".
+
+(* constructor that returns operations bound to the same two-locations *)
+Definition make_pair: val :=
+  λ: "v1" "v2",
+     let: "l1" := ref "v1" in
+     let: "l2" := ref "v2" in
+     let: "s" := mk_sync #() in
+     ("s" (casp_seq ("l1", "l2")),
+      "s" (loadp_seq ("l1", "l2")),
+      "s" (storep_seq ("l1", "l2"))).
+
+Definition casp: val := λ: "s", Fst (Fst "s").
+Definition loadp: val := λ: "s", Snd (Fst "s").
+Definition storep: val := λ: "s", Snd "s".
+
+Global Opaque casp_seq storep_seq loadp_seq.
+
+(* Instantiate a (stupid) lock of a pair of resource *)
+
+Definition newplock : val := λ: <>, make_pair #false #false.
+
+Definition pacquire : val :=
+  rec: "pacquire" "p" :=
+    if: casp "p" (#false, #true) then #() else "pacquire" "p".
+
+Definition prelease : val :=
+    λ: "p", storep "p" #false.
+
+Section proof.
+  Context `{!heapG Σ, !lockG Σ} (N: namespace).
+
+  Definition plocked : iProp Σ :=
+    (∃ (γ1 γ2: gname),
+       heapN ⊥ N ∧ heap_ctx ∧
+       own γ1 (Excl ()) ∧ own γ2 (Excl ()))%I.
+
+  Definition plock_inv (γ1 γ2 : gname) (R1 R2: iProp Σ) (l1 l2: loc) : iProp Σ :=
+    (∃ (b1 b2: bool),
+       l1 ↦ #b1 ★ l2 ↦ #b2 ★
+       (if b1 then True else own γ1 (Excl ()) ★ R1) ★
+       (if b2 then True else own γ2 (Excl ()) ★ R2))%I.
+
+  Definition is_plock (fs: val) (R1 R2 : iProp Σ) : iProp Σ :=
+    (∃ (l1 l2: loc) (f1 f2 f3: val) (γ1 γ2: gname),
+       heapN ⊥ N ∧ heap_ctx ∧ fs = (f1, f2, f3)%V ∧
+       refines f1 (casp_seq' l1 l2) (plock_inv γ1 γ2 R1 R2 l1 l2) ∧
+       refines f2 (loadp_seq' l1 l2) (plock_inv γ1 γ2 R1 R2 l1 l2) ∧
+       refines f3 (storep_seq' l1 l2) (plock_inv γ1 γ2 R1 R2 l1 l2))%I.
+
+  Global Instance is_plock_persistent p R1 R2: PersistentP (is_plock p R1 R2).
+  Proof. apply _. Qed.
+
+  Lemma not_false_is_true: ∀ b: bool, b ≠ false -> b = true.
+  Proof. intros b H. destruct (Sumbool.sumbool_of_bool b); by (try contradiction). Qed.
+
+  Lemma newplock_spec (R1 R2: iProp Σ) (Φ: val → iProp Σ):
+    heapN ⊥ N →
+    heap_ctx ★ R1 ★ R2 ★ (∀ p, is_plock p R1 R2 -★ Φ p)
+    ⊢ WP newplock #() {{ Φ }}.
+  Proof.
+    iIntros (HN) "(#? & HR1 & HR2 & HΦ)".
+    wp_seq. wp_let. wp_let.
+    wp_alloc l1 as "Hl1". wp_let.
+    iVs (own_alloc (Excl ())) as (γ1) "Hγ1"; first done.
+    wp_alloc l2 as "Hl2". wp_let.
+    iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
+    wp_bind (mk_sync _).
+    iApply (mk_sync_spec_wp _ (plock_inv γ1 γ2 R1 R2 l1 l2)); try by auto.
+    iSplit; first by auto.
+    iSplitR "HΦ".
+    + rewrite /plock_inv.
+      iExists false, false.
+      by iFrame.
+    + iIntros (s) "#Hs".
+      wp_let. wp_bind (s _).
+      iApply wp_wand_r.
+      iSplitR "HΦ".
+      { wp_let. wp_bind (λ: _, _)%E. wp_value. iApply "Hs". }
+      iIntros (v) "HRcas".
+      wp_bind (s _)%E.
+      iApply wp_wand_r.
+      iSplitR "HRcas HΦ".
+      { wp_let. wp_bind (λ: _, _)%E.
+        wp_value. (* XXX: manually force lambda to be value *)
+        iApply "Hs". }
+      iIntros (v0) "HRload".
+      wp_bind (s _)%E.
+      iApply wp_wand_r.
+      iSplitR "HRcas HRload HΦ".
+      { wp_let. wp_bind (λ: _, _)%E. wp_value. iApply "Hs". }
+      iIntros (v1) "HRstore".
+      wp_value.
+      iApply "HΦ".
+      rewrite /is_plock. iExists l1, l2, _, _, _, γ1, γ2.
+      repeat (iSplit; first by auto).
+      rewrite /casp_seq'.
+      iApply "HRstore".
+  Qed.
+
+  Lemma pacquire_spec (p: val) (R1 R2: iProp Σ) (Φ : val → iProp Σ):
+    is_plock p R1 R2 ★ (plocked -★ R1 -★ R2 -★ Φ #()) ⊢ WP pacquire p {{ Φ }}.
+  Proof.
+    iIntros "(#Hp & HΦ)".
+    iLöb as "Hl".
+    wp_rec. wp_let.
+    rewrite /is_plock /refines.
+    iDestruct "Hp" as (l1 l2 casp loadp storep γ1 γ2) "(#? & #? & % & #HRcas & _ & #HRstore)".
+    subst. wp_proj. wp_proj. wp_bind (casp _).
+    iAssert ({{ True }} casp (#false%V, #true%V)%E {{ z, z = #false ∨ (z =#true ★ plocked ★ R1 ★ R2)}})%I as "#HP".
+    (* prove the contextual property of casp closure returned from constructor *)
+    {
+      iApply ("HRcas" with "[]")=>//.
+      iIntros "!# [Hplk _]".
+      repeat (try (wp_let); try wp_proj).
+      iDestruct "Hplk" as (b1 b2) "(Hl1 & Hl2 & Hdisj1 & Hdisj2)".
+      wp_load.
+      destruct b1.
+      - wp_op=>[|_]//.
+        destruct b2; wp_if.
+        + iSplitL; last by iLeft.
+          iExists true, true. by iFrame.
+        + iSplitL; last by auto.
+          iExists true, false. by iFrame.
+      - wp_op=>[_|]//.
+        destruct b2; wp_if; wp_proj; wp_load.
+        + wp_op=>[_|]// _; wp_if.
+          iSplitL; last by iLeft.
+          iExists false, true. by iFrame.
+        + wp_op=>[_|]//. wp_if.
+          wp_proj. wp_store. wp_proj. wp_store.
+          iSplitL "Hl1 Hl2".
+          { rewrite /plock_inv. iExists true, true.
+            iFrame. iSplitL; done. }
+          iRight.
+          iDestruct "Hdisj1" as "[Ho1 HR1]".
+          iDestruct "Hdisj2" as "[Ho2 HR2]".
+          iFrame. iSplitR; first by auto.
+          iExists γ1, γ2. iFrame.
+          iVsIntro. iSplit; by auto.
+    }
+    iApply wp_wand_r.
+    iSplitR; first by iApply "HP".
+    iIntros (v) "[%|(% & Hlocked & HR1 & HR2)]"; subst.
+    - wp_if. iApply "Hl". iApply "HΦ".
+    - wp_if. iVsIntro. iApply ("HΦ" with "Hlocked HR1 HR2").
+  Qed.
+
+End proof.

sync.v

+From iris.program_logic Require Export weakestpre hoare.
+From iris.proofmode Require Import invariants ghost_ownership.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang.lib Require Import spin_lock.
+From iris.tests Require Import atomic.
+Import uPred.
+
+(* See CaReSL paper §3.2 *)
+Definition mk_sync: val :=
+  λ: <>,
+       let: "l" := newlock #() in
+       λ: "f" "x",
+          acquire "l";;
+          let: "ret" := "f" "x" in
+          release "l";;
+          "ret".
+
+Global Opaque mk_sync.
+
+Section proof.
+  Context `{!heapG Σ, !lockG Σ} (N: namespace).
+
+  (* concurrent object triple: R, p . <l, α p l> e <v, β p l v>*)
+  Definition conc_obj_triple {A: Type}
+             (α: val → A → iProp Σ)
+             (β: val → A → val → iProp Σ)
+             (Ei Eo: coPset)
+             (e: expr) : iProp Σ :=
+    (∀ P Q,
+       (□ (∀ (R: val → iProp Σ) p,
+             P ★ R p -★
+               ∃ l: A, α p l ★
+                 (∀ v, β p l v -★ Q l v ★ R p)))
+          -★ {{ P }} e {{ v, ∃ l, Q l v }})%I.
+
+  Arguments conc_obj_triple {_} _ _ _ _ _.
+  
+  (* f' refines f *)
+  Definition refines (f' f: val) (R: iProp Σ): iProp Σ :=
+    (□ ∀ (x: expr) (v: val) (P: iProp Σ) (Q: val -> iProp Σ),
+         to_val x = Some v -★
+         {{ R ★ P }} f x {{ z, R ★ Q z }} -★
+         {{ P }} f' x {{ z, Q z }})%I.
+
+  Global Instance refines_persistent f f' R: PersistentP (refines f f' R).
+  Proof. apply _. Qed.
+
+  Global Opaque refines.
+  
+  Definition is_syncer (R: iProp Σ) (s: val) : iProp Σ :=
+    (∀ (f : val), WP s f {{ f', refines f' f R }})%I.
+
+  Lemma mk_sync_spec_wp:
+    ∀ (R: iProp Σ) (Φ: val -> iProp Σ),
+      heapN ⊥ N →
+      heap_ctx ★ R ★ (∀ s, □ (is_syncer R s) -★ Φ s) ⊢ WP mk_sync #() {{ Φ }}.
+  Proof.
+    iIntros (R Φ HN) "(#Hh & HR & HΦ)".
+    wp_seq. wp_bind (newlock _).
+    iApply newlock_spec; first by auto.
+    iSplitR "HR HΦ"; first by auto.
+    iFrame "HR".
+    iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
+    rewrite /is_syncer. iIntros (f).
+    wp_let. iVsIntro. rewrite /refines. iIntros "!#".
+    iIntros (x v P Q <-%of_to_val) "#Hf !# HP".
+    wp_let.
+    wp_bind (acquire _).
+    iApply acquire_spec.
+    iSplit; first by auto.
+    iIntros "Hlocked R".
+    wp_seq. wp_bind (f _).
+    iDestruct ("Hf" with "[R HP]") as "Hf'"; first by iFrame.
+    iApply wp_wand_r.
+    iSplitL "Hf'"; first by auto.
+    iIntros (v') "[HR HQv]".
+    wp_let.
+    wp_bind (release _).
+    iApply release_spec.
+    iFrame "HR".
+    iSplitR; eauto.
+    iFrame.
+    by wp_seq.
+  Qed.
+End proof.
+
+Section sync_atomic.
+  Context `{!heapG Σ, !lockG Σ} (N : namespace) {A: Type}.
+
+  Variable α: val → A → iProp Σ.
+  Variable β: val → A → val → iProp Σ.
+  Variable f_cons f_seq: val.
+  Variable R: val → iProp Σ.
+
+  Definition mk_whatever (f_cons: val) (f_seq: val) : val :=
+    λ: <>,
+         let: "x" := f_cons #() in
+         let: "s" := mk_sync #() in
+         "s" (λ:<>, f_seq "x").
+
+  Definition whatever_triple (obj: val) :=
+    conc_obj_triple α β (nclose heapN) ⊤ (obj #()).
+
+  Definition whatever_seq_spec :=
+    ∀ (p: val) (l: A) (Φ: val → iProp Σ),
+      heapN ⊥ N →
+      heap_ctx ★ α p l ★ (∀ v, β p l v -★ Φ v)
+      ⊢ WP f_seq p {{ Φ }}.
+
+  Definition f_cons_spec :=
+    ∀ (Φ: val → iProp Σ),
+      heapN ⊥ N →
+      heap_ctx ★ (∀ v, R v -★ Φ v)%I
+      ⊢ WP f_cons #() {{ Φ }}.
+  
+  Lemma mk_whatever_spec:
+    ∀ (Φ: val → iProp Σ),
+      heapN ⊥ N →
+      whatever_seq_spec →
+      f_cons_spec →
+      heap_ctx ★      
+      (∀ obj, whatever_triple obj -★ Φ obj)
+      ⊢ WP mk_whatever f_cons f_seq #() {{ Φ }}.
+  Proof.
+    iIntros (Φ HN Hseq Hcons) "[#Hh HΦ]".
+    wp_let. wp_bind (f_cons _). iApply Hcons=>//.
+    iFrame "Hh".
+    iIntros (v) "HR".
+    wp_let. rewrite /mk_sync. (* TODO: use the derived lemmas above *)
+    wp_seq. wp_bind (newlock _). iApply (newlock_spec)=>//.
+    iFrame "Hh HR".
+    iIntros (lk γ) "#Hlk".
+    repeat wp_let.
+    iApply "HΦ".
+    rewrite /whatever_triple /conc_obj_triple.
+    iIntros (P Q) "#H".
+    iAlways. iIntros "HP". wp_seq.
+    iSpecialize ("H" $! R v).
+    wp_bind (acquire _).
+    iApply acquire_spec.
+    iFrame "Hlk". iIntros "Hlked HR".
+    iDestruct ("H" with "[HP HR]") as (x) "[Hl Hnext]"; first by iFrame.
+    wp_seq. wp_let.
+    iApply Hseq=>//. iFrame "Hh Hl".
+    iIntros (v') "Hbeta".
+    iDestruct ("Hnext" $! v' with "Hbeta") as "[HQ HR]".
+    wp_let. wp_bind (release _). iApply release_spec.
+    iFrame "Hlk Hlked HR".
+    wp_seq. iVsIntro. by iExists x.
+  Qed.
+End sync_atomic.