graph -> lin notes

theories/examples/exchanger/proof_graph_lin.v

@@ -31,6 +31,10 @@ Notation exchanger_event_map := (exchanger_event_map event_id).
 Notation exchanger_event_set := (gset event_id).
 Notation exchanger_event_order := (event_order event_id).
 
+(* TODO
+Use mo. Linearization works because there's no (o1, o2) ∈ order if (o1, o2) ∈ com.
+*)
+
 Definition ExchangerHandle (v : val) (γ : gname) (N : namespace) (f : Qp)
     (events : exchanger_event_map)
     (owned : exchanger_event_set)

theories/examples/queue/proof_graph_lin.v

@@ -85,6 +85,7 @@ Graph property
 Ordering
 - Order deqs by linearizing hb. Add definitions/lemmas for this.
   - d1 -hb> d2 ⇒ d1 < d2
+  - sort pairs by dequeue's mo
 - Order enqs by deq order
   - d1 < d2 ∧ e1 -com> d1 ∧ e2 -com> d2 ⇒ e1 < e2
   - CHECK: e1 -hb> e2 ⇒ e1 < e2
@@ -93,13 +94,12 @@ Ordering
   - CHECK: e1 < e2 → ¬ (e2 -hb> e1)
     - e2 -hb> e1 → ¬ (d1 -hb> d2) → ??
     +            → d2 -hb> d1 → d2 < d1 → e2 < e1
-- Unmatched enqueues: linearize hb
+- Unmatched enqueues: use mo (includes hb)
 - ✗ Interleaving: starting from e_1,
   + ¬(dj -hb> ei) ⇒ insert ei in front of dj,
   + otherwise ⇒ insert dj
   * XXX counterexample of di -hb> ej ⇒ di < ej: d2 -hb> e3, e1 < e2 < e3 < d1 < d2
-- ✓ Additional constraint for enqueue insertion:
-  e should not be inserted before d if ∃ d', d ≤ d', d' -hb> e
+- Fixed: e should not be inserted before d if ∃ d', d ≤ d', d' -hb> e
 Invariant
 1. (o1, o2) ∈ orders → o1 -hb> o2
   - maintain logview in handle
@@ -154,15 +154,109 @@ Proof
       - EmpDeq: "Any umatched enqs do not happen before EmpDeq"
         should be strengthened to
         e -hb> x → ∃ d, (e, d) ∈ com ∧ ¬(x -hb> b)
+      - strengthen empdeq rule: e = Enq → x = EmpDeq → e -hb> x → ∃ d, (e, d) ∈ com ∧ d -hb> x.
+        then d2 -hb> d1, contradicts ..
+      e1───────►d1◄─────x
+                    /--/▲
+                   /    │
+                  /     │
+      e2───────►d2      │
+      │                 │
+      │                 │
+      └─────────────────┘
 - orders_consistent: good
 - queue_history: good
 
 
 Implementation
 - show existence of (eids : list event_id) follows the ordering rule
-- prove that such orderins also satisfy linearization, orders_consistent, queue_history
+- prove that such orderings also satisfy linearization, orders_consistent, queue_history
 - don't do it with function...
 - use hahn?
+
+
+1. Focus on strong queue only, use mo
+Proof
+- linearization: from FIFO_a
+- orders_consistent: same
+- queue_history:
+  + ... †
+  + add deq: show ∃ e, (e, d) ∈ com, enqs = deqs ++ (e :: queue')
+    - ... †
+    - among the unmatched enqueues, e should be the mo-minimal
+      - method 1: Suppose e isn't mo-minimal and let e' be the mo-minimal one
+        Then e' < e < d. NOTE FIFO_c can't rule this out..
+      - method 2: If all events are known, we know that d is the mo-minimal,
+        so e is also mo-minimal ...? No.
+        This still doesn't rule out the case where a globally unmatched enqueue
+        is the mo-minimal in the current unmatched enques.
+      - Is mo_consec, len(hs) = len(enqs) + len(deqs) + len(empdeqs) useful? No.
+  + ... †
+
+
+2.
+- strengthen FIFO_b = FIFO_b + FIFO_c:
+  (e2, d2) ∈ com → e1 ≤ e2 → ∃ d1, d1 ≤ d2 ∧ (e1, d1) ∈ G.(com)
+- queue_history:
+  - ... †
+  + add empdeq: enqs = deqs ++ []
+    - ✗ there is no unmatched enqueues in the prefix
+      - NOTE: non_empty only talks about hb, and it can't be fixed
+    - Q: Can empdeqs be pushed to the past (to the point when the queue is empty)?
+      + ∃ unmatched e
+        + e -hb> x: contradicts non_empty
+        + otherwise: push to the past, somewhere before e
+          + can't push due ∃ (e', d') ∈ com
+            + e < e' < d' -hb> x: contradicts FIFO_b
+            + e' < e < d' -hb> x: NOTE can't rule out
+            + e' < e < d' < x, e' -hb> x:
+      + otherwise: insert here
+    - NOTE: can't use mo, counterexample: (e1, d1) ∈ com, e1 -hb> x, e1 < e2 < d1 < x
+
+3.
+- queue_history:
+  - proof method
+    1. keep `queue_history hs queue` in invariant (only possible for mo-linearizable)
+    2. all at once in info with IH `queue_history (take i hs) queue`
+  - Lemma queue_current : queue_history hs queue → enqs = deqs ++ queue
+    - (e1, d1), ... (en, dn) matched, unmatched en+1 ..
+  + add enq: easy
+  + add deq: show ∃ e, (e, d) ∈ com, enqs = deqs ++ (e :: queue')
+    - d has a matching enq e
+      - NOTE: can't derived from consistency, need the op spec
+    - e is in the prefix
+      - by e -hb> d, or by dequeue spec
+    - among the unmatched enqueues, e should be the mo-minimal
+      - Suppose ∃ unmatched e', e' < e < d.
+        By FIFO_b, ∃ d', d' ≤ d ∧ (e', d') ∈ com. This contradicts unmatched e'.
+    - ...?
+  + add empdeq: enqs = deqs ++ [] ...
++ Order deqs and empdeqs first with mo and insert enqs (ordered by mo) using hb and semantics.
+  - Q: In `e1 -hb> x, e1 < e2 < d1 < x`, how do decide whether to insert e2?
+- NOTE: Expressing "unmatched in the current prefix"? Filter mo-before events?
+  unmatched_enq_mono is weak.
++ Fix the mo-order by pushing enqs to the future, only through deqs/empdeqs
+  - invariant
+    - the prefix is queue_history
+    - what about the suffix?
+  - the enq being pushed is unmatched
+  - Q: unable to push back (blocked by hb) and not queue_history
+    + d blocks e
+      + (e, d) ∈ com:
+      + otherwise:
+    + x blocks e: e is unmatched in the prefix
++ Fix the mo-order by pushing deq/empdeq to the past, only through enqs
+
+4.
+- Strengthen non_empty:
+  ∀ e, e -hb> x → ∃ d, (e, d) ∈ G.(com) ∧ d -hb> x
++ order deqs/empdeqs by mo and insert enqs ordered by mo using hb and semantics
+  - counterexample: e1 < e2 < d1 < x, e2 -hb> d1 ⇒ x e1 e2 d; need to reorder d/x
++ order enqs/deqs by mo and insert empdeqs ordered by mo using hb and semantics
+  - counterexample: e1 < e2 < d1 < x, d1 -hb> x ⇒ e1 d1 x e2; need to reorder e/d
+- e should not be inserted before d/x if ∃ d', d ≤ d', d' -hb> e
+
+
 *)
 Inductive queue_graph_sim G E events orders : Prop :=
   | queue_graph_sim_intro