examples/msg/mc/bugged2.c

   1 /******************** Non-deterministic message ordering  *********************/
   2 /* Server assumes a fixed order in the reception of messages from its clients */
   3 /* which is incorrect because the message ordering is non-deterministic       */
   4 /******************************************************************************/
   5
   6 #include <msg/msg.h>
   7 #include <mc/modelchecker.h>
   8 #define N 3
   9
  10 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");
  11
  12 int server(int argc, char *argv[]);
  13 int client(int argc, char *argv[]);
  14
  15 int server(int argc, char *argv[])
  16 {
  17   m_task_t task1, task2;
  18   long val1, val2;
  19
  20   MSG_task_receive(&task1, "mymailbox");
  21   val1 = (long) MSG_task_get_data(task1);
  22   MSG_task_destroy(task1);
  23   task1 = NULL;
  24   INFO1("Received %lu", val1);
  25
  26   MSG_task_receive(&task2, "mymailbox");
  27   val2 = (long) MSG_task_get_data(task2);
  28   MSG_task_destroy(task2);
  29   task2 = NULL;
  30   INFO1("Received %lu", val2);
  31
  32   MC_assert(min(val1, val2) == 1);
  33
  34   MSG_task_receive(&task1, "mymailbox");
  35   val1 = (long) MSG_task_get_data(task1);
  36   MSG_task_destroy(task1);
  37   INFO1("Received %lu", val1);
  38
  39   MSG_task_receive(&task2, "mymailbox");
  40   val2 = (long) MSG_task_get_data(task2);
  41   MSG_task_destroy(task2);
  42   INFO1("Received %lu", val2);
  43
  44   INFO0("OK");
  45   return 0;
  46 }
  47
  48 int client(int argc, char *argv[])
  49 {
  50   m_task_t task1 =
  51       MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
  52   m_task_t task2 =
  53       MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
  54
  55   INFO1("Send %d!", atoi(argv[1]));
  56   MSG_task_send(task1, "mymailbox");
  57
  58   INFO1("Send %d!", atoi(argv[1]));
  59   MSG_task_send(task2, "mymailbox");
  60
  61   return 0;
  62 }
  63
  64 int main(int argc, char *argv[])
  65 {
  66   MSG_global_init(&argc, argv);
  67
  68   MSG_create_environment("platform.xml");
  69
  70   MSG_function_register("server", server);
  71
  72   MSG_function_register("client", client);
  73
  74   MSG_launch_application("deploy_bugged2.xml");
  75
  76   MSG_main();
  77
  78   return 0;
  79 }