summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
499a538)
Not very useful because state comparison does not work with SMPI
privatisation yet.
snapshot->privatization_regions =
xbt_new(mc_mem_region_t, SIMIX_process_count());
for (i = 0; i < SIMIX_process_count(); i++) {
snapshot->privatization_regions =
xbt_new(mc_mem_region_t, SIMIX_process_count());
for (i = 0; i < SIMIX_process_count(); i++) {
- // TODO, add support for sparse snapshot
+ mc_mem_region_t ref_reg =
+ mc_model_checker->parent_snapshot ? mc_model_checker->parent_snapshot->privatization_regions[i] : NULL;
snapshot->privatization_regions[i] =
snapshot->privatization_regions[i] =
- MC_region_new(-1, mappings[i], size_data_exe, NULL);
+ MC_region_new(-1, mappings[i], size_data_exe, ref_reg);
}
snapshot->privatization_index = loaded_page;
}
}
snapshot->privatization_index = loaded_page;
}
mc_mem_region_t r2, mc_snapshot_t snapshot1,
mc_snapshot_t snapshot2)
{
mc_mem_region_t r2, mc_snapshot_t snapshot1,
mc_snapshot_t snapshot2)
{
+ xbt_assert(r1 && r2,
+ "Missing region. Did you enable SMPI privatisation? It is not compatible with state comparison.");
struct mc_compare_state state;
xbt_dynar_t variables;
struct mc_compare_state state;
xbt_dynar_t variables;