examples/msg/mc/bugged3.c

   1 /**************** Shared buffer between asynchronous receives *****************/
   2 /* Server process assumes that the data from the second communication comm2   */
   3 /* will overwrite the one from the first communication, because of the order  */
   4 /* of the wait calls. This is not true because data copy can be triggered by  */
   5 /* a call to wait on the other end of the communication (client).             */
   6 /* NOTE that the communications use different mailboxes, but they share the   */
   7 /* same buffer for reception (task1).                                         */
   8 /******************************************************************************/
   9
  10 #include <msg/msg.h>
  11 #include <mc/modelchecker.h>
  12
  13 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3,"this example");
  14
  15 int server(int argc,char *argv[]);
  16 int client(int argc,char *argv[]);
  17
  18 int server(int argc,char *argv[])
  19 {
  20   m_task_t task1;
  21   long val1;
  22   msg_comm_t comm1, comm2;
  23
  24   comm1 = MSG_task_irecv(&task1,"mymailbox1");
  25   comm2 = MSG_task_irecv(&task1,"mymailbox2");
  26   MSG_comm_wait(comm1, -1);
  27   MSG_comm_wait(comm2, -1);
  28
  29   val1 = (long)MSG_task_get_data(task1);
  30   INFO1("Received %lu", val1);
  31
  32   MC_assert(val1 == 2);
  33
  34   INFO0("OK");
  35   return 0;
  36 }
  37
  38 int client(int argc,char *argv[])
  39 {
  40   msg_comm_t comm;
  41   char *mbox;
  42   m_task_t task1 = MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
  43
  44   mbox = bprintf("mymailbox%s", argv[1]);
  45
  46   INFO1("Send %d!", atoi(argv[1]));
  47   comm = MSG_task_isend(task1,mbox);
  48   MSG_comm_wait(comm, -1);
  49
  50   xbt_free(mbox);
  51
  52   return 0;
  53 }
  54
  55 int main(int argc,char*argv[])
  56 {
  57   MSG_global_init(&argc,argv);
  58
  59   MSG_create_environment("platform.xml");
  60
  61   MSG_function_register("server", server);
  62
  63   MSG_function_register("client", client);
  64
  65   MSG_launch_application("deploy_bugged3.xml");
  66
  67   MSG_main();
  68
  69   return 0;
  70 }