examples/msg/mc/bugged2_liveness.c

   1 /***************** Producer/Consumer Algorithm *************************/
   2 /* This example implements a producer/consumer algorithm.              */
   3 /* If consumer work before producer, message is empty                  */
   4 /***********************************************************************/
   5
   6
   7 #include "msg/msg.h"
   8 #include "mc/mc.h"
   9 #include "xbt/automaton.h"
  10 #include "bugged2_liveness.h"
  11
  12 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged2_liveness, "my log messages");
  13
  14 char* buffer;
  15
  16 int consume = 0;
  17 int produce = 0;
  18 int cready = 0;
  19 int pready = 0;
  20
  21 int predPready(){
  22   return pready;
  23 }
  24
  25 int predCready(){
  26   return cready;
  27 }
  28
  29 int predConsume(){
  30   return consume;
  31 }
  32
  33 int predProduce(){
  34   return produce;
  35 }
  36
  37 int coordinator(int argc, char *argv[])
  38 {
  39   xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
  40   int CS_used = 0;
  41
  42   while(1) {
  43     m_task_t task = NULL;
  44     MSG_task_receive(&task, "coordinator");
  45     const char *kind = MSG_task_get_name(task);
  46     if (!strcmp(kind, "request")) {
  47       char *req = MSG_task_get_data(task);
  48       if (CS_used) {
  49   XBT_INFO("CS already used. Queue the request");
  50   xbt_dynar_push(requests, &req);
  51       } else {
  52   m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
  53   MSG_task_send(answer, req);
  54   CS_used = 1;
  55   XBT_INFO("CS idle. Grant immediatly");
  56       }
  57     } else {
  58       if (xbt_dynar_length(requests) > 0) {
  59   XBT_INFO("CS release. Grant to queued requests");
  60   char *req;
  61   xbt_dynar_pop(requests, &req);
  62   MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
  63       } else {
  64   XBT_INFO("CS_realase, ressource now idle");
  65   CS_used = 0;
  66       }
  67     }
  68
  69     MSG_task_destroy(task);
  70
  71   }
  72
  73   return 0;
  74
  75 }
  76
  77 int producer(int argc, char *argv[])
  78 {
  79
  80   char * my_mailbox = bprintf("%s", argv[1]);
  81
  82   while(1) {
  83
  84     /* Create message */
  85     const char *mess = "message";
  86
  87     pready = 1;
  88     XBT_INFO("pready = 1");
  89
  90     /* CS request */
  91     XBT_INFO("Producer ask the request");
  92     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
  93
  94     /* Wait the answer */
  95     m_task_t grant = NULL;
  96     MSG_task_receive(&grant, my_mailbox);
  97     MSG_task_destroy(grant);
  98
  99     /* Push message (size of buffer = 1) */
 100     buffer = strdup(mess);
 101
 102     produce = 1;
 103     XBT_INFO("produce = 1");
 104
 105     /* CS release */
 106     MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
 107
 108     produce = 0;
 109     pready = 0;
 110
 111     XBT_INFO("pready et produce = 0");
 112
 113   }
 114
 115   return 0;
 116
 117 }
 118
 119 int consumer(int argc, char *argv[])
 120 {
 121
 122   char * my_mailbox = bprintf("%s", argv[1]);
 123   char *mess;
 124
 125
 126   while(1) {
 127
 128     /* CS request */
 129     XBT_INFO("Consumer ask the request");
 130     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
 131
 132     cready = 1;
 133     XBT_INFO("cready = 1");
 134
 135     /* Wait the answer */
 136     m_task_t grant = NULL;
 137     MSG_task_receive(&grant, my_mailbox);
 138     MSG_task_destroy(grant);
 139
 140     /* Pop message  */
 141     mess = malloc(8*sizeof(char));
 142     mess = strdup(buffer);
 143     buffer[0] = '\0';
 144
 145     /* Display message */
 146     XBT_INFO("Message : %s", mess);
 147     if(strcmp(mess, "") != 0){
 148       consume = 1;
 149       XBT_INFO("consume = 1");
 150     }
 151
 152     /* CS release */
 153     MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
 154
 155     free(mess);
 156
 157     consume = 0;
 158     cready = 0;
 159
 160     XBT_INFO("cready et consume = 0");
 161
 162   }
 163
 164   return 0;
 165
 166 }
 167
 168
 169 int main(int argc, char *argv[])
 170 {
 171
 172   buffer = malloc(8*sizeof(char));
 173   buffer[0]='\0';
 174
 175   MSG_init(&argc, argv);
 176
 177   MSG_config("model-check/property","promela2_bugged2_liveness");
 178   MC_automaton_new_propositional_symbol("pready", &predPready);
 179   MC_automaton_new_propositional_symbol("cready", &predCready);
 180   MC_automaton_new_propositional_symbol("consume", &predConsume);
 181   MC_automaton_new_propositional_symbol("produce", &predProduce);
 182
 183   MSG_create_environment("../msg_platform.xml");
 184   MSG_function_register("coordinator", coordinator);
 185   MSG_function_register("consumer", consumer);
 186   MSG_function_register("producer", producer);
 187   MSG_launch_application("deploy_bugged2_liveness.xml");
 188   MSG_main();
 189
 190   return 0;
 191
 192 }