Skip to content

Commit

Permalink
improved upon partial order reduction via restricting choice of linea…
Browse files Browse the repository at this point in the history 
…rization to univocal actions
  • Loading branch information
@erwanM974
erwanM974 committed Feb 18, 2024
1 parent df1b8f7 commit 194d961
Show file tree
Hide file tree
Showing 3 changed files with 285 additions and 162 deletions.
219 changes: 57 additions & 162 deletions src/process/ana/handling/matches.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ use crate::core::execution::trace::trace::TraceAction;
use crate::core::language::eliminate_lf::eliminable::LifelineEliminable;
use crate::core::language::syntax::interaction::Interaction;
use crate::process::ana::context::AnalysisContext;
use crate::process::ana::handling::partial_order_reduction::{get_domination_domain, get_domination_maps, get_head_actions_ids_maps, is_action_univocal_in_analysis};
use crate::process::ana::node::flags::{MultiTraceAnalysisFlags, TraceAnalysisFlags};
use crate::process::ana::param::anakind::{AnalysisKind, SimulationActionCriterion, SimulationLoopCriterion};
use crate::process::ana::param::param::AnalysisParameterization;
Expand Down Expand Up @@ -222,189 +223,83 @@ impl AnalysisParameterization {
head_actions.push((canal_id,trace_head,is_last_on_canal));
}
}

// ***
if use_partial_order_reduction {
let mut head_action_id_to_frt_elts : HashMap<usize,HashSet<FrontierElement>> = hashmap!{};
let mut head_action_id_to_follow_ups : HashMap<usize,HashSet<Interaction>> = hashmap!{};

// iter immediately executable multi-actions
for frt_elt in global_frontier(&interaction) {
// iter head actions to look for a match
'iter_head : for (x,(coloc_id,head,is_last)) in head_actions.iter().enumerate() {
// if there is a match keeps track of frt_elt and the follow_up interaction
if frt_elt.target_actions == **head {
let exe_result = execute_interaction(interaction,
&frt_elt.position,
&frt_elt.target_lf_ids,
false);
let follow_up = if algo_uses_lifeline_removal_steps && *is_last {
let lfs_to_remove = context.co_localizations.get_coloc_lfs_ids(*coloc_id);
exe_result.interaction.eliminate_lifelines(lfs_to_remove)
} else {
exe_result.interaction
};
head_action_id_to_follow_ups.entry(x)
.or_insert_with(HashSet::new)
.insert(follow_up);
head_action_id_to_frt_elts.entry(x)
.or_insert_with(HashSet::new)
.insert(frt_elt);
break 'iter_head;
}
}
}

// for every combination/pair A1,A2 of head action that have matches
// determines whether or not A1 dominates A2 i.e.,
// all follow ups that can be obtained by executing first A2 and then A1
// can also be reached via executing first A1 and then A2
let mut dominated_by : HashMap<usize,HashSet<usize>> = hashmap!{};
// we use ".sorted()" so that the iter is deterministic
for pair in head_action_id_to_follow_ups.keys().sorted().combinations(2) {
let left = **pair.get(0).unwrap();
let (left_coloc_id,left_actions,left_is_last) = head_actions.get(left).unwrap();
let right = **pair.get(1).unwrap();
let (right_coloc_id,right_actions,right_is_last) = head_actions.get(right).unwrap();
let mut left_then_right = hashset!{};
for left_follow_up in head_action_id_to_follow_ups.get(&left).unwrap() {
for after_left in global_frontier(left_follow_up) {
if after_left.target_actions == **right_actions {
let exe_result = execute_interaction(left_follow_up,
&after_left.position,
&after_left.target_lf_ids,
false);
let follow_up = if algo_uses_lifeline_removal_steps && *right_is_last {
let lfs_to_remove = context.co_localizations.get_coloc_lfs_ids(*right_coloc_id);
exe_result.interaction.eliminate_lifelines(lfs_to_remove)
} else {
exe_result.interaction
};
left_then_right.insert(follow_up);
}
}
}
let mut right_then_left = hashset!{};
for right_follow_up in head_action_id_to_follow_ups.get(&right).unwrap() {
for after_right in global_frontier(right_follow_up) {
if after_right.target_actions == **left_actions {
let exe_result = execute_interaction(right_follow_up,
&after_right.position,
&after_right.target_lf_ids,
false);
let follow_up = if algo_uses_lifeline_removal_steps && *left_is_last {
let lfs_to_remove = context.co_localizations.get_coloc_lfs_ids(*left_coloc_id);
exe_result.interaction.eliminate_lifelines(lfs_to_remove)
} else {
exe_result.interaction
};
right_then_left.insert(follow_up);
}
}
}
//
if left_then_right.is_subset(&right_then_left) {
dominated_by.entry(left)
.and_modify(|dom_by| { dom_by.insert(right); })
.or_insert(hashset![right]);
}
if right_then_left.is_subset(&left_then_right) {
dominated_by.entry(right)
.and_modify(|dom_by| { dom_by.insert(left); })
.or_insert(hashset![left]);
}
}


/** BELOW WAS AN ATTEMPT WITH ITERATIVE ELIMINATIONS BUT IT MAKES FALSE NEGATIVES IN THE ANALYSIS **/
/*
// we use a VEC so that iteration is deterministic
let mut remaining_heads : Vec<usize> = head_action_id_to_follow_ups.keys().copied().sorted().collect();
//println!("there are {:} heads, starting removing..", remaining_heads.len());
// remove Condorcet losers from the remaining heads as long as there are Condorcet losers
'outer_loop : loop {
if remaining_heads.len() == 1 {
// of course, we should not remove the last remaining head,
// even if it is dominated
break 'outer_loop;
}
let mut loser = None;
'iter_heads : for (x,head_id) in remaining_heads.iter().enumerate() {
if let Some(head_id_is_dominated_by) = dominated_by.get(head_id) {
//println!("head {:} is dominated by: {:?}",head_id, head_id_is_dominated_by);
let the_remaining_others : HashSet<usize> = remaining_heads
.iter()
.copied()
.filter(|x| *x != *head_id)
.collect();
//println!("the other remaining heads are : {:?}",the_remaining_others);
if the_remaining_others.is_subset(head_id_is_dominated_by) {
//println!("this includes all the {:} other remaining heads",the_remaining_others.len());
loser = Some(x);
break 'iter_heads;
}
}
}
if let Some(loser_index) = loser {
// a Condorcet loser has been found and must be removed
remaining_heads.remove(loser_index);
} else {
// no Condorcet loser remains
break 'outer_loop;
let mut univocal_head_actions = vec![];
for (head_act_id,(coloc_id,head,_)) in head_actions.iter().enumerate() {
if is_action_univocal_in_analysis(context,interaction,*coloc_id,head) {
univocal_head_actions.push(head_act_id);
}
}
// if there is at least one univocal head action
// it may be possible to perform Partial Order Reduction
if !univocal_head_actions.is_empty() {
// computes the frontier and follow_ups for all the head actions
let (mut head_action_id_to_frt_elts,head_action_id_to_follow_ups) = get_head_actions_ids_maps(
algo_uses_lifeline_removal_steps,context,interaction,&head_actions
);

*/

let all_heads : Vec<usize> = head_action_id_to_follow_ups.keys().copied().sorted().collect();
let mut non_loser_heads : Vec<usize> = vec![];
for head_id in all_heads.iter() {
if let Some(head_id_is_dominated_by) = dominated_by.get(head_id) {
// if there is a univocal head action that dominates all the other head actions
// then it may be kept to make a unique successor
// thus implemented partial order reduction
let all_heads : Vec<usize> = head_action_id_to_follow_ups.keys().copied().sorted().collect();
for head_id in univocal_head_actions {
// computes the domination domains for each univocal head action
let domination_domain = get_domination_domain(
algo_uses_lifeline_removal_steps,
context,
&head_actions,
&head_action_id_to_follow_ups,
head_id
);
let the_others : HashSet<usize> = all_heads
.iter()
.copied()
.filter(|x| *x != *head_id)
.filter(|x| *x != head_id)
.collect();
let is_loser = the_others.is_subset(head_id_is_dominated_by);
if !is_loser {
non_loser_heads.push(*head_id);
if the_others.is_subset(&domination_domain) {
// a univocal dominant head action has been found
let frt_elts = head_action_id_to_frt_elts.remove(&head_id).unwrap();
let mut next_steps = vec![];
for frt_elt in frt_elts {
let canal_ids_of_targets = context.co_localizations.get_coloc_ids_from_lf_ids(
&frt_elt.target_lf_ids
);
let kind = AnalysisStepKind::Execute(frt_elt,
canal_ids_of_targets,
hashmap!{});
// ***
next_steps.push( kind );
}
return next_steps;
}
}

}

// gathers final next_steps
let mut next_steps = vec![];
for head_id in non_loser_heads {
let frt_elts = head_action_id_to_frt_elts.remove(&head_id).unwrap();
for frt_elt in frt_elts {
let canal_ids_of_targets = context.co_localizations.get_coloc_ids_from_lf_ids(&frt_elt.target_lf_ids);

}

// DEFAULT BEHAVIOR TO REVERT TO
let mut next_steps = vec![];
// iter immediately executable multi-actions
for frt_elt in global_frontier(&interaction) {
// iter head actions to look for a match
'iter_head : for (_,head,_) in head_actions.iter() {
if frt_elt.target_actions == **head {
let canal_ids_of_targets = context.co_localizations
.get_coloc_ids_from_lf_ids(&frt_elt.target_lf_ids);
let kind = AnalysisStepKind::Execute(frt_elt,
canal_ids_of_targets,
hashmap!{});
// ***
next_steps.push( kind );
break 'iter_head;
}
}
return next_steps;
} else {
let mut next_steps = vec![];
// iter immediately executable multi-actions
for frt_elt in global_frontier(&interaction) {
// iter head actions to look for a match
'iter_head : for (_,head,_) in head_actions.iter() {
if frt_elt.target_actions == **head {
let canal_ids_of_targets = context.co_localizations
.get_coloc_ids_from_lf_ids(&frt_elt.target_lf_ids);
let kind = AnalysisStepKind::Execute(frt_elt,
canal_ids_of_targets,
hashmap!{});
// ***
next_steps.push( kind );
break 'iter_head;
}
}
}
return next_steps;
}
return next_steps;

}

Expand Down
1 change: 1 addition & 0 deletions src/process/ana/handling/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,3 +17,4 @@ limitations under the License.
pub mod handler;
pub mod local_analysis;
mod matches;
mod partial_order_reduction;
Loading

0 comments on commit 194d961

Please sign in to comment.