linearization utils

src/consistency/sat.rs

@@ -281,7 +281,7 @@ impl Sat {
         self.add_clauses(&clauses);
     }
 
-    pub fn solve(&self, path: &PathBuf) -> bool {
+    pub fn solve(&self, path: &PathBuf) -> Option<Vec<(usize, usize)>> {
         let inp_cnf = path.join("history.cnf");
         let out_cnf = path.join("result.cnf");
         self.cnf.write_to_file(&inp_cnf);
@@ -341,15 +341,40 @@ impl Sat {
 
             edges.sort_unstable();
 
+            // building co
+            let mut parents: HashMap<(usize, usize), HashSet<(usize, usize)>> = Default::default();
             for e in &edges {
                 if e.0 == Edge::CO {
-                    println!("{:?}", e);
+                    parents
+                        .entry(e.2)
+                        .or_insert_with(Default::default)
+                        .insert(e.1);
+
+                    parents.entry(e.1).or_insert_with(Default::default);
+                }
+            }
+
+            let mut lin = Vec::new();
+
+            while !parents.is_empty() {
+                let next_t: Vec<_> = parents
+                    .iter()
+                    .filter_map(|(t1, t2s)| if t2s.is_empty() { Some(*t1) } else { None })
+                    .collect();
+                assert_eq!(next_t.len(), 1);
+
+                parents.retain(|_, t2s| !t2s.is_empty());
+
+                for (_, t2s) in parents.iter_mut() {
+                    t2s.remove(&next_t[0]);
                 }
+
+                lin.push(next_t[0]);
             }
 
-            true
+            Some(lin)
         } else {
-            false
+            None
         }
     }
 

src/verifier/mod.rs

@@ -415,7 +415,7 @@ impl Verifier {
                 _ => unreachable!(),
             }
 
-            sat_solver.solve(&self.dir)
+            sat_solver.solve(&self.dir).is_some()
         } else {
             info!(self.log, "using our algorithms");
 
@@ -475,7 +475,32 @@ impl Verifier {
                     if ser_hist.history.vis.has_cycle() {
                         false
                     } else {
-                        ser_hist.get_linearization().is_some()
+                        let lin_o = ser_hist.get_linearization();
+                        {
+                            // checking correctness
+                            if let Some(ref lin) = lin_o {
+                                let mut curr_value_map: HashMap<usize, (usize, usize)> =
+                                    Default::default();
+                                for txn_id in lin.iter() {
+                                    let (read_info, write_info) =
+                                        transaction_infos.get(txn_id).unwrap();
+                                    for (x, txn1) in read_info.iter() {
+                                        match curr_value_map.get(&x) {
+                                            Some(txn1_) => assert_eq!(txn1_, txn1),
+                                            _ => unreachable!(),
+                                        }
+                                    }
+                                    for &x in write_info.iter() {
+                                        curr_value_map.insert(x, *txn_id);
+                                    }
+                                    // if !write_info.is_empty() {
+                                    //     println!("{:?}", txn_id);
+                                    //     println!("{:?}", curr_value_map);
+                                    // }
+                                }
+                            }
+                        }
+                        lin_o.is_some()
                     }
                 }
                 _ => unreachable!(),