support for skipped transactions in session

src/consistency/algo.rs

@@ -18,32 +18,16 @@ pub struct AtomicHistoryPO {
 }
 
 impl AtomicHistoryPO {
-    pub fn new(
-        n_sizes: &[usize],
-        txns_info: HashMap<TransactionId, TransactionInfo>,
-    ) -> AtomicHistoryPO {
+    pub fn new(txns_info: HashMap<TransactionId, TransactionInfo>) -> AtomicHistoryPO {
         let root = (0, 0);
         let mut so: DiGraph<TransactionId> = Default::default();
-        {
-            let v: Vec<_> = n_sizes
-                .iter()
-                .enumerate()
-                .filter_map(|(node_i, &node_len)| {
-                    if node_len > 0 {
-                        Some((node_i + 1, 0))
-                    } else {
-                        None
-                    }
-                })
-                .collect();
-            so.add_edges(root, &v);
-        }
 
         {
-            for (node_i, &node_len) in n_sizes.iter().enumerate() {
-                for transaction_i in 1..node_len {
-                    so.add_edge((node_i + 1, transaction_i - 1), (node_i + 1, transaction_i));
-                }
+            let mut transactions: Vec<_> = txns_info.keys().cloned().collect();
+            transactions.sort_unstable();
+
+            for ts in transactions.windows(2) {
+                so.add_edge(if ts[0].0 == ts[1].0 { ts[0] } else { (0, 0) }, ts[1])
             }
         }
 
@@ -123,13 +107,9 @@ pub struct PrefixConsistentHistory {
 }
 
 impl PrefixConsistentHistory {
-    pub fn new(
-        n_sizes: &[usize],
-        txns_info: HashMap<TransactionId, TransactionInfo>,
-        log: Logger,
-    ) -> Self {
+    pub fn new(txns_info: HashMap<TransactionId, TransactionInfo>, log: Logger) -> Self {
         Self {
-            history: AtomicHistoryPO::new(n_sizes, txns_info),
+            history: AtomicHistoryPO::new(txns_info),
             active_write: Default::default(),
             log,
         }
@@ -233,13 +213,9 @@ pub struct SnapshotIsolationHistory {
 }
 
 impl SnapshotIsolationHistory {
-    pub fn new(
-        n_sizes: &[usize],
-        txns_info: HashMap<TransactionId, TransactionInfo>,
-        log: Logger,
-    ) -> Self {
+    pub fn new(txns_info: HashMap<TransactionId, TransactionInfo>, log: Logger) -> Self {
         Self {
-            history: AtomicHistoryPO::new(n_sizes, txns_info),
+            history: AtomicHistoryPO::new(txns_info),
             active_write: Default::default(),
             active_variable: Default::default(),
             log,
@@ -368,13 +344,9 @@ pub struct SerializableHistory {
 }
 
 impl SerializableHistory {
-    pub fn new(
-        n_sizes: &[usize],
-        txns_info: HashMap<TransactionId, TransactionInfo>,
-        log: Logger,
-    ) -> Self {
+    pub fn new(txns_info: HashMap<TransactionId, TransactionInfo>, log: Logger) -> Self {
         Self {
-            history: AtomicHistoryPO::new(n_sizes, txns_info),
+            history: AtomicHistoryPO::new(txns_info),
             active_write: Default::default(),
             log,
         }

src/consistency/sat.rs

@@ -73,13 +73,11 @@ pub struct Sat {
     cnf: CNF,
     edge_variable: HashMap<(Edge, (usize, usize), (usize, usize)), usize>,
     write_variable: HashMap<usize, HashMap<(usize, usize), HashSet<(usize, usize)>>>,
-    n_sizes: Vec<usize>,
     transactions: Vec<(usize, usize)>,
 }
 
 impl Sat {
     pub fn new(
-        n_sizes: &[usize],
         txns_info: &HashMap<(usize, usize), (HashMap<usize, (usize, usize)>, HashSet<usize>)>,
     ) -> Self {
         let mut write_variable: HashMap<usize, HashMap<(usize, usize), HashSet<(usize, usize)>>> =
@@ -101,36 +99,27 @@ impl Sat {
             wr_map.entry((0, 0)).or_insert_with(Default::default);
         }
 
-        let mut transactions = vec![(0, 0)];
-
-        for (i_node, &n_transaction) in n_sizes.iter().enumerate() {
-            for i_transaction in 0..n_transaction {
-                transactions.push((i_node + 1, i_transaction));
-            }
-        }
+        let mut transactions: Vec<_> = txns_info.keys().cloned().collect();
+        transactions.sort_unstable();
 
         Sat {
             cnf: Default::default(),
             edge_variable: HashMap::new(),
             write_variable,
-            n_sizes: n_sizes.to_owned(),
             transactions,
         }
     }
 
     pub fn session(&mut self) {
         let mut clauses = Vec::new();
-        for (i_node, &n_transaction) in self.n_sizes.iter().enumerate() {
-            for i_transaction in 1..n_transaction {
-                // session orders
-                clauses.push(vec![(
-                    Edge::VI,
-                    (i_node + 1, i_transaction - 1),
-                    (i_node + 1, i_transaction),
-                    true,
-                )])
-            }
-            clauses.push(vec![(Edge::VI, (0, 0), (i_node + 1, 0), true)]);
+
+        for id in self.transactions.windows(2) {
+            clauses.push(vec![(
+                Edge::VI,
+                if id[0].0 == id[1].0 { id[0] } else { (0, 0) },
+                id[1],
+                true,
+            )])
         }
 
         self.add_clauses(&clauses);

src/verifier/mod.rs

@@ -232,7 +232,6 @@ impl Verifier {
         info!(self.log, "each read from latest write");
         info!(self.log, "atomic reads");
 
-        let n_sizes: Vec<_> = histories.iter().map(|ref v| v.len()).collect();
         let mut transaction_infos = HashMap::new();
 
         let mut root_write_info = HashSet::new();
@@ -329,22 +328,11 @@ impl Verifier {
             biconnected_components.iter().all(|component| {
                 info!(self.log, "doing for component {:?}", component);
                 let restrict_infos = self.restrict(&transaction_infos, component);
-                let restrict_n_sizes: Vec<_> = n_sizes
-                    .iter()
-                    .enumerate()
-                    .map(|(i, &size)| {
-                        if component.contains(&(i + 1)) {
-                            size
-                        } else {
-                            0
-                        }
-                    })
-                    .collect();
 
-                self.do_hard_verification(&restrict_infos, &restrict_n_sizes)
+                self.do_hard_verification(&restrict_infos)
             })
         } else {
-            self.do_hard_verification(&transaction_infos, &n_sizes)
+            self.do_hard_verification(&transaction_infos)
         };
 
         let duration = moment.elapsed();
@@ -388,10 +376,9 @@ impl Verifier {
             (usize, usize),
             (HashMap<usize, (usize, usize)>, HashSet<usize>),
         >,
-        n_sizes: &[usize],
     ) -> bool {
         if self.use_sat {
-            let mut sat_solver = Sat::new(n_sizes, &transaction_infos);
+            let mut sat_solver = Sat::new(&transaction_infos);
 
             sat_solver.pre_vis_co();
             sat_solver.session();
@@ -421,7 +408,7 @@ impl Verifier {
 
             match self.consistency_model {
                 Consistency::Causal => {
-                    let mut causal_hist = AtomicHistoryPO::new(&n_sizes, transaction_infos.clone());
+                    let mut causal_hist = AtomicHistoryPO::new(transaction_infos.clone());
 
                     let wr = causal_hist.get_wr();
                     causal_hist.vis_includes(&wr);
@@ -436,7 +423,6 @@ impl Verifier {
                 }
                 Consistency::SnapshotIsolation => {
                     let mut si_hist = SnapshotIsolationHistory::new(
-                        &n_sizes,
                         transaction_infos.clone(),
                         self.log.clone(),
                     );
@@ -458,7 +444,6 @@ impl Verifier {
                 }
                 Consistency::Serializable => {
                     let mut ser_hist = SerializableHistory::new(
-                        &n_sizes,
                         transaction_infos.clone(),
                         self.log.clone(),
                     );