[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 6ce5570..3cc7e2d 100644 (file)
--- 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 ef112fa..e6267e2 100644 (file)
--- 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 4b9cf04..5c5fb92 100644 (file)
--- 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 d7f46a1..ceb77db 100644 (file)
--- 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 a33d00e..251e184 100644 (file)
--- 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 c9dc25f..12ca0a8 100644 (file)
--- 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 b9308e6..a961720 100644 (file)
--- 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*/