From: Gabriel Corona Date: Thu, 12 Feb 2015 15:03:51 +0000 (+0100) Subject: Merge master into mc-process X-Git-Tag: v3_12~732^2~119 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/ffe8ce65fd9a8e18a0469f26f067c3ea6d5d60d4?hp=-c Merge master into mc-process --- ffe8ce65fd9a8e18a0469f26f067c3ea6d5d60d4 diff --combined examples/msg/mc/bugged1_liveness.tesh index b2e56421bc,5f72c22e51..dc3c3a7be1 --- a/examples/msg/mc/bugged1_liveness.tesh +++ b/examples/msg/mc/bugged1_liveness.tesh @@@ -2,8 -2,11 +2,8 @@@ ! expect signal SIGABRT ! timeout 20 -$ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 -> [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 > [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness -> [ 0.000000] (0:@) Get debug information ... -> [ 0.000000] (0:@) Get debug information done ! > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (3:client@Fafard) Ask the request > [ 0.000000] (2:client@Boivin) Propositions changed : r=1, cs=0 @@@ -12,7 -15,7 +12,7 @@@ > [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle > [ 0.000000] (3:client@Fafard) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly - > [ 0.000000] (0:@) Pair 21 already reached (equal to pair 9) ! + > [ 0.000000] (0:@) Pair 22 already reached (equal to pair 10) ! > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* > [ 0.000000] (0:@) | ACCEPTANCE CYCLE | > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* @@@ -37,7 -40,8 +37,8 @@@ > [ 0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) > [ 0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only)) > [ 0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) - > [ 0.000000] (0:@) Expanded pairs = 21 - > [ 0.000000] (0:@) Visited pairs = 21 + > [ 0.000000] (0:@) Expanded pairs = 22 + > [ 0.000000] (0:@) Visited pairs = 20 > [ 0.000000] (0:@) Executed transitions = 20 - > [ 0.000000] (0:@) Counter-example depth : 20 + > [ 0.000000] (0:@) Counter-example depth : 21 + diff --combined examples/msg/mc/bugged1_liveness_sparse.tesh index cc378b1a6b,bc934d924e..1ad6da3b2e --- a/examples/msg/mc/bugged1_liveness_sparse.tesh +++ b/examples/msg/mc/bugged1_liveness_sparse.tesh @@@ -2,8 -2,12 +2,8 @@@ ! expect signal SIGABRT ! timeout 60 -$ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes -> [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' -> [ 0.000000] (0:@) Configuration change: Set 'model-check/sparse-checkpoint' to 'yes' +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes > [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness -> [ 0.000000] (0:@) Get debug information ... -> [ 0.000000] (0:@) Get debug information done ! > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (3:client@Fafard) Ask the request > [ 0.000000] (2:client@Boivin) Propositions changed : r=1, cs=0 @@@ -12,7 -16,7 +12,7 @@@ > [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle > [ 0.000000] (3:client@Fafard) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly - > [ 0.000000] (0:@) Pair 21 already reached (equal to pair 9) ! + > [ 0.000000] (0:@) Pair 22 already reached (equal to pair 10) ! > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* > [ 0.000000] (0:@) | ACCEPTANCE CYCLE | > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* @@@ -37,7 -41,7 +37,7 @@@ > [ 0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) > [ 0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only)) > [ 0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) - > [ 0.000000] (0:@) Expanded pairs = 21 - > [ 0.000000] (0:@) Visited pairs = 21 + > [ 0.000000] (0:@) Expanded pairs = 22 + > [ 0.000000] (0:@) Visited pairs = 20 > [ 0.000000] (0:@) Executed transitions = 20 - > [ 0.000000] (0:@) Counter-example depth : 20 + > [ 0.000000] (0:@) Counter-example depth : 21 diff --combined examples/msg/mc/bugged1_liveness_visited.tesh index bf01872a9a,d05858a39f..859e793af3 --- a/examples/msg/mc/bugged1_liveness_visited.tesh +++ b/examples/msg/mc/bugged1_liveness_visited.tesh @@@ -2,8 -2,12 +2,8 @@@ ! expect signal SIGABRT ! timeout 90 -$ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 -> [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' -> [ 0.000000] (0:@) Configuration change: Set 'model-check/visited' to '100' +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 > [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness -> [ 0.000000] (0:@) Get debug information ... -> [ 0.000000] (0:@) Get debug information done ! > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (3:client@Fafard) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly @@@ -69,7 -73,7 +69,7 @@@ > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly > [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it - > [ 0.000000] (0:@) Pair 57 already reached (equal to pair 45) ! + > [ 0.000000] (0:@) Pair 58 already reached (equal to pair 46) ! > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* > [ 0.000000] (0:@) | ACCEPTANCE CYCLE | > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* @@@ -124,7 -128,8 +124,8 @@@ > [ 0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) > [ 0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) > [ 0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) - > [ 0.000000] (0:@) Expanded pairs = 57 - > [ 0.000000] (0:@) Visited pairs = 208 + > [ 0.000000] (0:@) Expanded pairs = 58 + > [ 0.000000] (0:@) Visited pairs = 201 > [ 0.000000] (0:@) Executed transitions = 207 - > [ 0.000000] (0:@) Counter-example depth : 50 + > [ 0.000000] (0:@) Counter-example depth : 51 + diff --combined examples/msg/mc/bugged1_liveness_visited_sparse.tesh index 95eea17ad1,9e987ea3cd..1750e8b638 --- a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh +++ b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh @@@ -2,8 -2,13 +2,8 @@@ ! expect signal SIGABRT ! timeout 90 -$ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes -> [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' -> [ 0.000000] (0:@) Configuration change: Set 'model-check/visited' to '100' -> [ 0.000000] (0:@) Configuration change: Set 'model-check/sparse-checkpoint' to 'yes' +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes > [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness -> [ 0.000000] (0:@) Get debug information ... -> [ 0.000000] (0:@) Get debug information done ! > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (3:client@Fafard) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly @@@ -69,7 -74,7 +69,7 @@@ > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly > [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it - > [ 0.000000] (0:@) Pair 57 already reached (equal to pair 45) ! + > [ 0.000000] (0:@) Pair 58 already reached (equal to pair 46) ! > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* > [ 0.000000] (0:@) | ACCEPTANCE CYCLE | > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* @@@ -124,7 -129,7 +124,7 @@@ > [ 0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) > [ 0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) > [ 0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) - > [ 0.000000] (0:@) Expanded pairs = 57 - > [ 0.000000] (0:@) Visited pairs = 208 + > [ 0.000000] (0:@) Expanded pairs = 58 + > [ 0.000000] (0:@) Visited pairs = 201 > [ 0.000000] (0:@) Executed transitions = 207 - > [ 0.000000] (0:@) Counter-example depth : 50 + > [ 0.000000] (0:@) Counter-example depth : 51 diff --combined src/mc/mc_checkpoint.c index b7dd845b1d,38f64893db..1fdf717986 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@@ -5,6 -5,7 +5,6 @@@ * under the terms of the license (GNU LGPL) which comes with this package. */ #define _GNU_SOURCE -#define UNW_LOCAL_ONLY #include @@@ -24,6 -25,7 +24,6 @@@ #include "../simix/smx_private.h" -#define UNW_LOCAL_ONLY #include #include @@@ -33,12 -35,12 +33,12 @@@ #include "mc_snapshot.h" #include "mc_object_info.h" #include "mc_mmu.h" +#include "mc_unw.h" +#include "mc_protocol.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc, "Logging specific to mc_checkpoint"); -char *libsimgrid_path; - /************************************ Free functions **************************************/ /*****************************************************************************************/ @@@ -47,16 -49,13 +47,16 @@@ static void MC_snapshot_stack_free(mc_s if (s) { xbt_dynar_free(&(s->local_variables)); xbt_dynar_free(&(s->stack_frames)); + mc_unw_destroy_context(s->context); + xbt_free(s->context); xbt_free(s); } } static void MC_snapshot_stack_free_voidp(void *s) { - MC_snapshot_stack_free((mc_snapshot_stack_t) * (void **) s); + mc_snapshot_stack_t stack = (mc_snapshot_stack_t) * (void **) s; + MC_snapshot_stack_free(stack); } static void local_variable_free(local_variable_t v) @@@ -70,66 -69,59 +70,66 @@@ static void local_variable_free_voidp(v local_variable_free((local_variable_t) * (void **) v); } -void MC_region_destroy(mc_mem_region_t reg) +void MC_region_destroy(mc_mem_region_t region) { - if (!reg) + if (!region) return; - - //munmap(reg->data, reg->size); - xbt_free(reg->data); - if (reg->page_numbers) { - mc_free_page_snapshot_region(reg->page_numbers, mc_page_count(reg->size)); + switch(region->storage_type) { + case MC_REGION_STORAGE_TYPE_NONE: + break; + case MC_REGION_STORAGE_TYPE_FLAT: + xbt_free(region->flat.data); + break; + case MC_REGION_STORAGE_TYPE_CHUNKED: + mc_free_page_snapshot_region(region->chunked.page_numbers, mc_page_count(region->size)); + xbt_free(region->chunked.page_numbers); + break; + case MC_REGION_STORAGE_TYPE_PRIVATIZED: + { + size_t regions_count = region->privatized.regions_count; + for (size_t i=0; i!=regions_count; ++i) { + MC_region_destroy(region->privatized.regions[i]); + } + free(region->privatized.regions); + break; + } } - xbt_free(reg); + xbt_free(region); } void MC_free_snapshot(mc_snapshot_t snapshot) { - unsigned int i; - for (i = 0; i < NB_REGIONS; i++) { - MC_region_destroy(snapshot->regions[i]); + for (size_t i = 0; i < snapshot->snapshot_regions_count; i++) { + MC_region_destroy(snapshot->snapshot_regions[i]); } - + xbt_free(snapshot->snapshot_regions); xbt_free(snapshot->stack_sizes); xbt_dynar_free(&(snapshot->stacks)); xbt_dynar_free(&(snapshot->to_ignore)); xbt_dynar_free(&snapshot->ignored_data); - - if (snapshot->privatization_regions) { - size_t n = xbt_dynar_length(snapshot->enabled_processes); - for (i = 0; i != n; ++i) { - MC_region_destroy(snapshot->privatization_regions[i]); - } - xbt_free(snapshot->privatization_regions); - } - xbt_free(snapshot); } /******************************* Snapshot regions ********************************/ /*********************************************************************************/ -static mc_mem_region_t mc_region_new_dense(int type, void *start_addr, void* permanent_addr, size_t size, mc_mem_region_t ref_reg) +static mc_mem_region_t mc_region_new_dense( + mc_region_type_t region_type, + void *start_addr, void* permanent_addr, size_t size, mc_mem_region_t ref_reg) { - mc_mem_region_t new_reg = xbt_new(s_mc_mem_region_t, 1); - new_reg->start_addr = start_addr; - new_reg->permanent_addr = permanent_addr; - new_reg->data = NULL; - new_reg->size = size; - new_reg->page_numbers = NULL; - new_reg->data = xbt_malloc(size); - memcpy(new_reg->data, permanent_addr, size); + mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1); + region->region_type = region_type; + region->storage_type = MC_REGION_STORAGE_TYPE_FLAT; + region->start_addr = start_addr; + region->permanent_addr = permanent_addr; + region->size = size; + region->flat.data = xbt_malloc(size); + MC_process_read(&mc_model_checker->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE, + region->flat.data, permanent_addr, size, + MC_PROCESS_INDEX_DISABLED); XBT_DEBUG("New region : type : %d, data : %p (real addr %p), size : %zu", - type, new_reg->data, permanent_addr, size); - return new_reg; - + region_type, region->flat.data, permanent_addr, size); + return region; } /** @brief Take a snapshot of a given region @@@ -140,7 -132,7 +140,7 @@@ * @param size Size of the data* * @param ref_reg Reference corresponding region */ -static mc_mem_region_t MC_region_new(int type, void *start_addr, void* permanent_addr, size_t size, mc_mem_region_t ref_reg) +static mc_mem_region_t MC_region_new(mc_region_type_t type, void *start_addr, void* permanent_addr, size_t size, mc_mem_region_t ref_reg) { if (_sg_mc_sparse_checkpoint) { return mc_region_new_sparse(type, start_addr, permanent_addr, size, ref_reg); @@@ -159,139 -151,113 +159,139 @@@ * @param reg Target region * @param reg_reg Current region (if not NULL), used for lazy per page restoration */ -static void MC_region_restore(mc_mem_region_t reg, mc_mem_region_t ref_reg) +static void MC_region_restore(mc_mem_region_t region, mc_mem_region_t ref_region) { - /*FIXME: check if start_addr is still mapped, if it is not, then map it - before copying the data */ - if (!reg->page_numbers) { - memcpy(reg->permanent_addr, reg->data, reg->size); - } else { - mc_region_restore_sparse(reg, ref_reg); + switch(region->storage_type) { + case MC_REGION_STORAGE_TYPE_NONE: + default: + xbt_die("Storage type not supported"); + break; + + case MC_REGION_STORAGE_TYPE_FLAT: + MC_process_write(&mc_model_checker->process, region->flat.data, + region->permanent_addr, region->size); + break; + + case MC_REGION_STORAGE_TYPE_CHUNKED: + mc_region_restore_sparse(&mc_model_checker->process, region, ref_region); + break; + + case MC_REGION_STORAGE_TYPE_PRIVATIZED: + { + bool has_ref_regions = ref_region && + ref_region->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED; + size_t process_count = region->privatized.regions_count; + for (size_t i = 0; i < process_count; i++) { + MC_region_restore(region->privatized.regions[i], + has_ref_regions ? ref_region->privatized.regions[i] : NULL); + } + break; + } } - return; } -static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, - void *start_addr, void* permanent_addr, size_t size) +// FIXME, multiple privatisation regions +// FIXME, cross-process +static inline +void* MC_privatization_address(mc_process_t process, int process_index) +{ + xbt_assert(process_index >= 0); + return smpi_privatisation_regions[process_index].address; +} + +static mc_mem_region_t MC_region_new_privatized( + mc_region_type_t region_type, void *start_addr, void* permanent_addr, size_t size, + mc_mem_region_t ref_reg) +{ + size_t process_count = smpi_process_count(); + mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1); + region->region_type = region_type; + region->storage_type = MC_REGION_STORAGE_TYPE_PRIVATIZED; + region->start_addr = start_addr; + region->permanent_addr = permanent_addr; + region->size = size; + region->privatized.regions_count = process_count; + region->privatized.regions = xbt_new(mc_mem_region_t, process_count); + + for (size_t i = 0; i < process_count; i++) { + mc_mem_region_t ref_subreg = NULL; + if (ref_reg && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED) + ref_subreg = ref_reg->privatized.regions[i]; + region->privatized.regions[i] = + MC_region_new(region_type, start_addr, + MC_privatization_address(&mc_model_checker->process, i), size, + ref_subreg); + } + + return region; +} +static void MC_snapshot_add_region(int index, mc_snapshot_t snapshot, mc_region_type_t type, + mc_object_info_t object_info, + void *start_addr, void* permanent_addr, size_t size) { - mc_mem_region_t ref_reg = - mc_model_checker->parent_snapshot ? mc_model_checker->parent_snapshot->regions[type] : NULL; - mc_mem_region_t new_reg = MC_region_new(type, start_addr, permanent_addr, size, ref_reg); - snapshot->regions[type] = new_reg; + if (type == MC_REGION_TYPE_DATA) + xbt_assert(object_info, "Missing object info for object."); + else if (type == MC_REGION_TYPE_HEAP) + xbt_assert(!object_info, "Unexpected object info for heap region."); + + mc_mem_region_t ref_reg = NULL; + if (mc_model_checker->parent_snapshot) + ref_reg = mc_model_checker->parent_snapshot->snapshot_regions[index]; + + mc_mem_region_t region; + const bool privatization_aware = MC_object_info_is_privatized(object_info); + if (privatization_aware && smpi_process_count()) + region = MC_region_new_privatized(type, start_addr, permanent_addr, size, ref_reg); + else + region = MC_region_new(type, start_addr, permanent_addr, size, ref_reg); + + region->object_info = object_info; + snapshot->snapshot_regions[index] = region; return; } -static void MC_get_memory_regions(mc_snapshot_t snapshot) +static void MC_get_memory_regions(mc_process_t process, mc_snapshot_t snapshot) { + const size_t n = process->object_infos_size; + snapshot->snapshot_regions_count = n + 1; + snapshot->snapshot_regions = xbt_new0(mc_mem_region_t, n + 1); + + for (size_t i = 0; i!=n; ++i) { + mc_object_info_t object_info = process->object_infos[i]; + MC_snapshot_add_region(i, snapshot, MC_REGION_TYPE_DATA, object_info, + object_info->start_rw, object_info->start_rw, + object_info->end_rw - object_info->start_rw); + } - void *start_heap = std_heap->base; - void *end_heap = std_heap->breakval; - MC_snapshot_add_region(snapshot, 0, start_heap, start_heap, - (char *) end_heap - (char *) start_heap); - snapshot->heap_bytes_used = mmalloc_get_bytes_used(std_heap); - snapshot->privatization_regions = NULL; + xbt_mheap_t heap = MC_process_get_heap(process); + void *start_heap = heap->base; + void *end_heap = heap->breakval; - MC_snapshot_add_region(snapshot, 1, - mc_libsimgrid_info->start_rw, mc_libsimgrid_info->start_rw, - mc_libsimgrid_info->end_rw - mc_libsimgrid_info->start_rw); + MC_snapshot_add_region(n, snapshot, MC_REGION_TYPE_HEAP, NULL, + start_heap, start_heap, + (char *) end_heap - (char *) start_heap); + snapshot->heap_bytes_used = mmalloc_get_bytes_used_remote( + heap->heaplimit, + MC_process_get_malloc_info(process)); #ifdef HAVE_SMPI - size_t i; if (smpi_privatize_global_variables && smpi_process_count()) { - // Snapshot the global variable of the application separately for each - // simulated process: - snapshot->privatization_regions = - xbt_new(mc_mem_region_t, smpi_process_count()); - for (i = 0; i < smpi_process_count(); i++) { - mc_mem_region_t ref_reg = - mc_model_checker->parent_snapshot ? mc_model_checker->parent_snapshot->privatization_regions[i] : NULL; - snapshot->privatization_regions[i] = - MC_region_new(-1, mc_binary_info->start_rw, smpi_privatisation_regions[i].address, size_data_exe, ref_reg); - } + // FIXME, cross-process snapshot->privatization_index = smpi_loaded_page; - snapshot->regions[2] = NULL; } else #endif { - MC_snapshot_add_region(snapshot, 2, - mc_binary_info->start_rw, mc_binary_info->start_rw, - mc_binary_info->end_rw - mc_binary_info->start_rw); - snapshot->privatization_regions = NULL; - snapshot->privatization_index = -1; - } -} - -/** @brief Finds the range of the different memory segments and binary paths */ -void MC_init_memory_map_info() -{ - - unsigned int i = 0; - s_map_region_t reg; - memory_map_t maps = MC_get_memory_map(); - - maestro_stack_start = NULL; - maestro_stack_end = NULL; - libsimgrid_path = NULL; - - while (i < maps->mapsize) { - reg = maps->regions[i]; - if (maps->regions[i].pathname == NULL) { - // Nothing to do - } else if ((reg.prot & PROT_WRITE) - && !memcmp(maps->regions[i].pathname, "[stack]", 7)) { - maestro_stack_start = reg.start_addr; - maestro_stack_end = reg.end_addr; - } else if ((reg.prot & PROT_READ) && (reg.prot & PROT_EXEC) - && !memcmp(basename(maps->regions[i].pathname), "libsimgrid", - 10)) { - if (libsimgrid_path == NULL) - libsimgrid_path = strdup(maps->regions[i].pathname); - } - i++; + snapshot->privatization_index = MC_PROCESS_INDEX_MISSING; } - - xbt_assert(maestro_stack_start, "maestro_stack_start"); - xbt_assert(maestro_stack_end, "maestro_stack_end"); - xbt_assert(libsimgrid_path, "libsimgrid_path&"); - - MC_free_memory_map(maps); - } /** \brief Fills the position of the segments (executable, read-only, read/write). * - * TODO, use dl_iterate_phdr to be more robust + * `dl_iterate_phdr` would be more robust but would not work in cross-process. * */ void MC_find_object_address(memory_map_t maps, mc_object_info_t result) { - unsigned int i = 0; s_map_region_t reg; const char *name = basename(result->file_name); @@@ -328,18 -294,6 +328,18 @@@ i++; } + result->start = result->start_rw; + if ((const void*) result->start_ro > result->start) + result->start = result->start_ro; + if ((const void*) result->start_exec > result->start) + result->start = result->start_exec; + + result->end = result->end_rw; + if (result->end_ro && (const void*) result->end_ro < result->end) + result->end = result->end_ro; + if (result->end_exec && (const void*) result->end_exec > result->end) + result->end = result->end_exec; + xbt_assert(result->file_name); xbt_assert(result->start_rw); xbt_assert(result->start_exec); @@@ -370,8 -324,6 +370,8 @@@ static bool mc_valid_variable(dw_variab static void mc_fill_local_variables_values(mc_stack_frame_t stack_frame, dw_frame_t scope, int process_index, xbt_dynar_t result) { + mc_process_t process = &mc_model_checker->process; + void *ip = (void *) stack_frame->ip; if (ip < scope->low_pc || ip >= scope->high_pc) return; @@@ -384,8 -336,7 +384,8 @@@ continue; int region_type; - if ((long) stack_frame->ip > (long) mc_libsimgrid_info->start_exec) + // FIXME, get rid of `region_type` + if ((long) stack_frame->ip > (long) process->libsimgrid_info->start_exec) region_type = 1; else region_type = 2; @@@ -401,7 -352,6 +401,7 @@@ new_var->address = current_variable->address; } else if (current_variable->locations.size != 0) { s_mc_location_t location; + // FIXME, cross-process support mc_dwarf_resolve_locations(&location, ¤t_variable->locations, current_variable->object_info, &(stack_frame->unw_cursor), @@@ -455,16 -405,15 +455,16 @@@ static void MC_stack_frame_free_voipd(v } } -static xbt_dynar_t MC_unwind_stack_frames(void *stack_context) +static xbt_dynar_t MC_unwind_stack_frames(mc_unw_context_t stack_context) { + mc_process_t process = &mc_model_checker->process; xbt_dynar_t result = xbt_dynar_new(sizeof(mc_stack_frame_t), MC_stack_frame_free_voipd); unw_cursor_t c; // TODO, check condition check (unw_init_local==0 means end of frame) - if (unw_init_local(&c, (unw_context_t *) stack_context) != 0) { + if (mc_unw_init_cursor(&c, stack_context) != 0) { xbt_die("Could not initialize stack unwinding"); @@@ -486,7 -435,7 +486,7 @@@ // TODO, use real addresses in frame_t instead of fixing it here - dw_frame_t frame = MC_find_function_by_ip((void *) ip); + dw_frame_t frame = MC_process_find_function(process, (void *) ip); stack_frame->frame = frame; if (frame) { @@@ -503,11 -452,11 +503,11 @@@ && !strcmp(frame->name, "smx_ctx_sysv_wrapper")) break; - int ret = ret = unw_step(&c); + int ret = unw_step(&c); if (ret == 0) { xbt_die("Unexpected end of stack."); } else if (ret < 0) { - xbt_die("Error while unwinding stack."); + xbt_die("Error while unwinding stack"); } } @@@ -529,19 -478,9 +529,19 @@@ static xbt_dynar_t MC_take_snapshot_sta unsigned int cursor = 0; stack_region_t current_stack; + // FIXME, cross-process support (stack_areas) xbt_dynar_foreach(stacks_areas, cursor, current_stack) { mc_snapshot_stack_t st = xbt_new(s_mc_snapshot_stack_t, 1); - st->stack_frames = MC_unwind_stack_frames(current_stack->context); + + unw_context_t* original_context = (unw_context_t*) current_stack->context; + + st->context = xbt_new0(s_mc_unw_context_t, 1); + if (mc_unw_init_context(st->context, &mc_model_checker->process, + original_context) < 0) { + xbt_die("Could not initialise the libunwind context."); + } + + st->stack_frames = MC_unwind_stack_frames(st->context); st->local_variables = MC_get_local_variables_values(st->stack_frames, current_stack->process_index); st->process_index = current_stack->process_index; @@@ -558,7 -497,6 +558,7 @@@ } +// FIXME, cross-process support (mc_heap_comparison_ignore) static xbt_dynar_t MC_take_snapshot_ignore() { @@@ -593,28 -531,23 +593,28 @@@ static void mc_free_snapshot_ignored_da static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot) { + xbt_assert(snapshot->process); snapshot->ignored_data = xbt_dynar_new(sizeof(s_mc_snapshot_ignored_data_t), mc_free_snapshot_ignored_data_pvoid); // Copy the memory: unsigned int cursor = 0; mc_checkpoint_ignore_region_t region; - xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) { + // FIXME, cross-process support (mc_checkpoint_ignore) + xbt_dynar_foreach (mc_model_checker->process.checkpoint_ignore, cursor, region) { s_mc_snapshot_ignored_data_t ignored_data; ignored_data.start = region->addr; ignored_data.size = region->size; ignored_data.data = malloc(region->size); - memcpy(ignored_data.data, region->addr, region->size); + // TODO, we should do this once per privatization segment: + MC_process_read(snapshot->process, + MC_ADDRESS_SPACE_READ_FLAGS_NONE, + ignored_data.data, region->addr, region->size, MC_PROCESS_INDEX_DISABLED); xbt_dynar_push(snapshot->ignored_data, &ignored_data); } // Zero the memory: - xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) { - memset(region->addr, 0, region->size); + xbt_dynar_foreach (mc_model_checker->process.checkpoint_ignore, cursor, region) { + MC_process_clear_memory(snapshot->process, region->addr, region->size); } } @@@ -624,8 -557,7 +624,8 @@@ static void MC_snapshot_ignore_restore( unsigned int cursor = 0; s_mc_snapshot_ignored_data_t ignored_data; xbt_dynar_foreach (snapshot->ignored_data, cursor, ignored_data) { - memcpy(ignored_data.start, ignored_data.data, ignored_data.size); + MC_process_write(snapshot->process, + ignored_data.data, ignored_data.start, ignored_data.size); } } @@@ -648,18 -580,17 +648,18 @@@ int mc_important_snapshot(mc_snapshot_ return false; } -static void MC_get_current_fd(mc_snapshot_t snapshot){ +static void MC_get_current_fd(mc_snapshot_t snapshot) +{ snapshot->total_fd = 0; const size_t fd_dir_path_size = 20; char fd_dir_path[fd_dir_path_size]; if (snprintf(fd_dir_path, fd_dir_path_size, - "/proc/%lli/fd", (long long int) getpid()) > fd_dir_path_size) + "/proc/%lli/fd", (long long int) snapshot->process->pid) > fd_dir_path_size) xbt_die("Unexpected buffer is too small for fd_dir_path"); - DIR* fd_dir = opendir (fd_dir_path); + DIR* fd_dir = opendir(fd_dir_path); if (fd_dir == NULL) xbt_die("Cannot open directory '/proc/self/fd'\n"); @@@ -674,8 -605,7 +674,8 @@@ const size_t source_size = 25; char source[25]; - if (snprintf(source, source_size, "/proc/self/fd/%s", fd_number->d_name) > source_size) + if (snprintf(source, source_size, "/proc/%lli/fd/%s", + (long long int) snapshot->process->pid, fd_number->d_name) > source_size) xbt_die("Unexpected buffer is too small for fd %s", fd_number->d_name); const size_t link_size = 200; @@@ -702,6 -632,10 +702,10 @@@ if (strncmp(link, "pipe:", 5) == 0 || strncmp(link, "socket:", 7) == 0) continue; + // If dot_output enabled, do not handle the corresponding file + if (dot_output != NULL && strcmp(basename(link), _sg_mc_dot_output_file) == 0) + continue; + // This is probably a shared memory used by lttng-ust: if(strncmp("/dev/shm/ust-shm-tmp-", link, 21)==0) continue; @@@ -721,37 -655,25 +725,37 @@@ closedir (fd_dir); } +static s_mc_address_space_class_t mc_snapshot_class = { + .read = (void*) &MC_snapshot_read +}; + mc_snapshot_t MC_take_snapshot(int num_state) { - + mc_process_t mc_process = &mc_model_checker->process; mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1); + snapshot->process = mc_process; + snapshot->address_space.address_space_class = &mc_snapshot_class; + snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL); smx_process_t process; + // FIXME, cross-process support (simix_global->process_list) xbt_swag_foreach(process, simix_global->process_list) { xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid); } MC_snapshot_handle_ignore(snapshot); - MC_get_current_fd(snapshot); + if (_sg_mc_snapshot_fds) + MC_get_current_fd(snapshot); + + const bool use_soft_dirty = _sg_mc_sparse_checkpoint + && _sg_mc_soft_dirty + && MC_process_is_self(mc_process); /* Save the std heap and the writable mapped pages of libsimgrid and binary */ - MC_get_memory_regions(snapshot); - if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) { + MC_get_memory_regions(mc_process, snapshot); + if (use_soft_dirty) mc_softdirty_reset(); - } snapshot->to_ignore = MC_take_snapshot_ignore(); @@@ -768,25 -690,36 +772,25 @@@ } MC_snapshot_ignore_restore(snapshot); - if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) { + if (use_soft_dirty) mc_model_checker->parent_snapshot = snapshot; - } return snapshot; } -void MC_restore_snapshot(mc_snapshot_t snapshot) +static inline +void MC_restore_snapshot_regions(mc_snapshot_t snapshot) { mc_snapshot_t parent_snapshot = mc_model_checker->parent_snapshot; - int new_fd; - unsigned int i; - for (i = 0; i < NB_REGIONS; i++) { + const size_t n = snapshot->snapshot_regions_count; + for (size_t i = 0; i < n; i++) { // For privatized, variables we decided it was not necessary to take the snapshot: - if (snapshot->regions[i]) - MC_region_restore(snapshot->regions[i], - parent_snapshot ? parent_snapshot->regions[i] : NULL); + if (snapshot->snapshot_regions[i]) + MC_region_restore(snapshot->snapshot_regions[i], + parent_snapshot ? parent_snapshot->snapshot_regions[i] : NULL); } #ifdef HAVE_SMPI - if (snapshot->privatization_regions) { - // Restore the global variables of the application separately for each - // simulated process: - for (i = 0; i < smpi_process_count(); i++) { - if (snapshot->privatization_regions[i]) { - MC_region_restore(snapshot->privatization_regions[i], - parent_snapshot ? parent_snapshot->privatization_regions[i] : NULL); - } - } - } if(snapshot->privatization_index >= 0) { // We just rewrote the global variables. // The privatisation segment SMPI thinks @@@ -797,16 -730,7 +801,16 @@@ smpi_really_switch_data_segment(snapshot->privatization_index); } #endif +} + +static inline +void MC_restore_snapshot_fds(mc_snapshot_t snapshot) +{ + if (mc_mode == MC_MODE_SERVER) + xbt_die("FD snapshot not implemented in client/server mode."); + int new_fd; + size_t i; for(i=0; i < snapshot->total_fd; i++){ new_fd = open(snapshot->current_fd[i]->filename, snapshot->current_fd[i]->flags); @@@ -821,29 -745,24 +825,29 @@@ }; lseek(snapshot->current_fd[i]->number, snapshot->current_fd[i]->current_position, SEEK_SET); } +} - if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) { +void MC_restore_snapshot(mc_snapshot_t snapshot) +{ + const bool use_soft_dirty = _sg_mc_sparse_checkpoint + && _sg_mc_soft_dirty + && MC_process_is_self(&mc_model_checker->process); + + MC_restore_snapshot_regions(snapshot); + if (_sg_mc_snapshot_fds) + MC_restore_snapshot_fds(snapshot); + if (use_soft_dirty) { mc_softdirty_reset(); } - MC_snapshot_ignore_restore(snapshot); - if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) { + if (use_soft_dirty) { mc_model_checker->parent_snapshot = snapshot; } + mc_model_checker->process.cache_flags = 0; } mc_snapshot_t simcall_HANDLER_mc_snapshot(smx_simcall_t simcall) { return MC_take_snapshot(1); } - -void *MC_snapshot(void) -{ - return simcall_mc_snapshot(); -} diff --combined src/mc/mc_comm_determinism.c index fc4e1bd772,b68e563946..6576d606c2 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@@ -18,8 -18,6 +18,6 @@@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm xbt_dynar_t initial_communications_pattern; xbt_dynar_t incomplete_communications_pattern; - xbt_dynar_t communications_pattern; - int nb_comm_pattern; /********** Static functions ***********/ @@@ -31,120 -29,136 +29,136 @@@ static void comm_pattern_free(mc_comm_p p = NULL; } - static void comm_pattern_free_voidp(void *p) + static void list_comm_pattern_free(mc_list_comm_pattern_t l) { - comm_pattern_free((mc_comm_pattern_t) * (void **) p); - } - - static mc_comm_pattern_t get_comm_pattern_from_idx(xbt_dynar_t pattern, - unsigned int *idx, - e_smx_comm_type_t type, - unsigned long proc) - { - mc_comm_pattern_t current_comm; - while (*idx < xbt_dynar_length(pattern)) { - current_comm = - (mc_comm_pattern_t) xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t); - if (current_comm->type == type && type == SIMIX_COMM_SEND) { - if (current_comm->src_proc == proc) - return current_comm; - } else if (current_comm->type == type && type == SIMIX_COMM_RECEIVE) { - if (current_comm->dst_proc == proc) - return current_comm; - } - (*idx)++; - } - return NULL; + xbt_dynar_free(&(l->list)); + xbt_free(l); + l = NULL; } - static int compare_comm_pattern(mc_comm_pattern_t comm1, - mc_comm_pattern_t comm2) - { + static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) { + if(comm1->type != comm2->type) + return TYPE_DIFF; if (strcmp(comm1->rdv, comm2->rdv) != 0) - return 1; + return RDV_DIFF; if (comm1->src_proc != comm2->src_proc) - return 1; + return SRC_PROC_DIFF; if (comm1->dst_proc != comm2->dst_proc) - return 1; + return DST_PROC_DIFF; if (comm1->data_size != comm2->data_size) - return 1; - if (memcmp(comm1->data, comm2->data, comm1->data_size) != 0) - return 1; + return DATA_SIZE_DIFF; + if(comm1->data == NULL && comm2->data == NULL) + return 0; + /*if(comm1->data != NULL && comm2->data !=NULL) { + if (!memcmp(comm1->data, comm2->data, comm1->data_size)) + return 0; + return DATA_DIFF; + }else{ + return DATA_DIFF; + }*/ return 0; } - static void deterministic_pattern(xbt_dynar_t pattern, int partial) - { - - unsigned int cursor = 0, send_index = 0, recv_index = 0; - mc_comm_pattern_t comm1, comm2; - unsigned int current_process = 1; /* Process 0 corresponds to maestro */ - unsigned int nb_comms1, nb_comms2; - xbt_dynar_t process_comms_pattern1, process_comms_pattern2; - - while (current_process < simix_process_maxpid) { - process_comms_pattern1 = (xbt_dynar_t)xbt_dynar_get_as(initial_communications_pattern, current_process, xbt_dynar_t); - process_comms_pattern2 = (xbt_dynar_t)xbt_dynar_get_as(pattern, current_process, xbt_dynar_t); - nb_comms1 = xbt_dynar_length(process_comms_pattern1); - nb_comms2 = xbt_dynar_length(process_comms_pattern2); - if(!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))) - xbt_die("Damn ! Some communications from the process %u are incomplete (%lu)! That means one or several simcalls are not handle.", current_process, xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))); - if (!partial && (nb_comms1 != nb_comms2)) { - XBT_INFO("The total number of communications is different between the compared patterns for the process %u.\n Communication determinism verification for this process cannot be performed.", current_process); - initial_global_state->send_deterministic = -1; - initial_global_state->comm_deterministic = -1; - } else { - while (cursor < nb_comms2) { - comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(process_comms_pattern1, cursor, mc_comm_pattern_t); - if (comm1->type == SIMIX_COMM_SEND) { - comm2 = get_comm_pattern_from_idx(process_comms_pattern2, &send_index, comm1->type, current_process); - if (compare_comm_pattern(comm1, comm2)) { - XBT_INFO("The communications pattern of the process %u is different! (Different communication : %u)", current_process, cursor+1); - initial_global_state->send_deterministic = 0; - initial_global_state->comm_deterministic = 0; - return; - } - send_index++; - } else if (comm1->type == SIMIX_COMM_RECEIVE) { - comm2 = get_comm_pattern_from_idx(process_comms_pattern2, &recv_index, comm1->type, current_process); - if (compare_comm_pattern(comm1, comm2)) { - initial_global_state->comm_deterministic = 0; - if (!_sg_mc_send_determinism){ - XBT_INFO("The communications pattern of the process %u is different! (Different communication : %u)", current_process, cursor+1); - return; - } - } - recv_index++; - } - cursor++; - } + static void print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) { + if (_sg_mc_comms_determinism && !initial_global_state->comm_deterministic) { + XBT_INFO("****************************************************"); + XBT_INFO("***** Non-deterministic communications pattern *****"); + XBT_INFO("****************************************************"); + XBT_INFO("The communications pattern of the process %d is different!", process); + switch(diff) { + case TYPE_DIFF: + XBT_INFO("Different communication type for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + case RDV_DIFF: + XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + case SRC_PROC_DIFF: + XBT_INFO("Different communication source process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + case DST_PROC_DIFF: + XBT_INFO("Different communication destination process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + case DATA_SIZE_DIFF: + XBT_INFO("Different communication data size for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + case DATA_DIFF: + XBT_INFO("Different communication data for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + default: + break; } - current_process++; - cursor = 0; - send_index = 0; - recv_index = 0; + MC_print_statistics(mc_stats); + xbt_abort(); + } else if (_sg_mc_send_determinism && !initial_global_state->send_deterministic) { + XBT_INFO("*********************************************************"); + XBT_INFO("***** Non-send-deterministic communications pattern *****"); + XBT_INFO("*********************************************************"); + XBT_INFO("The communications pattern of the process %d is different!", process); + switch(diff) { + case TYPE_DIFF: + XBT_INFO("Different communication type for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + case RDV_DIFF: + XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + case SRC_PROC_DIFF: + XBT_INFO("Different communication source process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + case DST_PROC_DIFF: + XBT_INFO("Different communication destination process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + case DATA_SIZE_DIFF: + XBT_INFO("Different communication data size for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + case DATA_DIFF: + XBT_INFO("Different communication data for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); + break; + default: + break; + } + MC_print_statistics(mc_stats); + xbt_abort(); } } - static void print_communications_pattern(xbt_dynar_t comms_pattern) + static void print_communications_pattern() { - unsigned int cursor = 0; + unsigned int cursor = 0, cursor2 = 0; mc_comm_pattern_t current_comm; + mc_list_comm_pattern_t current_list; unsigned int current_process = 1; - xbt_dynar_t current_pattern; while (current_process < simix_process_maxpid) { - current_pattern = (xbt_dynar_t)xbt_dynar_get_as(comms_pattern, current_process, xbt_dynar_t); + current_list = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, current_process, mc_list_comm_pattern_t); XBT_INFO("Communications from the process %u:", current_process); - xbt_dynar_foreach(current_pattern, cursor, current_comm) { + while(cursor2 < current_list->index_comm){ + current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(current_list->list, cursor2, mc_comm_pattern_t); if (current_comm->type == SIMIX_COMM_SEND) { - XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc, + XBT_INFO("(%u) [(%lu) %s -> (%lu) %s] %s ", cursor,current_comm->src_proc, current_comm->src_host, current_comm->dst_proc, current_comm->dst_host, "iSend"); } else { - XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc, + XBT_INFO("(%u) [(%lu) %s <- (%lu) %s] %s ", cursor, current_comm->dst_proc, current_comm->dst_host, current_comm->src_proc, current_comm->src_host, "iRecv"); } + cursor2++; + } + current_process++; + cursor = 0; + cursor2 = 0; + } + } + + static void print_incomplete_communications_pattern(){ + unsigned int cursor = 0; + unsigned int current_process = 1; + xbt_dynar_t current_pattern; + mc_comm_pattern_t comm; + while (current_process < simix_process_maxpid) { + current_pattern = (xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t); + XBT_INFO("Incomplete communications from the process %u:", current_process); + xbt_dynar_foreach(current_pattern, cursor, comm) { + XBT_DEBUG("(%u) Communication %p", cursor, comm); } current_process++; cursor = 0; @@@ -153,146 -167,190 +167,189 @@@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm) { + mc_process_t process = &mc_model_checker->process; void *addr_pointed; comm_pattern->src_proc = comm->comm.src_proc->pid; comm_pattern->dst_proc = comm->comm.dst_proc->pid; - comm_pattern->src_host = - simcall_host_get_name(comm->comm.src_proc->smx_host); - comm_pattern->dst_host = - simcall_host_get_name(comm->comm.dst_proc->smx_host); - if (comm_pattern->data_size == -1) { + comm_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host); + comm_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host); + if (comm_pattern->data_size == -1 && comm->comm.src_buff != NULL) { comm_pattern->data_size = *(comm->comm.dst_buff_size); comm_pattern->data = xbt_malloc0(comm_pattern->data_size); addr_pointed = *(void **) comm->comm.src_buff; - if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval) + if (addr_pointed > (void*) process->heap_address + && addr_pointed < MC_process_get_heap(process)->breakval) memcpy(comm_pattern->data, addr_pointed, comm_pattern->data_size); else memcpy(comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size); } } + static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) { + + mc_list_comm_pattern_t list_comm_pattern = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t); + + if(!backtracking){ + mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, comm->index, mc_comm_pattern_t); + e_mc_comm_pattern_difference_t diff; + + if((diff = compare_comm_pattern(initial_comm, comm)) != NONE_DIFF){ + if (comm->type == SIMIX_COMM_SEND) + initial_global_state->send_deterministic = 0; + initial_global_state->comm_deterministic = 0; + print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1); + } + } + + list_comm_pattern->index_comm++; + comm_pattern_free(comm); + + } + /********** Non Static functions ***********/ - void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, mc_call_type call_type) + void comm_pattern_free_voidp(void *p) { + comm_pattern_free((mc_comm_pattern_t) * (void **) p); + } + + void list_comm_pattern_free_voidp(void *p) { + list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p); + } + + void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type) { - + mc_process_t process = &mc_model_checker->process; mc_comm_pattern_t pattern = NULL; pattern = xbt_new0(s_mc_comm_pattern_t, 1); - pattern->num = ++nb_comm_pattern; pattern->data_size = -1; + pattern->data = NULL; + + pattern->index = ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, request->issuer->pid, mc_list_comm_pattern_t))->index_comm + xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t)); + void *addr_pointed; - if (call_type == MC_CALL_TYPE_SEND) { // ISEND + + if (call_type == MC_CALL_TYPE_SEND) { + /* Create comm pattern */ pattern->type = SIMIX_COMM_SEND; pattern->comm = simcall_comm_isend__get__result(request); + pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name); pattern->src_proc = pattern->comm->comm.src_proc->pid; pattern->src_host = simcall_host_get_name(request->issuer->smx_host); - pattern->data_size = pattern->comm->comm.src_buff_size; - pattern->data = xbt_malloc0(pattern->data_size); - addr_pointed = *(void **) pattern->comm->comm.src_buff; - if (addr_pointed > (void*) process->heap_address - && addr_pointed < MC_process_get_heap(process)->breakval) - memcpy(pattern->data, addr_pointed, pattern->data_size); - else - memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); - } else if (call_type == MC_CALL_TYPE_RECV) { // IRECV + if(pattern->comm->comm.src_buff != NULL){ + pattern->data_size = pattern->comm->comm.src_buff_size; + pattern->data = xbt_malloc0(pattern->data_size); + addr_pointed = *(void **) pattern->comm->comm.src_buff; - if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval) ++ if (addr_pointed > (void*) process->heap_address ++ && addr_pointed < MC_process_get_heap(process)->breakval) + memcpy(pattern->data, addr_pointed, pattern->data_size); + else + memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); + } + } else if (call_type == MC_CALL_TYPE_RECV) { pattern->type = SIMIX_COMM_RECEIVE; pattern->comm = simcall_comm_irecv__get__result(request); + pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name); pattern->dst_proc = pattern->comm->comm.dst_proc->pid; pattern->dst_host = simcall_host_get_name(request->issuer->smx_host); } else { xbt_die("Unexpected call_type %i", (int) call_type); } - if (pattern->comm->comm.rdv != NULL) - pattern->rdv = strdup(pattern->comm->comm.rdv->name); - else - pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name); - - xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(list, request->issuer->pid, xbt_dynar_t), &pattern); - - xbt_dynar_push_as((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t), int, xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(list, request->issuer->pid, xbt_dynar_t)) - 1); + xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t), &pattern); + XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, request->issuer->pid); } - void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm) - { + void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, int backtracking) { + mc_comm_pattern_t current_comm_pattern; unsigned int cursor = 0; - int index; unsigned int src = comm->comm.src_proc->pid; unsigned int dst = comm->comm.dst_proc->pid; + mc_comm_pattern_t src_comm_pattern; + mc_comm_pattern_t dst_comm_pattern; int src_completed = 0, dst_completed = 0; - /* Looking for the corresponding communication in the comm pattern list of the src process */ - xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, index){ - current_comm_pattern = (mc_comm_pattern_t) xbt_dynar_get_as((xbt_dynar_t)xbt_dynar_get_as(list, src, xbt_dynar_t), index, mc_comm_pattern_t); - if(current_comm_pattern->comm == comm){ + /* Complete comm pattern */ + xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, current_comm_pattern) { + if (current_comm_pattern-> comm == comm) { update_comm_pattern(current_comm_pattern, comm); - xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, NULL); src_completed = 1; + xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, &src_comm_pattern); + XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", src, cursor); break; } } - if(!src_completed) xbt_die("Corresponding communication for the source process not found!"); cursor = 0; - /* Looking for the corresponding communication in the comm pattern list of the dst process */ - xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, index){ - current_comm_pattern = (mc_comm_pattern_t) xbt_dynar_get_as((xbt_dynar_t)xbt_dynar_get_as(list, dst, xbt_dynar_t), index, mc_comm_pattern_t); - if(current_comm_pattern->comm == comm){ + xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, current_comm_pattern) { + if (current_comm_pattern-> comm == comm) { update_comm_pattern(current_comm_pattern, comm); - xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, NULL); dst_completed = 1; + xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, &dst_comm_pattern); + XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", dst, cursor); break; } } - if(!dst_completed) - xbt_die("Corresponding communication for the dest process not found!"); - - + xbt_die("Corresponding communication for the destination process not found!"); + + if (!initial_global_state->initial_communications_pattern_done) { + /* Store comm pattern */ + if(src_comm_pattern->index < xbt_dynar_length(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list)){ + xbt_dynar_set(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list, src_comm_pattern->index, &src_comm_pattern); + ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list->used++; + } else { + xbt_dynar_insert_at(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list, src_comm_pattern->index, &src_comm_pattern); + } + + if(dst_comm_pattern->index < xbt_dynar_length(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list)) { + xbt_dynar_set(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list, dst_comm_pattern->index, &dst_comm_pattern); + ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list->used++; + } else { + xbt_dynar_insert_at(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list, dst_comm_pattern->index, &dst_comm_pattern); + } + ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->index_comm++; + ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->index_comm++; + } else { + /* Evaluate comm determinism */ + deterministic_comm_pattern(src, src_comm_pattern, backtracking); + deterministic_comm_pattern(dst, dst_comm_pattern, backtracking); + } } /************************ Main algorithm ************************/ void MC_pre_modelcheck_comm_determinism(void) { - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); + MC_SET_MC_HEAP; mc_state_t initial_state = NULL; smx_process_t process; int i; - if (!mc_mem_set) - MC_SET_MC_HEAP; - if (_sg_mc_visited > 0) visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); - initial_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp); - for (i=0; ilist = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); + process_list_pattern->index_comm = 0; + xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern); } incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp); for (i=0; i 0) { /* Get current state */ - state = - (mc_state_t) - xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); + state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); XBT_DEBUG("**************************************************"); XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)", @@@ -343,8 -398,10 +397,10 @@@ && (req = MC_state_get_request(state, &value)) && (visited_state == NULL)) { - MC_LOG_REQUEST(mc_comm_determinism, req, value); - + req_str = MC_request_to_string(req, value); + XBT_DEBUG("Execute: %s", req_str); + xbt_free(req_str); + if (dot_output != NULL) { MC_SET_MC_HEAP; req_str = MC_request_get_dot_output(req, value); @@@ -355,7 -412,7 +411,7 @@@ mc_stats->executed_transitions++; /* TODO : handle test and testany simcalls */ - mc_call_type call = MC_CALL_TYPE_NONE; + e_mc_call_type_t call = MC_CALL_TYPE_NONE; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { call = mc_get_call_type(req); } @@@ -364,8 -421,10 +420,10 @@@ SIMIX_simcall_handle(req, value); /* After this call req is no longer useful */ MC_SET_MC_HEAP; - current_pattern = !initial_global_state->initial_communications_pattern_done ? initial_communications_pattern : communications_pattern; - mc_update_comm_pattern(call, req, value, current_pattern); + if(!initial_global_state->initial_communications_pattern_done) + handle_comm_pattern(call, req, value, initial_communications_pattern, 0); + else + handle_comm_pattern(call, req, value, NULL, 0); MC_SET_STD_HEAP; /* Wait for requests (schedules processes) */ @@@ -376,7 -435,7 +434,7 @@@ next_state = MC_state_new(); - if ((visited_state = is_visited_state()) == NULL) { + if ((visited_state = is_visited_state(next_state)) == NULL) { /* Get enabled processes and insert them in the interleave set of the next state */ xbt_swag_foreach(process, simix_global->process_list) { @@@ -386,14 -445,12 +444,12 @@@ } if (dot_output != NULL) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, - next_state->num, req_str); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str); } else { if (dot_output != NULL) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, - visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); } @@@ -416,49 -473,13 +472,13 @@@ MC_SET_MC_HEAP; - if (initial_global_state->initial_communications_pattern_done) { - if (!visited_state) { - deterministic_pattern(communications_pattern, 0); - } else { - deterministic_pattern(communications_pattern, 1); - } - - if (_sg_mc_comms_determinism && !initial_global_state->comm_deterministic) { - XBT_INFO("****************************************************"); - XBT_INFO("***** Non-deterministic communications pattern *****"); - XBT_INFO("****************************************************"); - XBT_INFO("** Initial communications pattern (per process): **"); - print_communications_pattern(initial_communications_pattern); - XBT_INFO("** Communications pattern counter-example (per process): **"); - print_communications_pattern(communications_pattern); - MC_print_statistics(mc_stats); - MC_SET_STD_HEAP; - return; - } else if (_sg_mc_send_determinism && !initial_global_state->send_deterministic) { - XBT_INFO - ("*********************************************************"); - XBT_INFO - ("***** Non-send-deterministic communications pattern *****"); - XBT_INFO - ("*********************************************************"); - XBT_INFO("** Initial communications pattern: **"); - print_communications_pattern(initial_communications_pattern); - XBT_INFO("** Communications pattern counter-example: **"); - print_communications_pattern(communications_pattern); - MC_print_statistics(mc_stats); - MC_SET_STD_HEAP; - return; - } - - } else { + if (!initial_global_state->initial_communications_pattern_done) initial_global_state->initial_communications_pattern_done = 1; - } /* Trash the current state, no longer needed */ xbt_fifo_shift(mc_stack); - MC_state_delete(state); - XBT_DEBUG("Delete state %d at depth %d", state->num, - xbt_fifo_size(mc_stack) + 1); + MC_state_delete(state, !state->in_visited_states ? 1 : 0); + XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1); MC_SET_STD_HEAP; @@@ -473,23 -494,20 +493,20 @@@ MC_SET_MC_HEAP; while ((state = xbt_fifo_shift(mc_stack)) != NULL) { - if (MC_state_interleave_size(state) - && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) { + if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ - XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, - xbt_fifo_size(mc_stack) + 1); + XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1); xbt_fifo_unshift(mc_stack, state); MC_SET_STD_HEAP; - MC_replay(mc_stack, -1); + MC_replay(mc_stack); + + XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack)); - XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, - xbt_fifo_size(mc_stack)); break; } else { - XBT_DEBUG("Delete state %d at depth %d", state->num, - xbt_fifo_size(mc_stack) + 1); - MC_state_delete(state); + XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1); + MC_state_delete(state, !state->in_visited_states ? 1 : 0); } } diff --combined src/mc/mc_forward.h index de151e09d4,267f82cbfa..bd78e99299 --- a/src/mc/mc_forward.h +++ b/src/mc/mc_forward.h @@@ -8,18 -8,14 +8,18 @@@ #define MC_FORWARD_H #include + #include "mc_interface.h" typedef struct s_mc_object_info s_mc_object_info_t, *mc_object_info_t; - typedef struct s_mc_transition s_mc_transition_t, *mc_transition_t; typedef struct s_dw_type s_dw_type_t, *dw_type_t; typedef struct s_memory_map s_memory_map_t, *memory_map_t; typedef struct s_dw_variable s_dw_variable_t, *dw_variable_t; typedef struct s_dw_frame s_dw_frame_t, *dw_frame_t; + typedef struct s_mc_pages_store s_mc_pages_store_t, *mc_pages_store_t; +typedef struct s_mc_snapshot s_mc_snapshot_t, *mc_snapshot_t; + +typedef struct s_mc_process s_mc_process_t, * mc_process_t; typedef struct s_mc_model_checker s_mc_model_checker_t, *mc_model_checker_t; extern mc_model_checker_t mc_model_checker; diff --combined src/mc/mc_global.c index 5c5fb92f92,63ecd05968..85dacbca78 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@@ -4,14 -4,15 +4,14 @@@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ +#include + #include "mc_base.h" #ifndef _XBT_WIN32 #include -#include #include #include -#include -#include #endif #include "simgrid/sg_config.h" @@@ -22,8 -23,8 +22,8 @@@ #include "xbt/dict.h" #ifdef HAVE_MC -#define UNW_LOCAL_ONLY #include +#include #include "../xbt/mmalloc/mmprivate.h" #include "mc_object_info.h" @@@ -34,17 -35,12 +34,17 @@@ #include "mc_snapshot.h" #include "mc_liveness.h" #include "mc_private.h" +#include "mc_unw.h" #endif #include "mc_record.h" +#include "mc_protocol.h" +#include "mc_client.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)"); +e_mc_mode_t mc_mode; + double *mc_time = NULL; #ifdef HAVE_MC @@@ -63,6 -59,14 +63,6 @@@ xbt_fifo_t mc_stack = NULL /* Liveness */ xbt_automaton_t _mc_property_automaton = NULL; -/* Variables */ -mc_object_info_t mc_libsimgrid_info = NULL; -mc_object_info_t mc_binary_info = NULL; - -mc_object_info_t mc_object_infos[2] = { NULL, NULL }; - -size_t mc_object_infos_size = 2; - /* Dot output */ FILE *dot_output = NULL; const char *colors[13]; @@@ -100,29 -104,57 +100,29 @@@ static void MC_init_dot_output( } -static void MC_init_debug_info(void) -{ - XBT_INFO("Get debug information ..."); - - memory_map_t maps = MC_get_memory_map(); - - /* Get local variables for state equality detection */ - mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1); - mc_object_infos[0] = mc_binary_info; - - mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0); - mc_object_infos[1] = mc_libsimgrid_info; - - // Use information of the other objects: - MC_post_process_object_info(mc_binary_info); - MC_post_process_object_info(mc_libsimgrid_info); - - MC_free_memory_map(maps); - XBT_INFO("Get debug information done !"); -} - - -mc_model_checker_t mc_model_checker = NULL; - -mc_model_checker_t MC_model_checker_new() +void MC_init() { - mc_model_checker_t mc = xbt_new0(s_mc_model_checker_t, 1); - mc->pages = mc_pages_store_new(); - mc->fd_clear_refs = -1; - mc->fd_pagemap = -1; - return mc; + MC_init_pid(getpid(), -1); } -void MC_model_checker_delete(mc_model_checker_t mc) { - mc_pages_store_delete(mc->pages); - if(mc->record) - xbt_dynar_free(&mc->record); -} - -void MC_init() +void MC_init_pid(pid_t pid, int socket) { - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); + if (mc_mode == MC_MODE_NONE) { + if (getenv(MC_ENV_SOCKET_FD)) { + mc_mode = MC_MODE_CLIENT; + } else { + mc_mode = MC_MODE_STANDALONE; + } + } mc_time = xbt_new0(double, simix_process_maxpid); /* Initialize the data structures that must be persistent across every iteration of the model-checker (in RAW memory) */ - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - mc_model_checker = MC_model_checker_new(); + mc_model_checker = MC_model_checker_new(pid, socket); mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); @@@ -130,6 -162,9 +130,6 @@@ mc_stats = xbt_new0(s_mc_stats_t, 1); mc_stats->state_size = 1; - MC_init_memory_map_info(); - MC_init_debug_info(); /* FIXME : get debug information only if liveness verification or visited state reduction */ - if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0')) MC_init_dot_output(); @@@ -159,9 -194,9 +159,9 @@@ /* Main MC state: */ MC_ignore_global_variable("mc_model_checker"); - MC_ignore_global_variable("communications_pattern"); MC_ignore_global_variable("initial_communications_pattern"); MC_ignore_global_variable("incomplete_communications_pattern"); + MC_ignore_global_variable("nb_comm_pattern"); /* MC __thread variables: */ MC_ignore_global_variable("mc_diff_info"); @@@ -177,22 -212,16 +177,22 @@@ /* SIMIX */ MC_ignore_global_variable("smx_total_comms"); - MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); + if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) { + MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); + - smx_process_t process; - xbt_swag_foreach(process, simix_global->process_list) { - MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup)); + smx_process_t process; + xbt_swag_foreach(process, simix_global->process_list) { - MC_ignore_heap(&(process->process_hookup), - sizeof(process->process_hookup)); - } ++ MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup)); ++ } } } - if (raw_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); + + if (mc_mode == MC_MODE_CLIENT) { + // This will move somehwere else: + MC_client_handle_messages(); + } } @@@ -201,9 -230,13 +201,9 @@@ static void MC_modelcheck_comm_determinism_init(void) { - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_init(); - if (!mc_mem_set) - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); /* Create exploration stack */ mc_stack = xbt_fifo_new(); @@@ -222,16 -255,21 +222,16 @@@ MC_modelcheck_comm_determinism(); - if(mc_mem_set) - MC_SET_MC_HEAP; - + mmalloc_set_current_heap(heap); } static void MC_modelcheck_safety_init(void) { - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - _sg_mc_safety = 1; MC_init(); - if (!mc_mem_set) - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); /* Create exploration stack */ mc_stack = xbt_fifo_new(); @@@ -248,7 -286,8 +248,7 @@@ MC_modelcheck_safety(); - if (mc_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); xbt_abort(); //MC_exit(); @@@ -256,11 -295,15 +256,11 @@@ static void MC_modelcheck_liveness_init() { - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - _sg_mc_liveness = 1; MC_init(); - if (!mc_mem_set) - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); /* Create exploration stack */ mc_stack = xbt_fifo_new(); @@@ -276,7 -319,8 +276,7 @@@ MC_print_statistics(mc_stats); xbt_free(mc_time); - if (mc_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); } @@@ -325,7 -369,8 +325,8 @@@ int MC_deadlock_check( return deadlock; } - void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value, xbt_dynar_t pattern) { + void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int value, xbt_dynar_t pattern, int backtracking) { + switch(call_type) { case MC_CALL_TYPE_NONE: break; @@@ -334,6 -379,7 +335,7 @@@ get_comm_pattern(pattern, req, call_type); break; case MC_CALL_TYPE_WAIT: + case MC_CALL_TYPE_WAITANY: { smx_synchro_t current_comm = NULL; if (call_type == MC_CALL_TYPE_WAIT) @@@ -342,12 -388,51 +344,51 @@@ current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t); // First wait only must be considered: if (current_comm->comm.refcount == 1) - complete_comm_pattern(pattern, current_comm); + complete_comm_pattern(pattern, current_comm, backtracking); break; } default: xbt_die("Unexpected call type %i", (int)call_type); } + + } + + static void MC_restore_communications_pattern(mc_state_t state) { + mc_list_comm_pattern_t list_process_comm; + unsigned int cursor, cursor2; + xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){ + list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int); + } + mc_comm_pattern_t comm; + cursor = 0; + xbt_dynar_t initial_incomplete_process_comms, incomplete_process_comms; + for(int i=0; iincomplete_comm_pattern, i, xbt_dynar_t); + xbt_dynar_foreach(incomplete_process_comms, cursor2, comm) { + mc_comm_pattern_t copy_comm = xbt_new0(s_mc_comm_pattern_t, 1); + copy_comm->index = comm->index; + copy_comm->type = comm->type; + copy_comm->comm = comm->comm; + copy_comm->rdv = strdup(comm->rdv); + copy_comm->data_size = -1; + copy_comm->data = NULL; + if(comm->type == SIMIX_COMM_SEND){ + copy_comm->src_proc = comm->src_proc; + copy_comm->src_host = comm->src_host; + if(comm->data != NULL){ + copy_comm->data_size = comm->data_size; + copy_comm->data = xbt_malloc0(comm->data_size); + memcpy(copy_comm->data, comm->data, comm->data_size); + } + }else{ + copy_comm->dst_proc = comm->dst_proc; + copy_comm->dst_host = comm->dst_host; + } + xbt_dynar_push(initial_incomplete_process_comms, ©_comm); + } + } } /** @@@ -355,63 -440,47 +396,47 @@@ * a given model-checker stack. * \param stack The stack with the transitions to execute. * \param start Start index to begin the re-execution. - * - * If start==-1, restore the initial state and replay the actions the - * the transitions in the stack. - * - * Otherwise, we only replay a part of the transitions of the stacks - * without restoring the state: it is assumed that the current state - * match with the transitions to execute. */ - void MC_replay(xbt_fifo_t stack, int start) + void MC_replay(xbt_fifo_t stack) { - int raw_mem = (mmalloc_get_current_heap() == mc_heap); + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - int value, i = 1, count = 1, j; + int value, count = 1, j; char *req_str; smx_simcall_t req = NULL, saved_req = NULL; xbt_fifo_item_t item, start_item; mc_state_t state; - smx_process_t process = NULL; - + XBT_DEBUG("**** Begin Replay ****"); - if (start == -1) { - /* Restore the initial state */ - MC_restore_snapshot(initial_global_state->snapshot); - /* At the moment of taking the snapshot the raw heap was set, so restoring - * it will set it back again, we have to unset it to continue */ - MC_SET_STD_HEAP; - } - - start_item = xbt_fifo_get_last_item(stack); - if (start != -1) { - while (i != start) { - start_item = xbt_fifo_get_prev_item(start_item); - i++; + /* Intermediate backtracking */ + if(_sg_mc_checkpoint > 0) { + start_item = xbt_fifo_get_first_item(stack); + state = (mc_state_t)xbt_fifo_get_item_content(start_item); + if(state->system_state){ + MC_restore_snapshot(state->system_state); + if(_sg_mc_comms_determinism || _sg_mc_send_determinism) + MC_restore_communications_pattern(state); + MC_SET_STD_HEAP; + return; } } - MC_SET_MC_HEAP; - if (mc_reduce_kind == e_mc_reduce_dpor) { - xbt_dict_reset(first_enabled_state); - xbt_swag_foreach(process, simix_global->process_list) { - if (MC_process_is_enabled(process)) { - char *key = bprintf("%lu", process->pid); - char *data = bprintf("%d", count); - xbt_dict_set(first_enabled_state, key, data, NULL); - xbt_free(key); - } - } - } + /* Restore the initial state */ + MC_restore_snapshot(initial_global_state->snapshot); + /* At the moment of taking the snapshot the raw heap was set, so restoring + * it will set it back again, we have to unset it to continue */ + MC_SET_STD_HEAP; + + start_item = xbt_fifo_get_last_item(stack); + + MC_SET_MC_HEAP; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - for (j=0; jindex_comm = 0; } } @@@ -424,16 -493,7 +449,7 @@@ state = (mc_state_t) xbt_fifo_get_item_content(item); saved_req = MC_state_get_executed_request(state, &value); - - if (mc_reduce_kind == e_mc_reduce_dpor) { - MC_SET_MC_HEAP; - char *key = bprintf("%lu", saved_req->issuer->pid); - if(xbt_dict_get_or_null(first_enabled_state, key)) - xbt_dict_remove(first_enabled_state, key); - xbt_free(key); - MC_SET_STD_HEAP; - } - + if (saved_req) { /* because we got a copy of the executed request, we have to fetch the real one, pointed by the request field of the issuer process */ @@@ -447,38 -507,20 +463,20 @@@ } /* TODO : handle test and testany simcalls */ - mc_call_type call = MC_CALL_TYPE_NONE; - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { + e_mc_call_type_t call = MC_CALL_TYPE_NONE; + if (_sg_mc_comms_determinism || _sg_mc_send_determinism) call = mc_get_call_type(req); - } SIMIX_simcall_handle(req, value); - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - MC_SET_MC_HEAP; - mc_update_comm_pattern(call, req, value, communications_pattern); - MC_SET_STD_HEAP; - } - + MC_SET_MC_HEAP; + if (_sg_mc_comms_determinism || _sg_mc_send_determinism) + handle_comm_pattern(call, req, value, NULL, 1); + MC_SET_STD_HEAP; + MC_wait_for_requests(); count++; - - if (mc_reduce_kind == e_mc_reduce_dpor) { - MC_SET_MC_HEAP; - /* Insert in dict all enabled processes */ - xbt_swag_foreach(process, simix_global->process_list) { - if (MC_process_is_enabled(process) ) { - char *key = bprintf("%lu", process->pid); - if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) { - char *data = bprintf("%d", count); - xbt_dict_set(first_enabled_state, key, data, NULL); - } - xbt_free(key); - } - } - MC_SET_STD_HEAP; - } } /* Update statistics */ @@@ -488,19 -530,40 +486,34 @@@ } XBT_DEBUG("**** End Replay ****"); - - if (raw_mem) - MC_SET_MC_HEAP; - else - MC_SET_STD_HEAP; - - + mmalloc_set_current_heap(heap); } - void MC_replay_liveness(xbt_fifo_t stack, int all_stack) + void MC_replay_liveness(xbt_fifo_t stack) { initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap); xbt_fifo_item_t item; - int depth = 1; + mc_pair_t pair = NULL; + mc_state_t state = NULL; + smx_simcall_t req = NULL, saved_req = NULL; + int value, depth = 1; + char *req_str; XBT_DEBUG("**** Begin Replay ****"); + /* Intermediate backtracking */ + if(_sg_mc_checkpoint > 0) { + item = xbt_fifo_get_first_item(stack); + pair = (mc_pair_t) xbt_fifo_get_item_content(item); + if(pair->graph_state->system_state){ + MC_restore_snapshot(pair->graph_state->system_state); + MC_SET_STD_HEAP; + return; + } + } + /* Restore the initial state */ MC_restore_snapshot(initial_global_state->snapshot); @@@ -511,26 -574,21 +524,21 @@@ /* Traverse the stack from the initial state and re-execute the transitions */ for (item = xbt_fifo_get_last_item(stack); - all_stack ? depth <= xbt_fifo_size(stack) : item != xbt_fifo_get_first_item(stack); + item != xbt_fifo_get_first_item(stack); item = xbt_fifo_get_prev_item(item)) { - mc_pair_t pair = (mc_pair_t) xbt_fifo_get_item_content(item); + pair = (mc_pair_t) xbt_fifo_get_item_content(item); - mc_state_t state = (mc_state_t) pair->graph_state; - smx_simcall_t req = NULL, saved_req = NULL; - int value; - char *req_str; + state = (mc_state_t) pair->graph_state; - if (pair->requests > 0) { + if (pair->exploration_started) { saved_req = MC_state_get_executed_request(state, &value); - //XBT_DEBUG("SavedReq->call %u", saved_req->call); if (saved_req != NULL) { /* because we got a copy of the executed request, we have to fetch the real one, pointed by the request field of the issuer process */ req = &saved_req->issuer->simcall; - //XBT_DEBUG("Req->call %u", req->call); /* Debug information */ if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) { @@@ -550,7 -608,7 +558,7 @@@ mc_stats->executed_transitions++; depth++; - + } XBT_DEBUG("**** End Replay ****"); @@@ -569,28 -627,32 +577,22 @@@ */ void MC_dump_stack_safety(xbt_fifo_t stack) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); MC_show_stack_safety(stack); - - if (!_sg_mc_checkpoint) { - - mc_state_t state; - - MC_SET_MC_HEAP; - while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) - MC_state_delete(state); - MC_SET_STD_HEAP; - - } - + + mc_state_t state; + + MC_SET_MC_HEAP; + while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) + MC_state_delete(state, !state->in_visited_states ? 1 : 0); - MC_SET_STD_HEAP; - - if (raw_mem_set) - MC_SET_MC_HEAP; - else - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); } void MC_show_stack_safety(xbt_fifo_t stack) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); int value; mc_state_t state; @@@ -609,7 -671,8 +611,7 @@@ } } - if (!raw_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); } void MC_show_deadlock(smx_simcall_t req) @@@ -637,33 -700,40 +639,30 @@@ void MC_show_stack_liveness(xbt_fifo_t char *req_str = NULL; for (item = xbt_fifo_get_last_item(stack); - (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item))) - : (NULL)); item = xbt_fifo_get_prev_item(item)) { + (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item))) : (NULL)); + item = xbt_fifo_get_prev_item(item)) { req = MC_state_get_executed_request(pair->graph_state, &value); - if (req) { - if (pair->requests > 0) { - req_str = MC_request_to_string(req, value); - XBT_INFO("%s", req_str); - xbt_free(req_str); - } else { - XBT_INFO("End of system requests but evolution in Büchi automaton"); - } + if (req && req->call != SIMCALL_NONE) { + req_str = MC_request_to_string(req, value); + XBT_INFO("%s", req_str); + xbt_free(req_str); } } } + void MC_dump_stack_liveness(xbt_fifo_t stack) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); mc_pair_t pair; - - MC_SET_MC_HEAP; while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL) MC_pair_delete(pair); - MC_SET_STD_HEAP; - - if (raw_mem_set) - MC_SET_MC_HEAP; - + mmalloc_set_current_heap(heap); } void MC_print_statistics(mc_stats_t stats) { - xbt_mheap_t previous_heap = mmalloc_get_current_heap(); - if (stats->expanded_pairs == 0) { XBT_INFO("Expanded states = %lu", stats->expanded_states); XBT_INFO("Visited states = %lu", stats->visited_states); @@@ -672,86 -742,81 +671,84 @@@ XBT_INFO("Visited pairs = %lu", stats->visited_pairs); } XBT_INFO("Executed transitions = %lu", stats->executed_transitions); - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0')) { fprintf(dot_output, "}\n"); fclose(dot_output); } if (initial_global_state != NULL) { if (_sg_mc_comms_determinism) - XBT_INFO("Communication-deterministic : %s", - !initial_global_state->comm_deterministic ? "No" : "Yes"); + XBT_INFO("Communication-deterministic : %s", !initial_global_state->comm_deterministic ? "No" : "Yes"); if (_sg_mc_send_determinism) - XBT_INFO("Send-deterministic : %s", - !initial_global_state->send_deterministic ? "No" : "Yes"); + XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes"); } - mmalloc_set_current_heap(previous_heap); -} - -void MC_assert(int prop) -{ - if (MC_is_active() && !prop) { - XBT_INFO("**************************"); - XBT_INFO("*** PROPERTY NOT VALID ***"); - XBT_INFO("**************************"); - XBT_INFO("Counter-example execution trace:"); - MC_record_dump_path(mc_stack); - MC_dump_stack_safety(mc_stack); - MC_print_statistics(mc_stats); - xbt_abort(); - } -} - -void MC_cut(void) -{ - user_max_depth_reached = 1; + mmalloc_set_current_heap(heap); } void MC_automaton_load(const char *file) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); xbt_automaton_load(_mc_property_automaton, file); - - MC_SET_STD_HEAP; - - if (raw_mem_set) - MC_SET_MC_HEAP; - + mmalloc_set_current_heap(heap); } -void MC_automaton_new_propositional_symbol(const char *id, void *fct) +static void register_symbol(xbt_automaton_propositional_symbol_t symbol) { + if (mc_mode != MC_MODE_CLIENT) + return; + s_mc_register_symbol_message_t message; + message.type = MC_MESSAGE_REGISTER_SYMBOL; + const char* name = xbt_automaton_propositional_symbol_get_name(symbol); + if (strlen(name) + 1 > sizeof(message.name)) + xbt_die("Symbol is too long"); + strncpy(message.name, name, sizeof(message.name)); + message.callback = xbt_automaton_propositional_symbol_get_callback(symbol); + message.data = xbt_automaton_propositional_symbol_get_data(symbol); + MC_client_send_message(&message, sizeof(message)); +} - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; +void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void)) +{ + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); - xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct); - - MC_SET_STD_HEAP; + xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct); + register_symbol(symbol); + mmalloc_set_current_heap(heap); +} - if (raw_mem_set) - MC_SET_MC_HEAP; +void MC_automaton_new_propositional_symbol_pointer(const char *id, int* value) +{ + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + if (_mc_property_automaton == NULL) + _mc_property_automaton = xbt_automaton_new(); + xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_pointer(_mc_property_automaton, id, value); + register_symbol(symbol); + mmalloc_set_current_heap(heap); +} +void MC_automaton_new_propositional_symbol_callback(const char* id, + xbt_automaton_propositional_symbol_callback_type callback, + void* data, xbt_automaton_propositional_symbol_free_function_type free_function) +{ + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + if (_mc_property_automaton == NULL) + _mc_property_automaton = xbt_automaton_new(); + xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_callback( + _mc_property_automaton, id, callback, data, free_function); + register_symbol(symbol); + mmalloc_set_current_heap(heap); } void MC_dump_stacks(FILE* file) { - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); int nstack = 0; stack_region_t current_stack; @@@ -773,7 -838,9 +770,7 @@@ ++nstack; } - - if (raw_mem_set) - MC_SET_MC_HEAP; + mmalloc_set_current_heap(heap); } #endif diff --combined src/mc/mc_liveness.c index ceb77db24f,6a21a60f2c..ec50dad337 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@@ -21,40 -21,41 +21,33 @@@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_live /********* Global variables *********/ xbt_dynar_t acceptance_pairs; - xbt_dynar_t successors; xbt_parmap_t parmap; /********* Static functions *********/ static xbt_dynar_t get_atomic_propositions_values() { - int res; - int_f_void_t f; unsigned int cursor = 0; xbt_automaton_propositional_symbol_t ps = NULL; xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL); - xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps) { - f = (int_f_void_t) ps->function; - res = f(); + int res = xbt_automaton_propositional_symbol_evaluate(ps); xbt_dynar_push_as(values, int, res); } return values; } -- - static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, - xbt_automaton_state_t - automaton_state, - xbt_dynar_t - atomic_propositions) - { -static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair){ - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; ++static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair) { + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - mc_visited_pair_t pair = NULL; - pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions); - pair->acceptance_pair = 1; + mc_visited_pair_t new_pair = NULL; + new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); + new_pair->acceptance_pair = 1; if (xbt_dynar_is_empty(acceptance_pairs)) { - xbt_dynar_push(acceptance_pairs, &pair); + xbt_dynar_push(acceptance_pairs, &new_pair); } else { @@@ -63,7 -64,7 +56,7 @@@ mc_visited_pair_t pair_test; int cursor; - index = get_search_interval(acceptance_pairs, pair, &min, &max); + index = get_search_interval(acceptance_pairs, new_pair, &min, &max); if (min != -1 && max != -1) { // Acceptance pair with same number of processes and same heap bytes used exists @@@ -76,75 -77,78 +69,68 @@@ } */ cursor = min; - while (cursor <= max) { - pair_test = - (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, cursor, - mc_visited_pair_t); - if (xbt_automaton_state_compare - (pair_test->automaton_state, pair->automaton_state) == 0) { - if (xbt_automaton_propositional_symbols_compare_value - (pair_test->atomic_propositions, - pair->atomic_propositions) == 0) { - if (snapshot_compare(pair_test, pair) == 0) { - XBT_INFO("Pair %d already reached (equal to pair %d) !", - pair->num, pair_test->num); - - xbt_fifo_shift(mc_stack); - if (dot_output != NULL) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - initial_global_state->prev_pair, pair_test->num, - initial_global_state->prev_req); - mmalloc_set_current_heap(heap); - return NULL; + if(pair->search_cycle == 1){ + while (cursor <= max) { + pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t); + if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) { + if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_pair->atomic_propositions) == 0) { + if (snapshot_compare(pair_test, new_pair) == 0) { + XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); + xbt_fifo_shift(mc_stack); + if (dot_output != NULL) + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req); - - if (!raw_mem_set) - MC_SET_STD_HEAP; - ++ mmalloc_set_current_heap(heap); + return NULL; + } } } + cursor++; } - cursor++; } - xbt_dynar_insert_at(acceptance_pairs, min, &pair); + xbt_dynar_insert_at(acceptance_pairs, min, &new_pair); } else { - pair_test = - (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index, - mc_visited_pair_t); - if (pair_test->nb_processes < pair->nb_processes) { - xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair); + pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t); + if (pair_test->nb_processes < new_pair->nb_processes) { + xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair); } else { - if (pair_test->heap_bytes_used < pair->heap_bytes_used) - xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair); + if (pair_test->heap_bytes_used < new_pair->heap_bytes_used) + xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair); else - xbt_dynar_insert_at(acceptance_pairs, index, &pair); + xbt_dynar_insert_at(acceptance_pairs, index, &new_pair); } } } - - if (!raw_mem_set) - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); - return pair; + return new_pair; - } -static void remove_acceptance_pair(int pair_num) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; +static void remove_acceptance_pair(int pair_num) +{ + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); unsigned int cursor = 0; mc_visited_pair_t pair_test = NULL; + int pair_found = 0; xbt_dynar_foreach(acceptance_pairs, cursor, pair_test) { if (pair_test->num == pair_num) { + pair_found = 1; break; } } - xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test); + if(pair_found == 1) { + xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test); + + pair_test->acceptance_removed = 1; - pair_test->acceptance_removed = 1; + if (_sg_mc_visited == 0 || pair_test->visited_removed == 1) + MC_visited_pair_delete(pair_test); - if (_sg_mc_visited == 0) { - MC_visited_pair_delete(pair_test); - } else if (pair_test->visited_removed == 1) { - MC_visited_pair_delete(pair_test); } - if (!raw_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); } @@@ -154,36 -158,25 +140,25 @@@ static int MC_automaton_evaluate_label( switch (l->type) { case 0:{ - int left_res = - MC_automaton_evaluate_label(l->u.or_and.left_exp, - atomic_propositions_values); - int right_res = - MC_automaton_evaluate_label(l->u.or_and.right_exp, - atomic_propositions_values); + int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values); + int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values); return (left_res || right_res); } case 1:{ - int left_res = - MC_automaton_evaluate_label(l->u.or_and.left_exp, - atomic_propositions_values); - int right_res = - MC_automaton_evaluate_label(l->u.or_and.right_exp, - atomic_propositions_values); + int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values); + int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values); return (left_res && right_res); } case 2:{ - int res = - MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values); + int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values); return (!res); } case 3:{ unsigned int cursor = 0; xbt_automaton_propositional_symbol_t p = NULL; - xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, - p) { + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p) { - if (strcmp(p->pred, l->u.predicat) == 0) + if (strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0) - return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, - int); + return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, int); } return -1; } @@@ -195,8 -188,7 +170,7 @@@ } } - void MC_pre_modelcheck_liveness(void) - { + void MC_pre_modelcheck_liveness(void) { initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap); @@@ -208,26 -200,23 +182,23 @@@ MC_SET_MC_HEAP; acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); - visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); - successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); + if(_sg_mc_visited > 0) + visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); initial_global_state->snapshot = MC_take_snapshot(0); initial_global_state->prev_pair = 0; - MC_SET_STD_HEAP; - unsigned int cursor = 0; xbt_automaton_state_t automaton_state; - + xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state) { if (automaton_state->type == -1) { /* Initial automaton state */ - MC_SET_MC_HEAP; - initial_pair = MC_pair_new(); initial_pair->automaton_state = automaton_state; initial_pair->graph_state = MC_state_new(); initial_pair->atomic_propositions = get_atomic_propositions_values(); + initial_pair->depth = 1; /* Get enabled processes and insert them in the interleave set of the graph_state */ xbt_swag_foreach(process, simix_global->process_list) { @@@ -236,173 -225,136 +207,134 @@@ } } - initial_pair->requests = - MC_state_interleave_size(initial_pair->graph_state); + initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state); initial_pair->search_cycle = 0; xbt_fifo_unshift(mc_stack, initial_pair); - - MC_SET_STD_HEAP; - - MC_modelcheck_liveness(); - - if (cursor != 0) { - MC_restore_snapshot(initial_global_state->snapshot); - MC_SET_STD_HEAP; - } } } + MC_SET_STD_HEAP; + + MC_modelcheck_liveness(); + if (initial_global_state->raw_mem_set) MC_SET_MC_HEAP; - else - MC_SET_STD_HEAP; - - } -void MC_modelcheck_liveness() { -- +void MC_modelcheck_liveness() +{ - smx_process_t process; + smx_process_t process = NULL; mc_pair_t current_pair = NULL; - - if (xbt_fifo_size(mc_stack) == 0) - return; - - /* Get current pair */ - current_pair = - (mc_pair_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); - - /* Update current state in buchi automaton */ - _mc_property_automaton->current_state = current_pair->automaton_state; - - XBT_DEBUG - ("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)", - xbt_fifo_size(mc_stack), current_pair->search_cycle, - MC_state_interleave_size(current_pair->graph_state), current_pair->num); - - mc_stats->visited_pairs++; - - int value; + int value, res, visited_num = -1; smx_simcall_t req = NULL; - - xbt_automaton_transition_t transition_succ; - unsigned int cursor = 0; - int res; - int visited_num; - + xbt_automaton_transition_t transition_succ = NULL; + int cursor = 0; mc_pair_t next_pair = NULL; xbt_dynar_t prop_values = NULL; mc_visited_pair_t reached_pair = NULL; - int counter_example_depth = 0; + + while(xbt_fifo_size(mc_stack) > 0){ - if (xbt_fifo_size(mc_stack) < _sg_mc_max_depth) { + /* Get current pair */ + current_pair = (mc_pair_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); - if (current_pair->requests > 0) { + /* Update current state in buchi automaton */ + _mc_property_automaton->current_state = current_pair->automaton_state; + + XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)", + current_pair->depth, current_pair->search_cycle, + MC_state_interleave_size(current_pair->graph_state), current_pair->num); - if (current_pair->search_cycle) { - - if ((current_pair->automaton_state->type == 1) - || (current_pair->automaton_state->type == 2)) { - if ((reached_pair = - is_reached_acceptance_pair(current_pair->num, - current_pair->automaton_state, - current_pair->atomic_propositions)) == - NULL) { - - counter_example_depth = xbt_fifo_size(mc_stack); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("| ACCEPTANCE CYCLE |"); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); - MC_show_stack_liveness(mc_stack); - MC_dump_stack_liveness(mc_stack); - MC_print_statistics(mc_stats); - XBT_INFO("Counter-example depth : %d", counter_example_depth); - xbt_abort(); + if (current_pair->requests > 0) { - } + if (current_pair->automaton_state->type == 1 && current_pair->exploration_started == 0) { + /* If new acceptance pair, return new pair */ + if ((reached_pair = is_reached_acceptance_pair(current_pair)) == NULL) { + int counter_example_depth = current_pair->depth; + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("| ACCEPTANCE CYCLE |"); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("Counter-example that violates formula :"); + MC_show_stack_liveness(mc_stack); + MC_dump_stack_liveness(mc_stack); + MC_print_statistics(mc_stats); + XBT_INFO("Counter-example depth : %d", counter_example_depth); + xbt_abort(); } } - if ((visited_num = - is_visited_pair(reached_pair, current_pair->num, - current_pair->automaton_state, - current_pair->atomic_propositions)) != -1) { - - MC_SET_MC_HEAP; - if (dot_output != NULL) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - initial_global_state->prev_pair, visited_num, - initial_global_state->prev_req); - MC_SET_STD_HEAP; - - } else { - - while ((req = - MC_state_get_request(current_pair->graph_state, - &value)) != NULL) { - - MC_SET_MC_HEAP; - if (dot_output != NULL) { - if (initial_global_state->prev_pair != 0 - && initial_global_state->prev_pair != current_pair->num) { - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - initial_global_state->prev_pair, current_pair->num, - initial_global_state->prev_req); - xbt_free(initial_global_state->prev_req); - } - initial_global_state->prev_pair = current_pair->num; - } - MC_SET_STD_HEAP; - - MC_LOG_REQUEST(mc_liveness, req, value); - - MC_SET_MC_HEAP; - if (dot_output != NULL) { - initial_global_state->prev_req = - MC_request_get_dot_output(req, value); - if (current_pair->search_cycle) - fprintf(dot_output, "%d [shape=doublecircle];\n", - current_pair->num); - } - MC_SET_STD_HEAP; - - MC_state_set_executed_request(current_pair->graph_state, req, value); - mc_stats->executed_transitions++; - - /* Answer the request */ - SIMIX_simcall_handle(req, value); - - /* Wait for requests (schedules processes) */ - MC_wait_for_requests(); + /* Pair already visited ? stop the exploration on the current path */ + if ((current_pair->exploration_started == 0) && (visited_num = is_visited_pair(reached_pair, current_pair)) != -1) { + if (dot_output != NULL){ MC_SET_MC_HEAP; - prop_values = get_atomic_propositions_values(); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, visited_num, initial_global_state->prev_req); + fflush(dot_output); MC_SET_STD_HEAP; + } - int new_pair = 0; - - /* Evaluate enabled transition according to atomic propositions values */ - cursor = 0; - xbt_dynar_foreach(current_pair->automaton_state->out, cursor, - transition_succ) { - - res = - MC_automaton_evaluate_label(transition_succ->label, - prop_values); - - if (res == 1) { // enabled transition in automaton - - if (new_pair) - MC_replay_liveness(mc_stack, 1); - - MC_SET_MC_HEAP; - + XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num); + MC_SET_MC_HEAP; + current_pair->requests = 0; + MC_SET_STD_HEAP; + goto backtracking; + + }else{ + + req = MC_state_get_request(current_pair->graph_state, &value); + + if (dot_output != NULL) { + MC_SET_MC_HEAP; + if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) { + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, current_pair->num, initial_global_state->prev_req); + xbt_free(initial_global_state->prev_req); + } + initial_global_state->prev_pair = current_pair->num; + initial_global_state->prev_req = MC_request_get_dot_output(req, value); + if (current_pair->search_cycle) + fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num); + fflush(dot_output); + MC_SET_STD_HEAP; + } + + char* req_str = MC_request_to_string(req, value); + XBT_DEBUG("Execute: %s", req_str); + xbt_free(req_str); + + /* Set request as executed */ + MC_state_set_executed_request(current_pair->graph_state, req, value); + + /* Update mc_stats */ + mc_stats->executed_transitions++; + if(current_pair->exploration_started == 0) + mc_stats->visited_pairs++; + + /* Answer the request */ + SIMIX_simcall_handle(req, value); + + /* Wait for requests (schedules processes) */ + MC_wait_for_requests(); + + MC_SET_MC_HEAP; + + current_pair->requests--; + current_pair->exploration_started = 1; + + /* Get values of atomic propositions (variables used in the property formula) */ + prop_values = get_atomic_propositions_values(); + + /* Evaluate enabled/true transitions in automaton according to atomic propositions values and create new pairs */ + cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1; + while (cursor >= 0) { + transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t); + res = MC_automaton_evaluate_label(transition_succ->label, prop_values); + if (res == 1 || res == 2) { /* 1 = True transition (always enabled), 2 = enabled transition according to atomic prop values */ next_pair = MC_pair_new(); next_pair->graph_state = MC_state_new(); next_pair->automaton_state = transition_succ->dst; next_pair->atomic_propositions = get_atomic_propositions_values(); - + next_pair->depth = current_pair->depth + 1; /* Get enabled processes and insert them in the interleave set of the next graph_state */ xbt_swag_foreach(process, simix_global->process_list) { if (MC_process_is_enabled(process)) { @@@ -410,122 -362,56 +342,56 @@@ } } - next_pair->requests = - MC_state_interleave_size(next_pair->graph_state); + next_pair->requests = MC_state_interleave_size(next_pair->graph_state); - if (next_pair->automaton_state->type == 1 - || next_pair->automaton_state->type == 2 - || current_pair->search_cycle) + /* FIXME : get search_cycle value for each acceptant state */ + if (next_pair->automaton_state->type == 1 || current_pair->search_cycle) next_pair->search_cycle = 1; + /* Add new pair to the exploration stack */ xbt_fifo_unshift(mc_stack, next_pair); - if (mc_stats->expanded_pairs % 1000000 == 0) - XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs); - - MC_SET_STD_HEAP; - - new_pair = 1; - - MC_modelcheck_liveness(); - - } - - } - - /* Then, evaluate true transitions (always true, whatever atomic propositions values) */ - cursor = 0; - xbt_dynar_foreach(current_pair->automaton_state->out, cursor, - transition_succ) { - - res = - MC_automaton_evaluate_label(transition_succ->label, - prop_values); - - if (res == 2) { // true transition in automaton - - if (new_pair) - MC_replay_liveness(mc_stack, 1); - - MC_SET_MC_HEAP; - - next_pair = MC_pair_new(); - next_pair->graph_state = MC_state_new(); - next_pair->automaton_state = transition_succ->dst; - next_pair->atomic_propositions = get_atomic_propositions_values(); - - /* Get enabled process and insert it in the interleave set of the next graph_state */ - xbt_swag_foreach(process, simix_global->process_list) { - if (MC_process_is_enabled(process)) { - MC_state_interleave_process(next_pair->graph_state, process); - } - } - - next_pair->requests = - MC_state_interleave_size(next_pair->graph_state); - - if (next_pair->automaton_state->type == 1 - || next_pair->automaton_state->type == 2 - || current_pair->search_cycle) - next_pair->search_cycle = 1; - - xbt_fifo_unshift(mc_stack, next_pair); - - if (mc_stats->expanded_pairs % 1000000 == 0) - XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs); - - MC_SET_STD_HEAP; - - new_pair = 1; - - MC_modelcheck_liveness(); - - } - - } - - if (MC_state_interleave_size(current_pair->graph_state) > 0) { - XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack)); - MC_replay_liveness(mc_stack, 0); - } + } + cursor--; + } + + MC_SET_STD_HEAP; + + } /* End of visited_pair test */ + + } else { + backtracking: + if(visited_num == -1) + XBT_DEBUG("No more request to execute. Looking for backtracking point."); + + MC_SET_MC_HEAP; + + xbt_dynar_free(&prop_values); + + /* Traverse the stack backwards until a pair with a non empty interleave + set is found, deleting all the pairs that have it empty in the way. */ + while ((current_pair = xbt_fifo_shift(mc_stack)) != NULL) { + if (current_pair->requests > 0) { + /* We found a backtracking point */ + XBT_DEBUG("Backtracking to depth %d", current_pair->depth); + xbt_fifo_unshift(mc_stack, current_pair); + MC_SET_STD_HEAP; + MC_replay_liveness(mc_stack); + XBT_DEBUG("Backtracking done"); + break; + }else{ + /* Delete pair */ + XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth); + if (current_pair->automaton_state->type == 1) + remove_acceptance_pair(current_pair->num); + MC_pair_delete(current_pair); } - } - - } - - } else { - - XBT_WARN("/!\\ Max depth reached ! /!\\ "); - if (MC_state_interleave_size(current_pair->graph_state) > 0) { - XBT_WARN - ("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); - if (_sg_mc_max_depth == 1000) - XBT_WARN - ("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value."); - } - - } - - if (xbt_fifo_size(mc_stack) == _sg_mc_max_depth) { - XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached", - current_pair->num, xbt_fifo_size(mc_stack)); - } else { - XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num, - xbt_fifo_size(mc_stack)); - } - - - MC_SET_MC_HEAP; - xbt_dynar_free(&prop_values); - current_pair = xbt_fifo_shift(mc_stack); - if (xbt_fifo_size(mc_stack) != _sg_mc_max_depth - 1 - && current_pair->requests > 0 && current_pair->search_cycle) { - remove_acceptance_pair(current_pair->num); - } - MC_pair_delete(current_pair); - - MC_SET_STD_HEAP; - + + MC_SET_STD_HEAP; + } /* End of if (current_pair->requests > 0) else ... */ + + } /* End of while(xbt_fifo_size(mc_stack) > 0) */ + } diff --combined src/mc/mc_private.h index f6087c6678,4a86245aeb..bcc454fce1 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@@ -7,8 -7,6 +7,8 @@@ #ifndef MC_PRIVATE_H #define MC_PRIVATE_H +#include + #include "simgrid_config.h" #include #include @@@ -23,7 -21,6 +23,7 @@@ #include "mc/datatypes.h" #include "xbt/fifo.h" #include "xbt/config.h" + #include "xbt/function_types.h" #include "xbt/mmalloc.h" #include "../simix/smx_private.h" @@@ -41,15 -38,12 +41,15 @@@ SG_BEGIN_DECL( typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function_index_item_t; -/****************************** Snapshots ***********************************/ - -extern xbt_dynar_t mc_checkpoint_ignore; - /********************************* MC Global **********************************/ +/** Initialisation of the model-checker + * + * @param pid PID of the target process + * @param socket FD for the communication socket **in server mode** (or -1 otherwise) + */ +void MC_init_pid(pid_t pid, int socket); + extern FILE *dot_output; extern const char* colors[13]; extern xbt_parmap_t parmap; @@@ -57,8 -51,8 +57,8 @@@ extern int user_max_depth_reached; int MC_deadlock_check(void); - void MC_replay(xbt_fifo_t stack, int start); - void MC_replay_liveness(xbt_fifo_t stack, int all_stack); + void MC_replay(xbt_fifo_t stack); + void MC_replay_liveness(xbt_fifo_t stack); void MC_show_deadlock(smx_simcall_t req); void MC_show_stack_safety(xbt_fifo_t stack); void MC_dump_stack_safety(xbt_fifo_t stack); @@@ -88,13 -82,16 +88,13 @@@ extern mc_stats_t mc_stats void MC_print_statistics(mc_stats_t stats); -extern char *libsimgrid_path; - /********************************** Snapshot comparison **********************************/ typedef struct s_mc_comparison_times{ double nb_processes_comparison_time; double bytes_used_comparison_time; double stacks_sizes_comparison_time; - double binary_global_variables_comparison_time; - double libsimgrid_global_variables_comparison_time; + double global_variables_comparison_time; double heap_comparison_time; double stacks_comparison_time; }s_mc_comparison_times_t, *mc_comparison_times_t; @@@ -110,6 -107,9 +110,6 @@@ void print_comparison_times(void) /********************************** Variables with DWARF **********************************/ -dw_frame_t MC_find_function_by_ip(void* ip); -mc_object_info_t MC_ip_find_object_info(void* ip); - void MC_find_object_address(memory_map_t maps, mc_object_info_t result); /********************************** Miscellaneous **********************************/ @@@ -141,15 -141,6 +141,6 @@@ bool mc_address_test(mc_address_set_t p * */ uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks); - /* *********** Snapshot *********** */ - - #define MC_LOG_REQUEST(log, req, value) \ - if (XBT_LOG_ISENABLED(log, xbt_log_priority_debug)) { \ - char* req_str = MC_request_to_string(req, value); \ - XBT_DEBUG("Execute: %s", req_str); \ - xbt_free(req_str); \ - } - /** @brief Dump the stacks of the application processes * * This functions is currently not used but it is quite convenient diff --combined src/mc/mc_safety.c index 3898df5dff,83460ff5da..3d0fc9e41b --- a/src/mc/mc_safety.c +++ b/src/mc/mc_safety.c @@@ -15,24 -15,23 +15,18 @@@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, "Logging specific to MC safety verification "); - xbt_dict_t first_enabled_state; - /** * \brief Initialize the DPOR exploration algorithm */ void MC_pre_modelcheck_safety() { - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - mc_state_t initial_state = NULL; smx_process_t process; - /* Create the initial state and push it into the exploration stack */ - if (!mc_mem_set) - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); if (_sg_mc_visited > 0) - visited_states = - xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); - - if (mc_reduce_kind == e_mc_reduce_dpor) - first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f); + visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); initial_state = MC_state_new(); @@@ -56,22 -55,9 +50,7 @@@ } xbt_fifo_unshift(mc_stack, initial_state); -- - if (mc_reduce_kind == e_mc_reduce_dpor) { - /* To ensure the soundness of DPOR, we have to keep a list of - processes which are still enabled at each step of the exploration. - If max depth is reached, we interleave them in the state in which they have - been enabled for the first time. */ - xbt_swag_foreach(process, simix_global->process_list) { - if (MC_process_is_enabled(process)) { - char *key = bprintf("%lu", process->pid); - char *data = bprintf("%d", xbt_fifo_size(mc_stack)); - xbt_dict_set(first_enabled_state, key, data, NULL); - xbt_free(key); - } - } - } - if (!mc_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); } @@@ -84,27 -70,21 +63,21 @@@ void MC_modelcheck_safety(void char *req_str = NULL; int value; smx_simcall_t req = NULL, prev_req = NULL; - mc_state_t state = NULL, prev_state = NULL, next_state = - NULL, restored_state = NULL; + mc_state_t state = NULL, prev_state = NULL, next_state = NULL; smx_process_t process = NULL; xbt_fifo_item_t item = NULL; - mc_state_t state_test = NULL; - int pos; mc_visited_state_t visited_state = NULL; - int enabled = 0; while (xbt_fifo_size(mc_stack) > 0) { /* Get current state */ - state = (mc_state_t) - xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); + state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); XBT_DEBUG("**************************************************"); XBT_DEBUG - ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)", + ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)", xbt_fifo_size(mc_stack), state, state->num, - MC_state_interleave_size(state), user_max_depth_reached, - xbt_dict_size(first_enabled_state)); + MC_state_interleave_size(state), user_max_depth_reached); /* Update statistics */ mc_stats->visited_states++; @@@ -114,7 -94,9 +87,9 @@@ if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached && (req = MC_state_get_request(state, &value)) && visited_state == NULL) { - MC_LOG_REQUEST(mc_safety, req, value); + char* req_str = MC_request_to_string(req, value); + XBT_DEBUG("Execute: %s", req_str); + xbt_free(req_str); if (dot_output != NULL) { MC_SET_MC_HEAP; @@@ -125,14 -107,6 +100,6 @@@ MC_state_set_executed_request(state, req, value); mc_stats->executed_transitions++; - if (mc_reduce_kind == e_mc_reduce_dpor) { - MC_SET_MC_HEAP; - char *key = bprintf("%lu", req->issuer->pid); - xbt_dict_remove(first_enabled_state, key); - xbt_free(key); - MC_SET_STD_HEAP; - } - /* Answer the request */ SIMIX_simcall_handle(req, value); @@@ -144,7 -118,7 +111,7 @@@ next_state = MC_state_new(); - if ((visited_state = is_visited_state()) == NULL) { + if ((visited_state = is_visited_state(next_state)) == NULL) { /* Get an enabled process and insert it in the interleave set of the next state */ xbt_swag_foreach(process, simix_global->process_list) { @@@ -155,39 -129,18 +122,18 @@@ } } - if (_sg_mc_checkpoint - && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) { - next_state->system_state = MC_take_snapshot(next_state->num); - } - if (dot_output != NULL) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, - next_state->num, req_str); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str); } else { if (dot_output != NULL) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, - visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); } xbt_fifo_unshift(mc_stack, next_state); - if (mc_reduce_kind == e_mc_reduce_dpor) { - /* Insert in dict all enabled processes, if not included yet */ - xbt_swag_foreach(process, simix_global->process_list) { - if (MC_process_is_enabled(process)) { - char *key = bprintf("%lu", process->pid); - if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) { - char *data = bprintf("%d", xbt_fifo_size(mc_stack)); - xbt_dict_set(first_enabled_state, key, data, NULL); - } - xbt_free(key); - } - } - } - if (dot_output != NULL) xbt_free(req_str); @@@ -198,8 -151,7 +144,7 @@@ /* The interleave set is empty or the maximum depth is reached, let's back-track */ } else { - if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached - || visited_state != NULL) { + if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) { if (user_max_depth_reached && visited_state == NULL) XBT_DEBUG("User max depth reached !"); @@@ -208,35 -160,9 +153,9 @@@ else XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num); - if (mc_reduce_kind == e_mc_reduce_dpor) { - /* Interleave enabled processes in the state in which they have been enabled for the first time */ - xbt_swag_foreach(process, simix_global->process_list) { - if (MC_process_is_enabled(process)) { - char *key = bprintf("%lu", process->pid); - enabled = - (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key), - 0, 10); - xbt_free(key); - int cursor = xbt_fifo_size(mc_stack); - xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) { - if (cursor-- == enabled) { - if (!MC_state_process_is_done(state_test, process) - && state_test->num != state->num) { - XBT_DEBUG("Interleave process %lu in state %d", - process->pid, state_test->num); - MC_state_interleave_process(state_test, process); - break; - } - } - } - } - } - } - } else { - XBT_DEBUG("There are no more processes to interleave. (depth %d)", - xbt_fifo_size(mc_stack) + 1); + XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1); } @@@ -244,9 -170,8 +163,8 @@@ /* Trash the current state, no longer needed */ xbt_fifo_shift(mc_stack); - MC_state_delete(state); - XBT_DEBUG("Delete state %d at depth %d", state->num, - xbt_fifo_size(mc_stack) + 1); + MC_state_delete(state, !state->in_visited_states ? 1 : 0); + XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1); MC_SET_STD_HEAP; @@@ -270,8 -195,7 +188,7 @@@ if (mc_reduce_kind == e_mc_reduce_dpor) { req = MC_state_get_internal_request(state); xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) { - if (MC_request_depend - (req, MC_state_get_internal_request(prev_state))) { + if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { XBT_DEBUG("Dependent Transitions:"); prev_req = MC_state_get_executed_request(prev_state, &value); @@@ -291,65 -215,33 +208,33 @@@ break; - } else if (req->issuer == - MC_state_get_internal_request(prev_state)->issuer) { + } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) { - XBT_DEBUG("Simcall %d and %d with same issuer", req->call, - MC_state_get_internal_request(prev_state)->call); + XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call); break; } else { - XBT_DEBUG - ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", - req->call, req->issuer->pid, state->num, - MC_state_get_internal_request(prev_state)->call, - MC_state_get_internal_request(prev_state)->issuer->pid, - prev_state->num); + XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", + req->call, req->issuer->pid, state->num, + MC_state_get_internal_request(prev_state)->call, + MC_state_get_internal_request(prev_state)->issuer->pid, + prev_state->num); } } } - if (MC_state_interleave_size(state) - && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) { + if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ - XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, - xbt_fifo_size(mc_stack) + 1); - if (_sg_mc_checkpoint) { - if (state->system_state != NULL) { - MC_restore_snapshot(state->system_state); - xbt_fifo_unshift(mc_stack, state); - MC_SET_STD_HEAP; - } else { - pos = xbt_fifo_size(mc_stack); - item = xbt_fifo_get_first_item(mc_stack); - while (pos > 0) { - restored_state = (mc_state_t) xbt_fifo_get_item_content(item); - if (restored_state->system_state != NULL) { - break; - } else { - item = xbt_fifo_get_next_item(item); - pos--; - } - } - MC_restore_snapshot(restored_state->system_state); - xbt_fifo_unshift(mc_stack, state); - MC_SET_STD_HEAP; - MC_replay(mc_stack, pos); - } - } else { - xbt_fifo_unshift(mc_stack, state); - MC_SET_STD_HEAP; - MC_replay(mc_stack, -1); - } - XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, - xbt_fifo_size(mc_stack)); + XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1); + xbt_fifo_unshift(mc_stack, state); + MC_replay(mc_stack); + XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack)); break; } else { - XBT_DEBUG("Delete state %d at depth %d", state->num, - xbt_fifo_size(mc_stack) + 1); - MC_state_delete(state); + XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1); + MC_state_delete(state, !state->in_visited_states ? 1 : 0); } } MC_SET_STD_HEAP; diff --combined src/mc/mc_visited.c index 8010fde06d,f792c80b1e..77548d8330 --- a/src/mc/mc_visited.c +++ b/src/mc/mc_visited.c @@@ -18,10 -18,24 +18,24 @@@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visi xbt_dynar_t visited_pairs; xbt_dynar_t visited_states; + static int is_exploration_stack_state(mc_visited_state_t state){ + xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack); + while (item) { + if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){ + ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0; + return 1; + } + item = xbt_fifo_get_next_item(item); + } + return 0; + } + void visited_state_free(mc_visited_state_t state) { if (state) { - MC_free_snapshot(state->system_state); + if(!is_exploration_stack_state(state)){ + MC_free_snapshot(state->system_state); + } xbt_free(state); } } @@@ -37,12 -51,9 +51,12 @@@ void visited_state_free_voidp(void *s */ static mc_visited_state_t visited_state_new() { + mc_process_t process = &(mc_model_checker->process); mc_visited_state_t new_state = NULL; new_state = xbt_new0(s_mc_visited_state_t, 1); - new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap); + new_state->heap_bytes_used = mmalloc_get_bytes_used_remote( + MC_process_get_heap(process)->heaplimit, + MC_process_get_malloc_info(process)); new_state->nb_processes = xbt_swag_size(simix_global->process_list); new_state->system_state = MC_take_snapshot(mc_stats->expanded_states); new_state->num = mc_stats->expanded_states; @@@ -50,19 -61,14 +64,17 @@@ return new_state; } - - mc_visited_pair_t MC_visited_pair_new(int pair_num, - xbt_automaton_state_t automaton_state, - xbt_dynar_t atomic_propositions) + mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state) { + mc_process_t process = &(mc_model_checker->process); mc_visited_pair_t pair = NULL; pair = xbt_new0(s_mc_visited_pair_t, 1); - pair->graph_state = MC_state_new(); - pair->graph_state->system_state = MC_take_snapshot(pair_num); + pair->graph_state = graph_state; + if(pair->graph_state->system_state == NULL) + pair->graph_state->system_state = MC_take_snapshot(pair_num); - pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap); + pair->heap_bytes_used = mmalloc_get_bytes_used_remote( + MC_process_get_heap(process)->heaplimit, + MC_process_get_malloc_info(process)); pair->nb_processes = xbt_swag_size(simix_global->process_list); pair->automaton_state = automaton_state; pair->num = pair_num; @@@ -78,10 -84,23 +90,23 @@@ return pair; } + static int is_exploration_stack_pair(mc_visited_pair_t pair){ + xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack); + while (item) { + if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){ + ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1; + return 1; + } + item = xbt_fifo_get_next_item(item); + } + return 0; + } + void MC_visited_pair_delete(mc_visited_pair_t p) { p->automaton_state = NULL; - MC_state_delete(p->graph_state); + if( !is_exploration_stack_pair(p)) + MC_state_delete(p->graph_state, 1); xbt_dynar_free(&(p->atomic_propositions)); xbt_free(p); p = NULL; @@@ -106,7 -125,9 +131,7 @@@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) { - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); int cursor = 0, previous_cursor, next_cursor; int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test; @@@ -126,14 -147,11 +151,11 @@@ while (start <= end) { cursor = (start + end) / 2; if (_sg_mc_liveness) { - ref_test = - (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t); + ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t); nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes; heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used; } else { - ref_test = - (mc_visited_state_t) xbt_dynar_get_as(list, cursor, - mc_visited_state_t); + ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t); nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; } @@@ -151,22 -169,15 +173,15 @@@ previous_cursor = cursor - 1; while (previous_cursor >= 0) { if (_sg_mc_liveness) { - ref_test = - (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, - mc_visited_pair_t); + ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t); nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes; - heap_bytes_used_test = - ((mc_visited_pair_t) ref_test)->heap_bytes_used; + heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used; } else { - ref_test = - (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, - mc_visited_state_t); + ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t); nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; - heap_bytes_used_test = - ((mc_visited_state_t) ref_test)->heap_bytes_used; + heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; } - if (nb_processes_test != nb_processes - || heap_bytes_used_test != heap_bytes_used) + if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used) break; *min = previous_cursor; previous_cursor--; @@@ -174,33 -185,29 +189,26 @@@ next_cursor = cursor + 1; while (next_cursor < xbt_dynar_length(list)) { if (_sg_mc_liveness) { - ref_test = - (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, - mc_visited_pair_t); + ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t); nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes; - heap_bytes_used_test = - ((mc_visited_pair_t) ref_test)->heap_bytes_used; + heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used; } else { - ref_test = - (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, - mc_visited_state_t); + ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t); nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; - heap_bytes_used_test = - ((mc_visited_state_t) ref_test)->heap_bytes_used; + heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; } - if (nb_processes_test != nb_processes - || heap_bytes_used_test != heap_bytes_used) + if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used) break; *max = next_cursor; next_cursor++; } - if (!mc_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); return -1; } } } - if (!mc_mem_set) - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); return cursor; } @@@ -209,32 -216,45 +217,40 @@@ * \brief Checks whether a given state has already been visited by the algorithm. */ - mc_visited_state_t is_visited_state() + mc_visited_state_t is_visited_state(mc_state_t graph_state) { if (_sg_mc_visited == 0) return NULL; + int partial_comm = 0; + /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at least, data are transfered). These communications - are incomplete and they cannot be analyzed and compared with the initial pattern */ + are incomplete and they cannot be analyzed and compared with the initial pattern. */ if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { int current_process = 1; while (current_process < simix_process_maxpid) { - if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))) - return NULL; + if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){ + XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited."); + partial_comm = 1; + break; + } current_process++; } } - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); mc_visited_state_t new_state = visited_state_new(); + graph_state->system_state = new_state->system_state; + graph_state->in_visited_states = 1; + XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num); if (xbt_dynar_is_empty(visited_states)) { xbt_dynar_push(visited_states, &new_state); - - if (!mc_mem_set) - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); return NULL; } else { @@@ -267,47 -287,45 +283,44 @@@ return new_state->other_num; } */ - cursor = min; - while (cursor <= max) { - state_test = - (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, - mc_visited_state_t); - if (snapshot_compare(state_test, new_state) == 0) { - // The state has been visited: - - if (state_test->other_num == -1) - new_state->other_num = state_test->num; - else - new_state->other_num = state_test->other_num; - if (dot_output == NULL) - XBT_DEBUG("State %d already visited ! (equal to state %d)", - new_state->num, state_test->num); - else - XBT_DEBUG - ("State %d already visited ! (equal to state %d (state %d in dot_output))", - new_state->num, state_test->num, new_state->other_num); - - /* Replace the old state with the new one (with a bigger num) - (when the max number of visited states is reached, the oldest - one is removed according to its number (= with the min number) */ - xbt_dynar_remove_at(visited_states, cursor, NULL); - xbt_dynar_insert_at(visited_states, cursor, &new_state); - - mmalloc_set_current_heap(heap); - return state_test; + if(!partial_comm && initial_global_state->initial_communications_pattern_done){ + + cursor = min; + while (cursor <= max) { + state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t); + if (snapshot_compare(state_test, new_state) == 0) { + // The state has been visited: + + if (state_test->other_num == -1) + new_state->other_num = state_test->num; + else + new_state->other_num = state_test->other_num; + if (dot_output == NULL) + XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num); + else + XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num); + + /* Replace the old state with the new one (with a bigger num) + (when the max number of visited states is reached, the oldest + one is removed according to its number (= with the min number) */ + xbt_dynar_remove_at(visited_states, cursor, NULL); + xbt_dynar_insert_at(visited_states, cursor, &new_state); + XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num); + - if (!mc_mem_set) - MC_SET_STD_HEAP; ++ mmalloc_set_current_heap(heap); + return state_test; + } + cursor++; } - cursor++; } - - // The state has not been visited: insert the state in the dynamic array. + xbt_dynar_insert_at(visited_states, min, &new_state); - + XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states)); + } else { // The state has not been visited: insert the state in the dynamic array. - state_test = - (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, - mc_visited_state_t); + state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t); if (state_test->nb_processes < new_state->nb_processes) { xbt_dynar_insert_at(visited_states, index + 1, &new_state); } else { @@@ -317,11 -335,15 +330,15 @@@ xbt_dynar_insert_at(visited_states, index, &new_state); } + XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states)); + } // We have reached the maximum number of stored states; if (xbt_dynar_length(visited_states) > _sg_mc_visited) { + XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)"); + // Find the (index of the) older state (with the smallest num): int min2 = mc_stats->expanded_states; unsigned int cursor2 = 0; @@@ -335,38 -357,40 +352,35 @@@ // and drop it: xbt_dynar_remove_at(visited_states, index2, NULL); + XBT_DEBUG("Remove visited state (maximum number of stored states reached)"); } - if (!mc_mem_set) - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); return NULL; - } } /** * \brief Checks whether a given pair has already been visited by the algorithm. */ - int is_visited_pair(mc_visited_pair_t pair, int pair_num, - xbt_automaton_state_t automaton_state, - xbt_dynar_t atomic_propositions) - { + int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) { if (_sg_mc_visited == 0) return -1; - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - mc_visited_pair_t new_pair = NULL; + mc_visited_pair_t new_visited_pair = NULL; - if (pair == NULL) { - new_pair = - MC_visited_pair_new(pair_num, automaton_state, atomic_propositions); + if (visited_pair == NULL) { + new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); } else { - new_pair = pair; + new_visited_pair = visited_pair; } if (xbt_dynar_is_empty(visited_pairs)) { - xbt_dynar_push(visited_pairs, &new_pair); + xbt_dynar_push(visited_pairs, &new_visited_pair); } else { @@@ -375,7 -399,7 +389,7 @@@ mc_visited_pair_t pair_test; int cursor; - index = get_search_interval(visited_pairs, new_pair, &min, &max); + index = get_search_interval(visited_pairs, new_visited_pair, &min, &max); if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair); @@@ -407,28 -431,20 +421,20 @@@ } */ cursor = min; while (cursor <= max) { - pair_test = - (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, - mc_visited_pair_t); - if (xbt_automaton_state_compare - (pair_test->automaton_state, new_pair->automaton_state) == 0) { - if (xbt_automaton_propositional_symbols_compare_value - (pair_test->atomic_propositions, - new_pair->atomic_propositions) == 0) { - if (snapshot_compare(pair_test, new_pair) == 0) { + pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t); + if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) { + if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) { + if (snapshot_compare(pair_test, new_visited_pair) == 0) { if (pair_test->other_num == -1) - new_pair->other_num = pair_test->num; + new_visited_pair->other_num = pair_test->num; else - new_pair->other_num = pair_test->other_num; + new_visited_pair->other_num = pair_test->other_num; if (dot_output == NULL) - XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", - new_pair->num, pair_test->num); + XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num); else - XBT_DEBUG - ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", - new_pair->num, pair_test->num, new_pair->other_num); - xbt_dynar_remove_at(visited_pairs, cursor, NULL); - xbt_dynar_insert_at(visited_pairs, cursor, &new_pair); + XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num); + xbt_dynar_remove_at(visited_pairs, cursor, &pair_test); + xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair); pair_test->visited_removed = 1; if (pair_test->acceptance_pair) { if (pair_test->acceptance_removed == 1) @@@ -436,25 -452,24 +442,23 @@@ } else { MC_visited_pair_delete(pair_test); } - if (!mc_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); - return new_pair->other_num; + return new_visited_pair->other_num; } } } cursor++; } - xbt_dynar_insert_at(visited_pairs, min, &new_pair); + xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair); } else { - pair_test = - (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, - mc_visited_pair_t); - if (pair_test->nb_processes < new_pair->nb_processes) { - xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair); + pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t); + if (pair_test->nb_processes < new_visited_pair->nb_processes) { + xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair); } else { - if (pair_test->heap_bytes_used < new_pair->heap_bytes_used) - xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair); + if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used) + xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair); else - xbt_dynar_insert_at(visited_pairs, index, &new_pair); + xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair); } } @@@ -480,6 -495,8 +484,6 @@@ } - if (!mc_mem_set) - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); return -1; } diff --combined src/simix/smx_global.c index d568b5ae78,ecd64f0502..29474e8500 --- a/src/simix/smx_global.c +++ b/src/simix/smx_global.c @@@ -4,8 -4,6 +4,8 @@@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ +#include + #include "smx_private.h" #include "xbt/heap.h" #include "xbt/sysdep.h" @@@ -17,9 -15,6 +17,9 @@@ #ifdef HAVE_MC #include "mc/mc_private.h" +#include "mc/mc_model_checker.h" +#include "mc/mc_protocol.h" +#include "mc/mc_client.h" #endif #include "mc/mc_record.h" @@@ -211,20 -206,6 +211,20 @@@ void SIMIX_global_init(int *argc, char if (sg_cfg_get_boolean("clean_atexit")) atexit(SIMIX_clean); +#ifdef HAVE_MC + // The communication initialisation is done ASAP. + // We need to commuicate initialisation of the different layers to the model-checker. + if (mc_mode == MC_MODE_NONE) { + if (getenv(MC_ENV_SOCKET_FD)) { + mc_mode = MC_MODE_CLIENT; + MC_client_init(); + MC_client_hello(); + } else { + mc_mode = MC_MODE_STANDALONE; + } + } +#endif + if (_sg_cfg_exit_asap) exit(0); } @@@ -360,7 -341,7 +360,7 @@@ void SIMIX_run(void xbt_os_cputimer_resume(simix_global->timer_seq); #endif - /* Move all killing processes to the end of the list, because killing a process that have an ongoing simcall is a bad idea */ + /* Move all killer processes to the end of the list, because killing a process that have an ongoing simcall is a bad idea */ xbt_dynar_three_way_partition(simix_global->process_that_ran, process_syscall_color); /* answer sequentially and in a fixed arbitrary order all the simcalls that were issued during that sub-round */ diff --combined src/smpi/smpi_bench.c index 7028ea3960,26f7c542ee..7507e90939 --- a/src/smpi/smpi_bench.c +++ b/src/smpi/smpi_bench.c @@@ -638,7 -638,6 +638,7 @@@ void smpi_really_switch_data_segment(in } } + // FIXME, cross-process support (mmap across process when necessary) int current = smpi_privatisation_regions[dest].file_descriptor; XBT_DEBUG("Switching data frame to the one of process %d", dest); void* tmp = mmap (TOPAGE(start_data_exe), size_data_exe, PROT_READ | PROT_WRITE, MAP_FIXED | MAP_SHARED, current, 0); @@@ -754,8 -753,25 +754,25 @@@ void smpi_initialize_global_memory_segm int status; int file_descriptor= mkstemp (path); - if (file_descriptor < 0) - xbt_die("Impossible to create temporary file for memory mapping"); + if (file_descriptor < 0) { + if (errno==EMFILE) { + xbt_die("Impossible to create temporary file for memory mapping: %s\n\ + The open() system call failed with the EMFILE error code (too many files). \n\n\ + This means that you reached the system limits concerning the amount of files per process. \ + This is not a surprise if you are trying to virtualize many processes on top of SMPI. \ + Don't panic -- you should simply increase your system limits and try again. \n\n\ + First, check what your limits are:\n\ + cat /proc/sys/fs/file-max # Gives you the system-wide limit\n\ + ulimit -Hn # Gives you the per process hard limit\n\ + ulimit -Sn # Gives you the per process soft limit\n\ + cat /proc/self/limits # Displays any per-process limitation (including the one given above)\n\n\ + If one of these values is less than the amount of MPI processes that you try to run, then you got the explanation of this error. \ + Ask the Internet about tutorials on how to increase the files limit such as: https://rtcamp.com/tutorials/linux/increase-open-files-limit/", + strerror(errno)); + } + xbt_die("Impossible to create temporary file for memory mapping: %s", + strerror(errno)); + } status = unlink (path); if (status)