From: Gabriel Corona Date: Tue, 10 Feb 2015 13:37:10 +0000 (+0100) Subject: [mc] Server side symbol evaluation X-Git-Tag: v3_12~732^2~122 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/38d1cfd08cf30b0da496b20dfa8b849cbfdb7ab4 [mc] Server side symbol evaluation This is currently only handled for symbols represented as variables (opposed to symbols represented as callbacks): in order to evaluate the callback we will have to ask the MCed to evaluate the callback for us and send us the result back. --- diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 6ce5570b04..3cc7e2d583 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -41,6 +41,9 @@ extern int _sg_mc_visited; XBT_PUBLIC(void) MC_assert(int); XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, int(*fct)(void)); XBT_PUBLIC(void) MC_automaton_new_propositional_symbol_pointer(const char *id, int* value); +XBT_PUBLIC(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_PUBLIC(void *) MC_snapshot(void); XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2); XBT_PUBLIC(void) MC_cut(void); @@ -54,6 +57,8 @@ XBT_PUBLIC(void) MC_ignore(void *addr, size_t size); #define MC_assert(a) xbt_assert(a) #define MC_automaton_new_propositional_symbol(a, b) ((void)0) #define MC_automaton_new_propositional_symbol_pointer(a, b) ((void)0) +#define MC_automaton_new_propositional_symbol_callback(id,callback,data,free_function) \ + if(free_function) free_function(data); #define MC_snapshot() ((void*)0) #define MC_compare_snapshots(a, b) 0 #define MC_cut() ((void)0) diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h index ef112fa2d0..e6267e243b 100644 --- a/include/xbt/automaton.h +++ b/include/xbt/automaton.h @@ -58,9 +58,10 @@ typedef struct xbt_automaton_transition* xbt_automaton_transition_t; typedef struct xbt_automaton_propositional_symbol s_xbt_automaton_propositional_symbol; - typedef struct xbt_automaton_propositional_symbol* xbt_automaton_propositional_symbol_t; +typedef int (*xbt_automaton_propositional_symbol_callback_type)(void*); +typedef void (*xbt_automaton_propositional_symbol_free_function_type)(void*); XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new(void); @@ -96,17 +97,21 @@ XBT_PUBLIC(void) xbt_automaton_display(xbt_automaton_t a); XBT_PUBLIC(void) xbt_automaton_exp_label_display(xbt_automaton_exp_label_t l); +// xbt_automaton_propositional_symbol constructors: XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, int(*fct)(void)); - XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_pointer(xbt_automaton_t a, const char* id, int* value); - XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_callback( xbt_automaton_t a, const char* id, - int(*callback)(void*), void* data, void (*free_function)(void*)); + xbt_automaton_propositional_symbol_callback_type callback, + void* data, xbt_automaton_propositional_symbol_free_function_type free_function); -XBT_PUBLIC(int) xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol); +// xbt_automaton_propositional_symbol accessors: +XBT_PUBLIC(xbt_automaton_propositional_symbol_callback_type) xbt_automaton_propositional_symbol_get_callback(xbt_automaton_propositional_symbol_t symbol); +XBT_PUBLIC(void*) xbt_automaton_propositional_symbol_get_data(xbt_automaton_propositional_symbol_t symbol); +XBT_PUBLIC(const char*) xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol); -char* xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol); +// xbt_automaton_propositional_symbol methods! +XBT_PUBLIC(int) xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol); XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_get_current_state(xbt_automaton_t a); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 4b9cf0429e..5c5fb92f92 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -699,6 +699,21 @@ void MC_automaton_load(const char *file) mmalloc_set_current_heap(heap); } +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)); +} + void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void)) { xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); @@ -706,7 +721,8 @@ void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void)) if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); - xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct); + xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct); + register_symbol(symbol); mmalloc_set_current_heap(heap); } @@ -715,7 +731,21 @@ 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_new_pointer(_mc_property_automaton, id, value); + 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); } diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index d7f46a1296..ceb77db24f 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -31,7 +31,6 @@ static xbt_dynar_t get_atomic_propositions_values() unsigned int cursor = 0; xbt_automaton_propositional_symbol_t ps = NULL; xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL); - // FIXME, cross-process support xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps) { int res = xbt_automaton_propositional_symbol_evaluate(ps); xbt_dynar_push_as(values, int, res); diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h index a33d00ec1c..251e1842b0 100644 --- a/src/mc/mc_protocol.h +++ b/src/mc/mc_protocol.h @@ -44,6 +44,7 @@ typedef enum { MC_MESSAGE_UNIGNORE_HEAP, MC_MESSAGE_IGNORE_MEMORY, MC_MESSAGE_STACK_REGION, + MC_MESSAGE_REGISTER_SYMBOL, } e_mc_message_type; #define MC_MESSAGE_LENGTH 512 @@ -80,6 +81,13 @@ typedef struct s_mc_stack_region_message { s_stack_region_t stack_region; } s_mc_stack_region_message_t, *mc_stack_region_message_t; +typedef struct s_mc_register_symbol_message { + e_mc_message_type type; + char name[128]; + int (*callback)(void*); + void* data; +} s_mc_register_symbol_message_t, * mc_register_symbol_message_t; + int MC_protocol_send(int socket, void* message, size_t size); int MC_protocol_send_simple_message(int socket, int type); int MC_protocol_hello(int socket); diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index c9dc25f939..12ca0a89a3 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -29,6 +29,21 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic"); mc_server_t mc_server; +struct mc_symbol_pointer_callback +{ + mc_process_t process; + void* value; +}; + +static int mc_symbol_pointer_callback_evaluate(void* p) +{ + struct mc_symbol_pointer_callback* callback = (struct mc_symbol_pointer_callback*) p; + int value; + MC_process_read(callback->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE, + &value, callback->value, sizeof(value), MC_PROCESS_INDEX_ANY); + return value; +} + s_mc_server::s_mc_server(pid_t pid, int socket) { this->pid = pid; @@ -202,6 +217,25 @@ void s_mc_server::handle_events() } break; + case MC_MESSAGE_REGISTER_SYMBOL: + { + s_mc_register_symbol_message_t message; + if (size != sizeof(message)) + xbt_die("Broken message"); + memcpy(&message, buffer, sizeof(message)); + if (message.callback) + xbt_die("Support for callbacks/functions symbols not implemented in client/server mode."); + XBT_DEBUG("Received symbol: %s", message.name); + + struct mc_symbol_pointer_callback* callback = xbt_new(struct mc_symbol_pointer_callback, 1); + callback->process = &mc_model_checker->process; + callback->value = message.data; + + MC_automaton_new_propositional_symbol_callback(message.name, + mc_symbol_pointer_callback_evaluate, callback, free); + break; + } + default: xbt_die("Unexpected message from model-checked application"); diff --git a/src/xbt/automaton/automaton.c b/src/xbt/automaton/automaton.c index b9308e63d7..a961720fde 100644 --- a/src/xbt/automaton/automaton.c +++ b/src/xbt/automaton/automaton.c @@ -12,7 +12,7 @@ struct xbt_automaton_propositional_symbol{ char* pred; /** Callback used to evaluate the value of the symbol */ - int (*function)(void*); + int (*callback)(void*); /** Additional data for the callback. Alternatively it can be used as a pointer to the data. */ void* data; @@ -20,19 +20,6 @@ struct xbt_automaton_propositional_symbol{ void (*free_function)(void*); }; -int xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol) -{ - if (symbol->function) - return (symbol->function)(symbol->data); - else - return *(int*) symbol->data; -} - -char* xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol) -{ - return symbol->pred; -} - xbt_automaton_t xbt_automaton_new(){ xbt_automaton_t automaton = NULL; automaton = xbt_new0(struct xbt_automaton, 1); @@ -230,7 +217,7 @@ xbt_automaton_propositional_symbol_t xbt_automaton_propositional_symbol_new(xbt_ xbt_automaton_propositional_symbol_t prop_symb = NULL; prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1); prop_symb->pred = strdup(id); - prop_symb->function = call_simple_function; + prop_symb->callback = call_simple_function; prop_symb->data = fct; prop_symb->free_function = NULL; xbt_dynar_push(a->propositional_symbols, &prop_symb); @@ -242,7 +229,7 @@ XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_sym xbt_automaton_propositional_symbol_t prop_symb = NULL; prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1); prop_symb->pred = strdup(id); - prop_symb->function = NULL; + prop_symb->callback = NULL; prop_symb->data = value; prop_symb->free_function = NULL; xbt_dynar_push(a->propositional_symbols, &prop_symb); @@ -251,18 +238,42 @@ XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_sym XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_callback( xbt_automaton_t a, const char* id, - int(*callback)(void*), void* data, void (*free_function)(void*)) + xbt_automaton_propositional_symbol_callback_type callback, + void* data, xbt_automaton_propositional_symbol_free_function_type free_function) { xbt_automaton_propositional_symbol_t prop_symb = NULL; prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1); prop_symb->pred = strdup(id); - prop_symb->function = callback; + prop_symb->callback = callback; prop_symb->data = data; prop_symb->free_function = free_function; xbt_dynar_push(a->propositional_symbols, &prop_symb); return prop_symb; } +XBT_PUBLIC(int) xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol) +{ + if (symbol->callback) + return (symbol->callback)(symbol->data); + else + return *(int*) symbol->data; +} + +XBT_PUBLIC(xbt_automaton_propositional_symbol_callback_type) xbt_automaton_propositional_symbol_get_callback(xbt_automaton_propositional_symbol_t symbol) +{ + return symbol->callback; +} + +XBT_PUBLIC(void*) xbt_automaton_propositional_symbol_get_data(xbt_automaton_propositional_symbol_t symbol) +{ + return symbol->data; +} + +XBT_PUBLIC(const char*) xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol) +{ + return symbol->pred; +} + int xbt_automaton_state_compare(xbt_automaton_state_t s1, xbt_automaton_state_t s2){ /* single id for each state, id and type sufficient for comparison*/