! 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
> [ 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:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> [ 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
+
! 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
> [ 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:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> [ 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
! 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
> [ 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:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> [ 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
+
! 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
> [ 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:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> [ 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
* under the terms of the license (GNU LGPL) which comes with this package. */
#define _GNU_SOURCE
-#define UNW_LOCAL_ONLY
#include <unistd.h>
#include "../simix/smx_private.h"
-#define UNW_LOCAL_ONLY
#include <libunwind.h>
#include <libelf.h>
#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 **************************************/
/*****************************************************************************************/
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)
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
* @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);
* @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);
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);
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;
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;
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),
}
}
-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");
// 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) {
&& !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");
}
}
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;
}
+// FIXME, cross-process support (mc_heap_comparison_ignore)
static xbt_dynar_t MC_take_snapshot_ignore()
{
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);
}
}
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);
}
}
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");
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;
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;
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();
}
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
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);
};
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();
-}
xbt_dynar_t initial_communications_pattern;
xbt_dynar_t incomplete_communications_pattern;
- xbt_dynar_t communications_pattern;
- int nb_comm_pattern;
/********** Static functions ***********/
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;
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; i<simix_process_maxpid; i++){
- xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
- xbt_dynar_insert_at(initial_communications_pattern, i, &process_pattern);
- }
- communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
+ initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), list_comm_pattern_free_voidp);
for (i=0; i<simix_process_maxpid; i++){
- xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
- xbt_dynar_insert_at(communications_pattern, i, &process_pattern);
+ mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1);
+ process_list_pattern->list = 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<simix_process_maxpid; i++){
- xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(int), NULL);
+ xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), NULL);
xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
}
- nb_comm_pattern = 0;
-
initial_state = MC_state_new();
-
MC_SET_STD_HEAP;
-
+
XBT_DEBUG("********* Start communication determinism verification *********");
/* Wait for requests (schedules processes) */
smx_simcall_t req = NULL;
smx_process_t process = NULL;
mc_state_t state = NULL, next_state = NULL;
- xbt_dynar_t current_pattern;
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 = %d, interleaved processes = %d)",
&& (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);
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);
}
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) */
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) {
}
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);
}
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;
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);
}
}
#define MC_FORWARD_H
#include <mc/datatypes.h>
+ #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;
/* 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 <string.h>
+
#include "mc_base.h"
#ifndef _XBT_WIN32
#include <unistd.h>
-#include <sys/types.h>
#include <sys/wait.h>
#include <sys/time.h>
-#include <sys/mman.h>
-#include <libgen.h>
#endif
#include "simgrid/sg_config.h"
#include "xbt/dict.h"
#ifdef HAVE_MC
-#define UNW_LOCAL_ONLY
#include <libunwind.h>
+#include <xbt/mmalloc.h>
#include "../xbt/mmalloc/mmprivate.h"
#include "mc_object_info.h"
#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
/* 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];
}
-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);
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();
/* 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");
/* 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();
+ }
}
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();
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();
MC_modelcheck_safety();
- if (mc_mem_set)
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(heap);
xbt_abort();
//MC_exit();
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();
MC_print_statistics(mc_stats);
xbt_free(mc_time);
- if (mc_mem_set)
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(heap);
}
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;
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)
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; i<simix_process_maxpid; i++){
+ initial_incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
+ xbt_dynar_reset(initial_incomplete_process_comms);
+ incomplete_process_comms = xbt_dynar_get_as(state->incomplete_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);
+ }
+ }
}
/**
* 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; j<simix_process_maxpid; j++) {
- xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(communications_pattern, j, xbt_dynar_t));
- }
for (j=0; j<simix_process_maxpid; j++) {
xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
+ ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t))->index_comm = 0;
}
}
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 */
}
/* 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 */
}
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);
/* 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)) {
mc_stats->executed_transitions++;
depth++;
-
+
}
XBT_DEBUG("**** End Replay ****");
*/
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;
}
}
- if (!raw_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
}
void MC_show_deadlock(smx_simcall_t req)
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);
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;
++nstack;
}
-
- if (raw_mem_set)
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(heap);
}
#endif
/********* 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 {
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
} */
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);
}
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;
}
}
}
- void MC_pre_modelcheck_liveness(void)
- {
+ void MC_pre_modelcheck_liveness(void) {
initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
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) {
}
}
- 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)) {
}
}
- 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) */
+
}
#ifndef MC_PRIVATE_H
#define MC_PRIVATE_H
+#include <sys/types.h>
+
#include "simgrid_config.h"
#include <stdio.h>
#include <stdint.h>
#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"
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;
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);
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;
/********************************** 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 **********************************/
* */
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
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();
}
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);
}
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++;
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;
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);
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) {
}
}
- 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);
/* 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 !");
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);
}
/* 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;
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);
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;
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);
}
}
*/
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;
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;
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;
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;
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;
}
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--;
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;
}
* \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 {
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 {
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;
// 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 {
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);
} */
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)
} 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);
}
}
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
return -1;
}
/* 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 <stdlib.h>
+
#include "smx_private.h"
#include "xbt/heap.h"
#include "xbt/sysdep.h"
#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"
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);
}
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 */
}
}
+ // 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);
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)
