Commit acea2a52 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'robbert/lock_namespace' into 'master'

Remove namespaces from lock API.

See merge request iris/iris!416
parents 365095a0 bb126fdc
...@@ -94,6 +94,7 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -94,6 +94,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
* Affine, absorbing, persistent and timeless instances for telescopes. * Affine, absorbing, persistent and timeless instances for telescopes.
* Better support for telescopes in the proof mode, i.e., all tactics should * Better support for telescopes in the proof mode, i.e., all tactics should
recognize and distribute telescopes now. recognize and distribute telescopes now.
* Remove namespace `N` from `is_lock`.
**Changes in heap_lang:** **Changes in heap_lang:**
......
...@@ -3,38 +3,40 @@ From iris.heap_lang Require Export lifting notation. ...@@ -3,38 +3,40 @@ From iris.heap_lang Require Export lifting notation.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Structure lock Σ `{!heapG Σ} := Lock { Structure lock Σ `{!heapG Σ} := Lock {
(* -- operations -- *) (** * Operations *)
newlock : val; newlock : val;
acquire : val; acquire : val;
release : val; release : val;
(* -- predicates -- *) (** * Predicates *)
(* name is used to associate locked with is_lock *) (** [name] is used to associate locked with [is_lock] *)
name : Type; name : Type;
is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ; (** No namespace [N] parameter because we only expose program specs, which
anyway have the full mask. *)
is_lock (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
locked (γ: name) : iProp Σ; locked (γ: name) : iProp Σ;
(* -- general properties -- *) (** * General properties of the predicates *)
is_lock_ne N γ lk : Contractive (is_lock N γ lk); is_lock_ne γ lk : Contractive (is_lock γ lk);
is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R); is_lock_persistent γ lk R : Persistent (is_lock γ lk R);
is_lock_iff N γ lk R1 R2 : is_lock_iff γ lk R1 R2 :
is_lock N γ lk R1 - (R1 R2) - is_lock N γ lk R2; is_lock γ lk R1 - (R1 R2) - is_lock γ lk R2;
locked_timeless γ : Timeless (locked γ); locked_timeless γ : Timeless (locked γ);
locked_exclusive γ : locked γ - locked γ - False; locked_exclusive γ : locked γ - locked γ - False;
(* -- operation specs -- *) (** * Program specs *)
newlock_spec N (R : iProp Σ) : newlock_spec (R : iProp Σ) :
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}}; {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}};
acquire_spec N γ lk R : acquire_spec γ lk R :
{{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ R }}}; {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ R }}};
release_spec N γ lk R : release_spec γ lk R :
{{{ is_lock N γ lk R locked γ R }}} release lk {{{ RET #(); True }}} {{{ is_lock γ lk R locked γ R }}} release lk {{{ RET #(); True }}}
}. }.
Arguments newlock {_ _} _. Arguments newlock {_ _} _.
Arguments acquire {_ _} _. Arguments acquire {_ _} _.
Arguments release {_ _} _. Arguments release {_ _} _.
Arguments is_lock {_ _} _ _ _ _ _. Arguments is_lock {_ _} _ _ _ _.
Arguments locked {_ _} _ _. Arguments locked {_ _} _ _.
Existing Instances is_lock_ne is_lock_persistent locked_timeless. Existing Instances is_lock_ne is_lock_persistent locked_timeless.
Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N γ lk: Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) γ lk:
Proper (() ==> ()) (is_lock L N γ lk) := ne_proper _. Proper (() ==> ()) (is_lock L γ lk) := ne_proper _.
...@@ -21,7 +21,8 @@ Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ. ...@@ -21,7 +21,8 @@ Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
Section proof. Section proof.
Context `{!heapG Σ, !lockG Σ} (N : namespace). Context `{!heapG Σ, !lockG Σ}.
Let N := nroot .@ "spin_lock".
Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ := Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
( b : bool, l #b if b then True else own γ (Excl ()) R)%I. ( b : bool, l #b if b then True else own γ (Excl ()) R)%I.
......
...@@ -37,7 +37,8 @@ Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ. ...@@ -37,7 +37,8 @@ Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
Section proof. Section proof.
Context `{!heapG Σ, !tlockG Σ} (N : namespace). Context `{!heapG Σ, !tlockG Σ}.
Let N := nroot .@ "ticket_lock".
Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ := Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
( o n : nat, ( o n : nat,
......
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