Commit d831f1e2 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'master' into gen_proofmode

parents ac1a1276 adc0a095
......@@ -31,7 +31,7 @@ Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp Σ) : iProp Σ :=
( lv, l lv (lv = NONEV
v, lv = SOMEV v (Ψ v own γ (Excl ()))))%I.
w, lv = SOMEV w (Ψ w own γ (Excl ()))))%I.
Definition join_handle (l : loc) (Ψ : val iProp Σ) : iProp Σ :=
( γ, own γ (Excl ()) inv N (spawn_inv γ l Ψ))%I.
......
......@@ -36,7 +36,7 @@ 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).
Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
Proof. solve_proper. Qed.
(** The main proofs. *)
......@@ -90,6 +90,6 @@ End proof.
Typeclasses Opaque is_lock locked.
Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
......@@ -166,6 +166,6 @@ End proof.
Typeclasses Opaque is_lock issued locked.
Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
Canonical Structure ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; 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