change notation for tokens

chase-lev/chase-lev.tex

@@ -304,36 +304,36 @@ is consumed, thus ensures exclusivity between the permissions.
 
 For an element pushed to the queue at index $\tidx$ for the $i$-th time,
 we use two basic token types to model the permissions:
-a fractional ghost token $[P(\tidx,i)]_q$ and a unique ghost token $W(\tidx)$.
+a fractional ghost token $P_{q}(\tidx,i)$ and a unique ghost token $W(\tidx)$.
 The $i$-th represents the cycles of $\tidx$: by pushing and then popping, $\tidx$
 can be reused for several elements. We identify an element $\nnum$ pushed to the queue
 by the index $\tidx$ and the cycle $i$ of $\tidx$ used for $\nnum$.
-The pop-way permission for the escrow of $(\tidx,i)$ is the full fraction $[P(\tidx,i)]_1$.
-The steal-way permission for the escrow of $(\tidx,i)$ is $[P(\tidx,i)]_q \ast W(\tidx)$.
+The pop-way permission for the escrow of $(\tidx,i)$ is the full fraction $P_{1}(\tidx,i)$.
+The steal-way permission for the escrow of $(\tidx,i)$ is $P_{q}(\tidx,i) \ast W(\tidx)$.
 It's easy to see that the permissions satisfy our uniqueness and exclusivity requirements.
 
 How does the turning of pop-way permission into steal-way permission work?
 And how do $\pop$'s and $\steal$'s acquire these permissions?
 The pop-way permissions are first stored in the SC fence, using an SC invariant.
-If $\tidx$ is not stealable, the SC invariant stores $[P(\tidx,i)]_1$, where $i$ is the
+If $\tidx$ is not stealable, the SC invariant stores $P_{1}(\tidx,i)$, where $i$ is the
 most recent cycle of $\tidx$. If a $\pop$ tries to pop $\tidx$, it must be attempting
 to pop the element $(\tidx,i)$, and if it finds from the SC invariant that $\tidx$
-is not stealable, then it can acquire $[P(\tidx,i)]_1$ from the fence and thus
-use the escrow in the pop-way. Simultaneously when acquiring $[P(\tidx,i)]_1$,
+is not stealable, then it can acquire $P_{1}(\tidx,i)$ from the fence and thus
+use the escrow in the pop-way. Simultaneously when acquiring $P_{1}(\tidx,i)$,
 it asks the SC fence to allocate the pop-way permission $[P(\tidx,i+1)]_1$
 for the next cycle $i+1$ of $\tidx$\footnote{We have to do something with the permission
 to push here, to ensure agreement between pushes and pops.}.
 
 Now, the first attempt to steal $\tidx$ will turn $\tidx$ stealable, which
-translates to the SC invariant turning from storing $[P(\tidx,i)]_1$ to storing
-$[P(\tidx,i)]_q$ for some $q \in (0,1)$. $[P(\tidx,i)]_q$ is called the \emph{stealable permission}.
+translates to the SC invariant turning from storing $P_{1}(\tidx,i)$ to storing
+$P_{q}(\tidx,i)$ for some $q \in (0,1)$. $P_{q}(\tidx,i)$ is called the \emph{stealable permission}.
 Anyone owning the stealable permission of $(\tidx,i)$ knows that others can only
 steal, not pop, $(\tidx,i)$. So this permission allows one to enter the race for
 $(\tidx,i)$. This is the race between the CASes of $\pop$'s and $\steal$'s.
 There can be only one race for each index $\tidx$, so the prize of the race is
 the unique token $W(\tidx)$ (which has nothing to do with cycles, because
 the race can only be won once).
-Thus winning the race gives one the steal-way permission $[P(\tidx,i)]_q \ast W(\tidx)$ for $(\tidx,i)$,
+Thus winning the race gives one the steal-way permission $P_{q}(\tidx,i) \ast W(\tidx)$ for $(\tidx,i)$,
 which ensures that no one else can steal or pop $(\tidx,i)$.
 
 \paragraph{Queue-like-ness} We currently don't show this.
@@ -376,7 +376,7 @@ for $\nnum$ is:
 \def\TWES#1{\PRTINT{ES}{#1}}
 
 \begin{align*}
-  \TWES(\nnum,\tidx,i) \eqdef \Escrow{[P(\tidx,i)]_1 + [P(\tidx,i)]_q \ast W(\tidx) ~> E(\nnum)}
+  \TWES(\nnum,\tidx,i) \eqdef \Escrow{P_{1}(\tidx,i) + P_{q}(\tidx,i) \ast W(\tidx) ~> E(\nnum)}
 \end{align*}
 
 The $\push$ knows the exact index $\tidx$ and cycle $i$ to push $\nnum$ to, and it also has