Commit 0ccaa796 authored by Robbert's avatar Robbert

Merge branch 'robbert/lock_contractive' into 'master'

Make `_iff` and `_alter` lemmas for invariants consistent, and add `_iff` lemma for locks

See merge request iris/iris!414
parents df3450a6 31d5df29
......@@ -83,6 +83,11 @@ Coq development, but not every API-breaking change is listed. Changes marked
* Make use of `ofe_iso` in the COFE solver.
* The functions `{o,r,ur}Functor_diag` are no longer coercions, and renamed into
`{o,r,ur}Functor_apply` to better match their intent.
* Change `inv_iff`, `cinv_iff` and `na_inv_iff` to make order of arguments
consistent and more convenient for `iApply`. They are now of the form
`inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q` and (similar for `na_inv_iff` and
`cinv_iff`), following e.g., `inv_alter` and `wp_wand`.
* Add lemma `is_lock_iff` and show that `is_lock` is contractive.
**Changes in heap_lang:**
......
......@@ -53,11 +53,10 @@ Section proofs.
iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp).
Qed.
Lemma cinv_iff N γ P P' :
(P P') - cinv N γ P - cinv N γ P'.
Lemma cinv_iff N γ P Q : cinv N γ P - (P Q) - cinv N γ Q.
Proof.
iIntros "#HP". iApply inv_iff. iIntros "!> !>".
iSplit; iIntros "[?|$]"; iLeft; by iApply "HP".
iIntros "HI #HPQ". iApply (inv_iff with "HI"). iIntros "!> !>".
iSplit; iIntros "[?|$]"; iLeft; by iApply "HPQ".
Qed.
(*** Allocation rules. *)
......
......@@ -97,18 +97,17 @@ Section inv.
Global Instance inv_persistent N P : Persistent (inv N P).
Proof. rewrite inv_eq. apply _. Qed.
Lemma inv_alter N P Q:
inv N P - (P - Q (Q - P)) - inv N Q.
Lemma inv_alter N P Q : inv N P - (P - Q (Q - P)) - inv N Q.
Proof.
rewrite inv_eq. iIntros "#HI #Acc !>" (E H).
rewrite inv_eq. iIntros "#HI #HPQ !>" (E H).
iMod ("HI" $! E H) as "[HP Hclose]".
iDestruct ("Acc" with "HP") as "[$ HQP]".
iDestruct ("HPQ" with "HP") as "[$ HQP]".
iIntros "!> HQ". iApply "Hclose". iApply "HQP". done.
Qed.
Lemma inv_iff N P Q : (P Q) - inv N P - inv N Q.
Lemma inv_iff N P Q : inv N P - (P Q) - inv N Q.
Proof.
iIntros "#HPQ #HI". iApply (inv_alter with "HI").
iIntros "#HI #HPQ". iApply (inv_alter with "HI").
iIntros "!> !> HP". iSplitL "HP".
- by iApply "HPQ".
- iIntros "HQ". by iApply "HPQ".
......
......@@ -43,10 +43,10 @@ Section proofs.
Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
Proof. rewrite /na_inv; apply _. Qed.
Lemma na_inv_iff p N P Q : (P Q) - na_inv p N P - na_inv p N Q.
Lemma na_inv_iff p N P Q : na_inv p N P - (P Q) - na_inv p N Q.
Proof.
iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
iIntros "HI #HPQ". rewrite /na_inv. iDestruct "HI" as (i ?) "HI".
iExists i. iSplit; first done. iApply (inv_iff with "HI").
iIntros "!> !>".
iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
Qed.
......
......@@ -13,8 +13,10 @@ Structure lock Σ `{!heapG Σ} := Lock {
is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
locked (γ: name) : iProp Σ;
(* -- general properties -- *)
is_lock_ne N γ lk : NonExpansive (is_lock N γ lk);
is_lock_ne N γ lk : Contractive (is_lock N γ lk);
is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R);
is_lock_iff N γ lk R1 R2 :
is_lock N γ lk R1 - (R1 R2) - is_lock N γ lk R2;
locked_timeless γ : Timeless (locked γ);
locked_exclusive γ : locked γ - locked γ - False;
(* -- operation specs -- *)
......
......@@ -36,8 +36,8 @@ Section proof.
Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
Proof. solve_proper. Qed.
Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
Proof. solve_proper. Qed.
Global Instance is_lock_contractive γ l : Contractive (is_lock γ l).
Proof. solve_contractive. Qed.
(** The main proofs. *)
Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
......@@ -45,6 +45,16 @@ Section proof.
Global Instance locked_timeless γ : Timeless (locked γ).
Proof. apply _. Qed.
Lemma is_lock_iff γ lk R1 R2 :
is_lock γ lk R1 - (R1 R2) - is_lock γ lk R2.
Proof.
iDestruct 1 as (l ->) "#Hinv"; iIntros "#HR".
iExists l; iSplit; [done|]. iApply (inv_iff with "Hinv").
iIntros "!> !#"; iSplit; iDestruct 1 as (b) "[Hl H]";
iExists b; iFrame "Hl"; destruct b;
first [done|iDestruct "H" as "[$ ?]"; by iApply "HR"].
Qed.
Lemma newlock_spec (R : iProp Σ):
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
......@@ -92,5 +102,6 @@ End proof.
Typeclasses Opaque is_lock locked.
Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
{| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
......@@ -54,11 +54,10 @@ Section proof.
Definition locked (γ : gname) : iProp Σ := ( o, own γ ( (Excl' o, GSet )))%I.
Global Instance lock_inv_ne γ lo ln :
NonExpansive (lock_inv γ lo ln).
Proof. solve_proper. Qed.
Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk).
Global Instance lock_inv_ne γ lo ln : NonExpansive (lock_inv γ lo ln).
Proof. solve_proper. Qed.
Global Instance is_lock_contractive γ lk : Contractive (is_lock γ lk).
Proof. solve_contractive. Qed.
Global Instance is_lock_persistent γ lk R : Persistent (is_lock γ lk R).
Proof. apply _. Qed.
Global Instance locked_timeless γ : Timeless (locked γ).
......@@ -70,6 +69,16 @@ Section proof.
iDestruct (own_valid_2 with "H1 H2") as %[[] _].
Qed.
Lemma is_lock_iff γ lk R1 R2 :
is_lock γ lk R1 - (R1 R2) - is_lock γ lk R2.
Proof.
iDestruct 1 as (lo ln ->) "#Hinv"; iIntros "#HR".
iExists lo, ln; iSplit; [done|]. iApply (inv_iff with "Hinv").
iIntros "!> !#"; iSplit; iDestruct 1 as (o n) "(Ho & Hn & H● & H)";
iExists o, n; iFrame "Ho Hn H●";
(iDestruct "H" as "[[H◯ H]|H◯]"; [iLeft; iFrame "H◯"; by iApply "HR"|by iRight]).
Qed.
Lemma newlock_spec (R : iProp Σ) :
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
......@@ -163,5 +172,6 @@ End proof.
Typeclasses Opaque is_lock issued locked.
Canonical Structure ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
{| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment