basic arc code

theories/lang/arc.v

+From iris.base_logic.lib Require Import invariants.
+From iris.proofmode Require Import tactics.
+From iris.bi Require Import fractional.
+From iris.algebra Require Import excl csum frac auth.
+From lrust.lang Require Import notation new_delete.
+From gpfsl.gps Require Import middleware protocols.
+Set Default Proof Using "Type".
+
+(* Rust Arc has a maximum number of clones to prevent overflow. We currently
+  don't support this. *)
+
+Definition strong_count : val :=
+  λ: ["l"], !ᵃᶜ"l".
+
+Definition weak_count : val :=
+  λ: ["l"], !ᵃᶜ("l" +ₗ #1).
+
+Definition clone_arc : val :=
+  rec: "clone" ["l"] :=
+    let: "strong" := !ʳˡˣ"l" in
+    (* fully relaxed CAS *)
+    if: CAS "l" "strong" ("strong" + #1) Relaxed Relaxed Relaxed then #☠ else "clone" ["l"].
+
+Definition clone_weak : val :=
+  rec: "clone" ["l"] :=
+    let: "weak" := !ʳˡˣ("l" +ₗ #1) in
+    if: CAS ("l" +ₗ #1) "weak" ("weak" + #1) Relaxed Relaxed Relaxed then #☠ else "clone" ["l"].
+
+(*  // the value usize::MAX acts as a sentinel for temporarily "locking" the
+    // ability to upgrade weak pointers or downgrade strong ones; this is used
+    // to avoid races in `make_mut` and `get_mut`.
+    Her we use -1 for usize::MAX.
+*)
+Definition downgrade : val :=
+  rec: "downgrade" ["l"] :=
+    let: "weak" := !ʳˡˣ("l" +ₗ #1) in
+    if: "weak" = #(-1) then
+      (* -1 in weak indicates that somebody locked the counts; let's spin. *)
+      "downgrade" ["l"]
+    else
+      (*
+        // Unlike with Clone(), we need this to be an Acquire read to
+        // synchronize with the write coming from `is_unique`, so that the
+        // events prior to that write happen before this read.
+      *)
+      (* acquire CAS, i.e. relaxed fail read, acquire success read, relaxed write *)
+      if: CAS ("l" +ₗ #1) "weak" ("weak" + #1) Relaxed AcqRel Relaxed then #☠
+      else "downgrade" ["l"].
+
+Definition upgrade : val :=
+  rec: "upgrade" ["l"] :=
+    let: "strong" := !ʳˡˣ"l" in
+    if: "strong" = #0 then #false
+    else
+      if: CAS "l" "strong" ("strong" + #1) Relaxed Relaxed Relaxed then #true
+      else "upgrade" ["l"].
+
+Definition drop_weak : val :=
+  rec: "drop" ["l"] :=
+    (* This can ignore the lock because the lock is only held when there
+       are no other weak refs in existence, so this code will never be called
+       with the lock held. *)
+    let: "weak" := !ʳˡˣ("l" +ₗ #1) in
+    (* release CAS, i.e. relaxed fail read, relaxed success read, release write *)
+    if: CAS ("l" +ₗ #1) "weak" ("weak" - #1) Relaxed Relaxed AcqRel
+    then if: "weak" = #1 then FenceAcq ;; #true else #false
+    else "drop" ["l"].
+
+Definition drop_arc : val :=
+  rec: "drop" ["l"] :=
+    let: "strong" := !ʳˡˣ"l" in
+    if: CAS "l" "strong" ("strong" - #1) Relaxed Relaxed AcqRel
+    then if: "strong" = #1 then FenceAcq ;; #true else #false
+    else "drop" ["l"].
+
+Definition try_unwrap : val :=
+  λ: ["l"],
+    (* release CAS *)
+    if: CAS "l" #1 #0 Relaxed Relaxed AcqRel
+    then FenceAcq ;; #true
+    else #false.
+
+Definition is_unique : val :=
+  λ: ["l"],
+    (* Try to acquire the lock for the last ref by CASing weak count from 1 to -1. *)
+    (* acquire CAS *)
+    if: CAS ("l" +ₗ #1) #1 #(-1) Relaxed AcqRel Relaxed then
+      let: "strong" := !ʳˡˣ"l" in
+      let: "unique" := "strong" = #1 in
+      "l" +ₗ #1 <-ʳᵉˡ #1;;
+      "unique"
+    else
+      #false.
+
+(* to be used in make_mut *)
+(*// Note that we hold both a strong reference and a weak reference.
+  // Thus, releasing our strong reference only will not, by itself, cause
+  // the memory to be deallocated.
+  //
+  // Use Acquire to ensure that we see any writes to `weak` that happen
+  // before release writes (i.e., decrements) to `strong`. Since we hold a
+  // weak count, there's no chance the ArcInner itself could be
+  // deallocated. *)
+(* - Returns #2 to signal that there is another strong pointer, and trigger a deep copy.
+   - Returns #1 to signal that we have collected the last strong pointer and
+   the main content, but there are more than 1 weak pointers left, so its the job
+   of the last weak pointer to drop the remain resources.
+   - Returns #0 to signal that we have collected both the last strong and weak pointer,
+   so it's time to clean up everything. To call drop we reset "strong" back to 1.
+   The write "l" <- #1 seems to be good enough (TODO: really?), but C/Rust
+   uses a release write, may be because the strict distinction between atomics
+   and non-atomics. (TODO: is a relaxed write enough?) *)
+Definition try_unwrap_full : val :=
+  λ: ["l"],
+    (* acquire CAS *)
+    if: CAS "l" #1 #0 Relaxed AcqRel Relaxed then
+      if: !ʳˡˣ("l" +ₗ #1) = #1 then "l" <- #1;; #0
+      else #1
+    else #2.
+