feat(report): update proof

Author: huydo862003

report/chapters/index.typ

@@ -27,5 +27,5 @@
   ),
 )
 
-// #{ include "./theoretical-aspects/index.typ" }
-// #pagebreak()
+#{ include "./theoretical-aspects/index.typ" }
+#pagebreak()

report/chapters/theoretical-aspects/index.typ

@@ -82,9 +82,7 @@ The most noticeable difference from the sequential specification of the SPSC que
 
 In this section, we specify and prove a theorem for establishing dLTQueue and Slotqueue's correctness. Our theorem draws inspiration from @aspect-proof and @tss, in that we specify some properties that is sufficient for a linearizable history. However, @tss provided a theorem for stacks while @aspect-proof could only work with unbounded queues. Therefore, we provide a similar set of properties that work with bounded queues that maintain local buffers.
 
-We consider a history $H$.
-
-We append to $H$ a large enough number of dequeues so that any successfully-enqueued values should have been dequeued out. If we can prove that this extended history $H'$ is linearizable, then we can also prove that $H$ is linearizable.
+We consider a history $H$. We append to $H$ a large enough number of dequeues so that any successfully-enqueued values should have been dequeued out. If we can prove that this extended history $H'$ is linearizable, then we can also prove that $H$ is linearizable.
 
 Denote:
 - $M$ as the set of operations in $H'$.
@@ -98,10 +96,10 @@ In addition to the precedence partial order $->^(p r)$, there is also a relation
 
 For simplicity, we assume every enqueue enqueues a unique value.
 
-Consider the following properties that the history $H'$ can possess. The $=>$ is taken to mean the $->$ connective in propositional logic so as not to confuse with $->^(p r)$ and $->^(v a l)$.
-+ Every successful enqueue is matched by a dequeue: $forall e in M. E n q (e) and not F a i l e d(e) => exists d in M. e ->^(v a l) d$.
+Consider the following properties that the history $H'$ can possess. The $=>$ is taken to mean the $->$ connective, and $<=>$ is taken to mean the $<->$ connective in propositional logic so as not to confuse with $->^(p r)$ and $->^(v a l)$.
++ Every successful enqueue is matched by a dequeue: $forall e in M. E n q (e) and not F a i l e d(e) <=> E n q(e) and  exists d in M. e ->^(v a l) d$.
 + A failed enqueue cannot be matched: $forall e, d in M. F a i l e d(e) => e arrow.not^(v a l) d$.
-+ A dequeue can not dequeue a value out of nowhere: $forall d in M. D e q(d) and not E m p(d) => exists e in M. e->^(v a l) d$.
++ A dequeue can not dequeue a value out of nowhere: $forall d in M. D e q(d) and not E m p(d) <=> D e q(d) and exists e in M. e->^(v a l) d$.
 + A dequeue can not dequeue a future value: $forall e,d in M.e->^(v a l) d => d arrow.not^(p r)e$.
 + An enqueue can only be matched once by a dequeue: $forall e,d_1,d_2 in M.e ->^(v a l) d_1 and e ->^(v a l) d_2 =>d_1 = d_2$.
 + A dequeue can only be matched once by an enqueue: $forall e_1,e_2,d in M.e_1 ->^(v a l) d and e_2 ->^(v a l) d =>e_1 = e_2$.
@@ -132,16 +130,22 @@ We prove the following theorem.
 
   We prove that $->^(a u x)$ is irreflexive. Suppose the contrary, this must be caused by a cycle in $prec$. Suppose the shortest cycle is $m_0 prec dots prec m_k prec m_0$.
 
-  If there are at least two dequeues in the cycle $d_0$ and $d_1$. Because our history is an MPSC queue, $d_0$ and $d_1$ must be related by $->^(p r)$, suppose $d_0 ->^(p r) d_1$. If these two dequeues are not adjacent, we can create a smaller cycle by removing the operations between $d_0$ and $d_1$ in the old cycle. This means there are at most two dequeues in the cycle, and these two dequeues must be adjacent.
-
   We can easily prove that the cycle cannot have length 1 or 2. Suppose the cycle has length at least 3.
 
+  If there are at least two dequeues in the cycle $d_0$ and $d_1$, because our history is an MPSC queue, $d_0$ and $d_1$ must be related by $->^(p r)$, suppose $d_0 ->^(p r) d_1$. If these two dequeues are not adjacent, we can create a smaller cycle by removing the operations between $d_0$ and $d_1$ in the old cycle. This means there are at most two dequeues in the cycle, and these two dequeues must be adjacent.
+
   If there is no dequeue in the cycle, the cycle consists of only enqueues. Note that two enqueues can only be related via rule 1 or rule 3.
   - If rule 1 was applied, or $m_i ->^(p r) m_(i+1)$, by property 7, $m_i ->^(v a l) d_i$ and $m_(i+1) ->^(v a l) d_(i+1)$ and $d_i ->^(p r) d_(i+1)$.
   - If rule 3 was applied, then by the assumption, $m_i ->^(v a l) d_i$ and $m_(i+1) ->^(v a l) d_(i+1)$ and $d_i ->^(p r) d_(i+1)$.
   Therefore, $d_i ->^(p r) d_(i+1)$. This means $d_0 ->^(p r) d_1 ->^(p r) dots ->^(p r) d_k ->^(p r) d_0$, which is a contradiction.
 
-  If there is one dequeue in the cycle. Without loss of generality, suppose $m_0$ is a dequeue. Then, $m_0 prec m_1$ because rule 1 or rule 4 was applied and $m_k prec m_0$ because rule 1, rule 2 or rule 5 was applied.
+  If there is one dequeue in the cycle, without loss of generality, suppose $m_0$ is a dequeue. Then, $m_0 prec m_1$ because rule 1 or rule 4 was applied and $m_k prec m_0$ because rule 1, rule 2 or rule 5 was applied.
+  - If rule 1 was applied to obtain $m_0 prec m_1$ and rule 1 was applied to obtain $m_k prec m_0$, because $->^(p r)$ is a partial order, that means $m_k ->^(p r) m_1$ or $m_k prec m_1$, which results in a shorter cycle, a contradiction.
+  - If rule 1 was applied to obtain $m_0 prec m_1$ and rule 2 was applied to obtain $m_k prec m_0$, that means $m_0 ->^(p r) m_1$ and $m_k ->^(v a l) m_0$. Suppose $m_1 ->^(v a l) d$, then $d arrow.not^(p r) m_1$, by property 4. Furthermore $m_0 ->^(p r) m_1$, $m_0$ is also a dequeue, then we must have $m_0 ->^(p r) d$. Because $m_k ->^(v a l) m_0$, $m_1 ->^(v a l) d$ and $m_0 ->^(p r) d$, then by rule 3, $m_k prec m_1$, which results in a shorter cycle, a contradiction.
+  - If rule 1 was applied to obtain $m_0 prec m_1$ and rule 5 was applied to obtain $m_k prec m_0$, $m_k$ must be a failed enqueue and $m_0 ->^(p r) m_1$. Because the cycle length is at least 3, $m_(k-1)$ must be an enqueue. Then the only way for $m_(k-1)$ to be related to a failed enqueue like $m_k$ is via rule 1, or $m_(k-1) ->^(p r) m_k$. By rule 5, $m_k$ must overlap $m_0$. Because $m_0 ->^(p r) m_1$ we have $m_(k-1) ->^(p r) m_1$, which results in a shorter cycle, a contradiction.
+  - If rule 4 was applied to obtain $m_0 prec m_1$ and rule 1 was applied to obtain $m_k prec m_0$, that means $m_0$ is a failed dequeue and $m_k ->^(p r) m_0$.
+  - If rule 4 was applied to obtain $m_0 prec m_1$ and rule 2 was applied to obtain $m_k prec m_0$, that means $m_0$ is a failed dequeue (rule 4) but also matches an enqueue at the same time (rule 2), which yields a contradiction according to property 3.
+  - If rule 4 was applied to obtain $m_0 prec m_1$ and rule 5 was applied to obtain $m_k prec m_0$.
 
   (\*\*)
 ]