Add some comments

theories/examples/stack/proof_treiber_gps.v

@@ -17,7 +17,11 @@ Local Notation data := 1%nat (only parsing).
    memory.
   Furthermore, this implementation uses 0 and -1 as flags for EMPTY and
   FAIL_RACE repsectively, so if the client should not push elements with those
-  values, otherwise they'll lose resources. *)
+  values, otherwise they'll lose resources.
+
+  In order to support reclamation, we will need to track the freeable resources
+  more closely, and abandon [ReachableD] (see below). That may mean abandoning
+  GPS protocol altogether. *)
 
 (** The CMRA & functor we need. *)
 Class tstackG Σ := TreiberStackG { tstack_gpsG :> gpsIPG Σ unitProtocol; }.
@@ -42,7 +46,9 @@ Definition Reachable'
         match A with
         | nil     => ⌜l = 0⌝
         | v :: A' => ∃ l', ⌜l = (LitLoc l')⌝ ∗
-                      (* not strictly needed *) ⎡ † l' … 2 ⎤ ∗
+                      (* freeable resource is only needed for reclamation, which
+                        is not done yet *)
+                      ⎡ † l' … 2 ⎤ ∗
                       (l' >> data) ↦ #v ∗ P v ∗ ∃ q (n': lit),
                       (l' >> next) ↦{q} #n' ∗ ▷ F n' A'
         end)%I.
@@ -346,7 +352,7 @@ Proof.
   (* From HD we know s' is alive. *)
   iDestruct "HD" as (s1 ? q) "[Hs1 HD]". subst s'.
   (* we are leaking fractions of s1 ("Hs1") and others ("HD") here.
-    A non-leaking algorithm should have some way to retrieve this fraction.
+    A non-leaking algorithm should have some way to retrieve/avoid this fraction.
     Then the setup in this proof will not work any more. *)
   rewrite shift_0.
   wp_apply (GPS_iPP_CAS_live_loc (tstackN s) (Head P) _ _ _ s _ s1 #n _