From 82d08c14683be614627849e491fd38319e81e342 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Jun 2019 14:59:43 +0200
Subject: [PATCH] expand comments

---
 theories/logatom/conditional_increment/cinc.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index e5d87328..f44a503d 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -188,8 +188,10 @@ Section conditional_counter.
      Remember that the thread winning the CAS might be just helping.  The token
      is owned by the thread whose request this is.
      In this state, [l_ghost_winner] serves as a token to make sure that
-     only the CAS winner can transition to here, and [loc_token l] serves as a
-     "location" token to ensure there is no ABA going on. *)
+     only the CAS winner can transition to here, and owning half of[l] serves as a
+     "location" token to ensure there is no ABA going on. Notice how [counter_inv]
+     owns *more than* half of its [l], which means we know that the [l] there
+     and here cannot be the same. *)
   Definition done_state Q (l l_ghost_winner : loc) (γ_t : gname) :=
     ((Q ∨ own_token γ_t) ∗ l_ghost_winner ↦ - ∗ l ↦{1/2} -)%I.
 
@@ -210,6 +212,8 @@ Section conditional_counter.
 
   Definition counter_inv γ_b γ_n f c :=
     (∃ (b : bool) (l : loc) (q : Qp) (s : abstract_state),
+       (* We own *more than* half of [l], which shows that this cannot
+          be the [l] of any [state] protocol in the [done] state. *)
        f ↦ #b ∗ c ↦{1/2} #l ∗ l ↦{1/2 + q} (state_to_val s) ∗
        own γ_b (● Excl' b) ∗
        match s with
-- 
GitLab