wsc saturation

src/consistency/algo.rs

@@ -69,12 +69,19 @@ impl AtomicHistoryPO {
         wr
     }
 
-    pub fn vis_includes(&mut self, g: &DiGraph<TransactionId>) {
-        self.vis.union_with(g);
+    pub fn vis_includes(&mut self, g: &DiGraph<TransactionId>) -> bool {
+        self.vis.union_with(g)
     }
 
-    pub fn vis_is_trans(&mut self) {
-        self.vis = self.vis.take_closure();
+    pub fn vis_is_trans(&mut self) -> bool {
+        let closure = self.vis.take_closure();
+        let change = self
+            .vis
+            .adj_map
+            .iter()
+            .any(|(k, v)| closure.adj_map.get(k).unwrap().difference(v).count() > 0);
+        self.vis = closure;
+        change
     }
 
     pub fn causal_ww(&mut self) -> HashMap<Variable, DiGraph<TransactionId>> {
@@ -97,6 +104,28 @@ impl AtomicHistoryPO {
 
         ww
     }
+
+    pub fn causal_rw(&mut self) -> HashMap<Variable, DiGraph<TransactionId>> {
+        let mut rw: HashMap<Variable, DiGraph<TransactionId>> = Default::default();
+
+        for (&x, wr_x) in self.wr_rel.iter() {
+            let mut rw_x: DiGraph<TransactionId> = Default::default();
+            for (t1, t3s) in wr_x.adj_map.iter() {
+                for (t2, _) in wr_x.adj_map.iter() {
+                    if t1 != t2 {
+                        for t3 in t3s.iter() {
+                            if self.vis.has_edge(t3, t2) || self.vis.has_edge(t1, t2) {
+                                rw_x.add_edge(*t3, *t2);
+                            }
+                        }
+                    }
+                }
+            }
+            rw.insert(x, rw_x);
+        }
+
+        rw
+    }
 }
 
 #[derive(Debug)]

src/consistency/util.rs

@@ -84,13 +84,15 @@ where
         }
     }
 
-    pub fn union_with(&mut self, g: &Self) {
+    pub fn union_with(&mut self, g: &Self) -> bool {
+        let mut change = false;
         for (&u, vs) in g.adj_map.iter() {
             let entry = self.adj_map.entry(u).or_insert_with(Default::default);
             for &v in vs.iter() {
-                entry.insert(v);
+                change = entry.insert(v);
             }
         }
+        change
     }
 }
 

src/verifier/mod.rs

@@ -477,12 +477,26 @@ impl Verifier {
 
                     let wr = pre_hist.history.get_wr();
                     pre_hist.history.vis_includes(&wr);
-                    pre_hist.history.vis_is_trans();
-                    let ww = pre_hist.history.causal_ww();
-                    for (_, ww_x) in ww.iter() {
-                        pre_hist.history.vis_includes(ww_x);
+                    let mut change = false;
+                    // wsc code
+                    println!("wsc start");
+                    loop {
+                        change |= pre_hist.history.vis_is_trans();
+                        if !change {
+                            break;
+                        } else {
+                            change = false;
+                        }
+                        let ww = pre_hist.history.causal_ww();
+                        for (_, ww_x) in ww.iter() {
+                            change |= pre_hist.history.vis_includes(ww_x);
+                        }
+                        let rw = pre_hist.history.causal_rw();
+                        for (_, rw_x) in rw.iter() {
+                            change |= pre_hist.history.vis_includes(rw_x);
+                        }
                     }
-                    pre_hist.history.vis_is_trans();
+                    println!("wsc end");
 
                     if pre_hist.history.vis.has_cycle() {
                         Some(self.consistency_model)