Single-thread generate state graph

Author: zhangkw

src/callback.rs

@@ -166,7 +166,7 @@ impl PTACallbacks {
                 terminal_states,
             );
             for (api_name, initial_mark) in pn.api_marks.iter() {
-                state_graph.generate_states_with_api(api_name.clone(), initial_mark.clone());
+                // TODO: API可达图重构
             }
 
             // log::info!("deadlock state: {}", state_graph.detect_api_deadlock());

src/detect/atomicity_violation.rs

@@ -6,9 +6,10 @@ use crate::report::{AtomicOperation, AtomicReport, AtomicViolation, ViolationPat
 use petgraph::graph::NodeIndex;
 use petgraph::visit::EdgeRef;
 use petgraph::{Direction, Graph};
+use std::cell::RefCell;
 use std::collections::{HashMap, HashSet};
-use std::sync::{Arc, Mutex, RwLock};
-use std::thread;
+use std::rc::Rc;
+use std::sync::{Arc, RwLock};
 use std::time::Instant;
 
 pub struct AtomicityViolationDetector<'a> {
@@ -37,10 +38,10 @@ impl<'a> AtomicityViolationDetector<'a> {
 
         // 2. 将图结构包装在 Arc<RwLock> 中
         let graph = Arc::new(RwLock::new(self.state_graph.graph.clone()));
-        let initial_net = Arc::new(RwLock::new(self.state_graph.initial_net.as_ref().clone()));
 
         // 3. 并行检查违背
-        let violations = self.check_violations(loads, stores, &graph, &initial_net);
+        let violations =
+            self.check_violations(loads, stores, &graph, self.state_graph.initial_net.clone());
 
         if !violations.is_empty() {
             report.has_violation = true;
@@ -84,8 +85,10 @@ impl<'a> AtomicityViolationDetector<'a> {
         let mut loads = HashMap::new();
         let mut stores = HashMap::new();
 
-        for node_idx in self.state_graph.initial_net.node_indices() {
-            if let Some(PetriNetNode::T(t)) = self.state_graph.initial_net.node_weight(node_idx) {
+        for node_idx in self.state_graph.initial_net.borrow().node_indices() {
+            if let Some(PetriNetNode::T(t)) =
+                self.state_graph.initial_net.borrow().node_weight(node_idx)
+            {
                 match &t.transition_type {
                     ControlType::Call(CallType::AtomicLoad(var_id, ordering, span, thread_id)) => {
                         if format!("{:?}", ordering) == "Relaxed" {
@@ -123,50 +126,33 @@ impl<'a> AtomicityViolationDetector<'a> {
         loads: HashMap<NodeIndex, AtomicOp>,
         stores: HashMap<NodeIndex, AtomicOp>,
         graph: &Arc<RwLock<Graph<StateNode, StateEdge>>>,
-        initial_net: &Arc<RwLock<Graph<PetriNetNode, PetriNetEdge>>>,
+        initial_net: Rc<RefCell<Graph<PetriNetNode, PetriNetEdge>>>,
     ) -> Vec<ViolationPattern> {
-        let all_violations = Arc::new(Mutex::new(Vec::new()));
-        let mut handles = vec![];
+        let mut all_violations = Vec::new();
+        let graph = graph.read().unwrap();
+        let initial_net = initial_net.borrow();
 
         for (load_trans, load_op) in loads {
-            let all_violations = Arc::clone(&all_violations);
-            let stores = stores.clone();
-            let graph = Arc::clone(graph);
-            let initial_net = Arc::clone(initial_net);
-            unsafe {
-                let handle = thread::spawn(move || {
-                    let graph = graph.read().unwrap();
-                    for state in graph.node_indices() {
-                        for edge in graph.edges_directed(state, Direction::Outgoing) {
-                            if edge.weight().transition == load_trans {
-                                if let Some(violation) = Self::check_state_for_violation(
-                                    &graph,
-                                    &initial_net.read().unwrap(),
-                                    state,
-                                    &load_op,
-                                    &stores,
-                                ) {
-                                    all_violations.lock().unwrap().push(violation);
-                                }
-                            }
+            for state in graph.node_indices() {
+                for edge in graph.edges_directed(state, Direction::Outgoing) {
+                    if edge.weight().transition == load_trans {
+                        if let Some(violation) = Self::check_state_for_violation(
+                            &graph,
+                            &initial_net,
+                            state,
+                            &load_op,
+                            &stores,
+                        ) {
+                            all_violations.push(violation);
                         }
                     }
-                });
-                handles.push(handle);
+                }
             }
         }
 
-        for handle in handles {
-            handle.join().unwrap();
-        }
-
-        let violations = Arc::try_unwrap(all_violations)
-            .unwrap()
-            .into_inner()
-            .unwrap();
         let mut pattern_map: HashMap<ViolationPattern, Vec<Vec<(usize, u8)>>> = HashMap::new();
 
-        for violation in violations {
+        for violation in all_violations {
             let pattern = ViolationPattern {
                 load_op: AtomicOperation {
                     operation_type: "load".to_string(),

src/detect/datarace.rs

@@ -26,7 +26,12 @@ impl<'a> DataRaceDetector<'a> {
             // 收集当前状态的所有不安全操作
             for edge in self.state_graph.graph.edges(state) {
                 let transition = edge.weight().transition;
-                if let Some(node) = self.state_graph.initial_net.node_weight(transition) {
+                if let Some(node) = self
+                    .state_graph
+                    .initial_net
+                    .borrow()
+                    .node_weight(transition)
+                {
                     match node {
                         PetriNetNode::T(t) => match &t.transition_type {
                             ControlType::UnsafeRead(alias_id, span, basic_block, place_ty) => {

src/detect/deadlock.rs

@@ -66,8 +66,11 @@ impl<'a> DeadlockDetector<'a> {
 
             // 检查是否是正常终止状态
             let is_normal_termination = state.mark.iter().any(|(idx, _)| {
-                if let Some(PetriNetNode::P(place)) =
-                    self.state_graph.initial_net.node_weight(node_index(*idx))
+                if let Some(PetriNetNode::P(place)) = self
+                    .state_graph
+                    .initial_net
+                    .borrow()
+                    .node_weight(node_index(*idx))
                 {
                     place.name.contains("main_end")
                 } else {
@@ -255,8 +258,11 @@ impl<'a> DeadlockDetector<'a> {
         let has_terminal_state = cycle.iter().any(|&node| {
             if let Some(state) = self.state_graph.graph.node_weight(node) {
                 state.mark.iter().any(|(idx, _)| {
-                    if let Some(PetriNetNode::P(place)) =
-                        self.state_graph.initial_net.node_weight(node_index(*idx))
+                    if let Some(PetriNetNode::P(place)) = self
+                        .state_graph
+                        .initial_net
+                        .borrow()
+                        .node_weight(node_index(*idx))
                     {
                         place.name.contains("main_end")
                     } else {
@@ -335,8 +341,8 @@ impl<'a> DeadlockDetector<'a> {
     fn collect_lock_transitions(&self) -> HashMap<NodeIndex, Vec<NodeIndex>> {
         let mut lock_transitions = HashMap::new();
 
-        for node in self.state_graph.initial_net.node_indices() {
-            if let PetriNetNode::T(transition) = &self.state_graph.initial_net[node] {
+        for node in self.state_graph.initial_net.borrow().node_indices() {
+            if let PetriNetNode::T(transition) = &self.state_graph.initial_net.borrow()[node] {
                 match &transition.transition_type {
                     ControlType::Call(CallType::Lock(lock_place))
                     | ControlType::Call(CallType::RwLockWrite(lock_place))
@@ -360,10 +366,14 @@ impl<'a> DeadlockDetector<'a> {
             for edge in self
                 .state_graph
                 .initial_net
+                .borrow()
                 .edges_directed(transition, petgraph::Direction::Incoming)
             {
-                if let Some(PetriNetNode::P(_)) =
-                    self.state_graph.initial_net.node_weight(edge.source())
+                if let Some(PetriNetNode::P(_)) = self
+                    .state_graph
+                    .initial_net
+                    .borrow()
+                    .node_weight(edge.source())
                 {
                     let required_tokens = edge.weight().label;
                     let available_tokens = state_node
@@ -387,8 +397,11 @@ impl<'a> DeadlockDetector<'a> {
         let marking: Vec<(String, u8)> = mark
             .iter()
             .filter_map(|(idx, tokens)| {
-                if let Some(PetriNetNode::P(place)) =
-                    self.state_graph.initial_net.node_weight(node_index(*idx))
+                if let Some(PetriNetNode::P(place)) = self
+                    .state_graph
+                    .initial_net
+                    .borrow()
+                    .node_weight(node_index(*idx))
                 {
                     Some((format!("{} ({})", place.name, place.span), *tokens))
                 } else {

src/extern_tools/lola.rs

@@ -47,7 +47,7 @@ impl LolaAnalyzer {
             if let PetriNetNode::P(place) = &petri_net.net[index] {
                 let normalized_name = normalize_name(&place.name);
                 places.push(normalized_name.clone());
-                let tokens = place.tokens.read().unwrap();
+                let tokens = place.tokens.borrow();
                 if *tokens > 0 {
                     markings.push(format!("{}: {}", normalized_name, *tokens));
                 }

src/extern_tools/tina.rs

@@ -69,7 +69,7 @@ impl TinaAnalyzer {
 
         for index in petri_net.net.node_indices() {
             if let PetriNetNode::P(place) = &petri_net.net[index] {
-                let tokens = place.tokens.read().unwrap();
+                let tokens = place.tokens.borrow();
                 let mut pl_str =
                     format!("pl {} ({})", normalize_name_for_tina(&place.name), tokens);
 

src/graph/mod.rs

@@ -3,4 +3,3 @@ pub mod mir_pn;
 pub mod net_structure;
 pub mod pn;
 pub mod state_graph;
-pub mod unfolding_net;

src/graph/net_structure.rs

@@ -3,10 +3,12 @@ use crate::memory::pointsto::AliasId;
 
 use super::callgraph::InstanceId;
 use petgraph::graph::NodeIndex;
+use petgraph::Graph;
 use regex::Regex;
+use std::cell::RefCell;
 use std::collections::HashMap;
 use std::hash::Hash;
-use std::sync::{Arc, RwLock};
+use std::rc::Rc;
 use thiserror::Error;
 
 #[derive(Debug, Clone)]
@@ -18,13 +20,14 @@ pub enum Shape {
 #[derive(Debug, Clone)]
 pub struct Place {
     pub name: String,
-    // pub tokens: RefCell<usize>,
-    pub tokens: Arc<RwLock<u8>>,
+    pub tokens: Rc<RefCell<u8>>,
     pub capacity: u8,
     pub span: String,
     pub place_type: PlaceType,
 }
 
+type PetriNetGraph = Graph<PetriNetNode, PetriNetEdge>;
+
 #[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord)]
 pub enum PlaceType {
     Unsafe,
@@ -41,7 +44,7 @@ impl Place {
     pub fn new(name: String, token: u8, place_type: PlaceType) -> Self {
         Self {
             name,
-            tokens: Arc::new(RwLock::new(token)),
+            tokens: Rc::new(RefCell::new(token)),
             capacity: token,
             span: String::new(),
             place_type,
@@ -51,7 +54,7 @@ impl Place {
     pub fn new_with_span(name: String, token: u8, place_type: PlaceType, span: String) -> Self {
         Self {
             name,
-            tokens: Arc::new(RwLock::new(token)),
+            tokens: Rc::new(RefCell::new(token)),
             capacity: 1u8,
             span,
             place_type,
@@ -61,7 +64,7 @@ impl Place {
     pub fn new_with_no_token(name: String, place_type: PlaceType) -> Self {
         Self {
             name,
-            tokens: Arc::new(RwLock::new(0)),
+            tokens: Rc::new(RefCell::new(0)),
             capacity: 1u8,
             span: String::new(),
             place_type,
@@ -78,7 +81,7 @@ impl Place {
     ) -> Self {
         Self {
             name,
-            tokens: Arc::new(RwLock::new(token)),
+            tokens: Rc::new(RefCell::new(token)),
             capacity,
             span,
             place_type,

src/graph/pn.rs

@@ -470,7 +470,6 @@ impl<'compilation, 'pn, 'tcx> PetriNet<'compilation, 'pn, 'tcx> {
             let func_instance = self.callgraph.graph.node_weight(node_idx).unwrap();
             let func_id = func_instance.instance().def_id();
             let func_name = format_name(func_id);
-            log::info!("func_name: {}", func_name);
             if !func_name.starts_with(&self.options.crate_name)
                 || self.function_counter.contains_key(&func_id)
                 || func_name.contains("::deserialize")
@@ -886,8 +885,8 @@ impl<'compilation, 'pn, 'tcx> PetriNet<'compilation, 'pn, 'tcx> {
         for node in self.net.node_indices() {
             match &self.net[node] {
                 PetriNetNode::P(place) => {
-                    if *place.tokens.read().unwrap() > 0 {
-                        current_mark.insert((node.clone(), *place.tokens.read().unwrap() as u8));
+                    if *place.tokens.borrow() > 0 {
+                        current_mark.insert((node.clone(), *place.tokens.borrow() as u8));
                     }
                 }
                 PetriNetNode::T(_) => {
@@ -923,7 +922,7 @@ impl<'compilation, 'pn, 'tcx> PetriNet<'compilation, 'pn, 'tcx> {
                 &|_, nr| {
                     let label = match &nr.1 {
                         PetriNetNode::P(place) => {
-                            let tokens = *place.tokens.read().unwrap();
+                            let tokens = *place.tokens.borrow();
                             format!(
                                 "label = \"{}\\n(tokens: {})\", shape = circle",
                                 place.name, tokens
@@ -1060,7 +1059,7 @@ impl<'compilation, 'pn, 'tcx> PetriNet<'compilation, 'pn, 'tcx> {
                         continue;
                     }
                     _ => {
-                        terminal_states.push((node_idx.index(), *place.tokens.read().unwrap()));
+                        terminal_states.push((node_idx.index(), *place.tokens.borrow()));
                     }
                 }
             }