From fc6ca1fe78c4a579e6f8a4570ac0c5a28b215bbc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 24 Apr 2017 22:26:29 +0200
Subject: [PATCH] Mutex non-expansive, MutexGuard contractive
---
theories/lang/lib/lock.v | 2 +-
theories/typing/lib/mutex/mutex.v | 14 +++++++++++++-
theories/typing/lib/mutex/mutexguard.v | 11 ++++++++++-
3 files changed, 24 insertions(+), 3 deletions(-)
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index da77afe2..74c6b1c9 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -27,7 +27,7 @@ Section proof.
Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
- Global Instance lock_inv_ne γ l : NonExpansive (lock_proto γ l).
+ Global Instance lock_proto_ne γ l : NonExpansive (lock_proto γ l).
Proof. solve_proper. Qed.
Global Instance locked_timeless γ : TimelessP (locked γ).
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index f6c4e359..8d83630d 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -87,7 +87,19 @@ Section mutex.
Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
{ ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
- (* TODO: Non-expansiveness, compat with eqtype, Send+Sync if ty is Send. *)
+ Global Instance mutex_type_ne : TypeNonExpansive mutex.
+ Proof.
+ constructor;
+ solve_proper_core ltac:(fun _ => exact: type_dist2_S ||
+ f_type_equiv || f_contractive || f_equiv).
+ Qed.
+
+ Global Instance mutex_ne : NonExpansive mutex.
+ Proof.
+ constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+ Qed.
+
+ (* TODO: compat with eqtype, Send+Sync if ty is Send. *)
End mutex.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 0a04209e..66a94e0d 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -79,7 +79,16 @@ Section mguard.
Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
{ ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
- (* TODO: Contractivity, compat with lft_incl and eqtype.
+ Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
+ Proof.
+ constructor;
+ solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv
+ || exact: type_dist2_S).
+ Qed.
+ Global Instance mutexguard_ne α : NonExpansive (mutexguard α).
+ Proof. apply type_contractive_ne, _. Qed.
+
+ (* TODO: compat with lft_incl and eqtype.
MutexGuard is Sync if T is Send. *)
End mguard.
--
GitLab