Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq

theories/lang/lib/arc.v

@@ -7,6 +7,28 @@ From iris.algebra Require Import excl csum frac auth.
 From lrust.lang Require Import lang proofmode notation new_delete.
 Set Default Proof Using "Type".
 
+(* JH: while working on Arc, I think figured that the "weak count
+locking" mechanism that Rust is using and that is verified below may
+not be necessary.
+
+Instead, what can be done in get_mut is the following:
+  - First, do a CAS on the strong count to put it to 0 from the expected
+value 1. This has the effect, at the same time, of ensuring that no one
+else has a strong reference, and of forbidding other weak references to
+be upgraded (since the strong count is now at 0). If the CAS fail,
+simply return None.
+  - Second, check the weak count. If it is at 1, then we are sure that
+we are the only owner.
+  - Third, in any case write 1 in the strong count to cancel the CAS.
+
+What's wrong with this protocol? The "only" problem I can see is that if
+someone tries to upgrade a weak after we did the CAS, then this will
+fail even though this could be possible.
+
+RJ: Upgrade failing spuriously sounds like a problem severe enough to
+justify the locking protocol.
+*)
+
 Definition strong_count : val :=
   λ: ["l"], !ˢᶜ"l".
 

theories/typing/lib/join.v

@@ -81,6 +81,7 @@ Section join.
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
     iApply (type_new_subtype (Π[uninit R_A.(ty_size); uninit R_B.(ty_size)]));
+      (* FIXME: solve_typing should handle this without any aid. *)
       rewrite ?Z_nat_add; [solve_typing..|].
     iIntros (r); simpl_subst.
     iApply (type_memcpy R_A); [solve_typing..|].