X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/272ccad1b68b6d9c17069f3c934886925bb15b5d..1fb08bfd88ea0a1e8b4c1ec2b0ec4519126b6c51:/examples/msg/mc/bugged2_liveness.c diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c index 5a2dd19e80..fb7c2d854b 100644 --- a/examples/msg/mc/bugged2_liveness.c +++ b/examples/msg/mc/bugged2_liveness.c @@ -1,190 +1,110 @@ -/***************** Producer/Consumer Algorithm *************************/ -/* This example implements a producer/consumer algorithm. */ -/* If consumer work before producer, message is empty */ -/***********************************************************************/ - +/***************************** Bugged2 ****************************************/ +/* This example implements a centralized mutual exclusion algorithm. */ +/* One client stay always in critical section */ +/* LTL property checked : !(GFcs) */ +/******************************************************************************/ #include "msg/msg.h" #include "mc/mc.h" #include "xbt/automaton.h" #include "bugged2_liveness.h" -XBT_LOG_NEW_DEFAULT_CATEGORY(bugged2_liveness, "my log messages"); - -char* buffer; - -int consume = 0; -int produce = 0; -int cready = 0; -int pready = 0; +XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "my log messages"); + +int cs = 0; -int predPready(){ - return pready; +int predCS(){ + return cs; } -int predCready(){ - return cready; -} -int predConsume(){ - return consume; -} - -int predProduce(){ - return produce; -} +int coordinator(int argc, char **argv); +int client(int argc, char **argv); int coordinator(int argc, char *argv[]) { - xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL); - int CS_used = 0; - - while(1) { - m_task_t task = NULL; + int CS_used = 0; // initially the CS is idle + + while (1) { + msg_task_t task = NULL; MSG_task_receive(&task, "coordinator"); - const char *kind = MSG_task_get_name(task); - if (!strcmp(kind, "request")) { + const char *kind = MSG_task_get_name(task); //is it a request or a release? + if (!strcmp(kind, "request")) { // that's a request char *req = MSG_task_get_data(task); - if (CS_used) { - XBT_INFO("CS already used. Queue the request"); - xbt_dynar_push(requests, &req); - } else { - m_task_t answer = MSG_task_create("grant", 0, 1000, NULL); - MSG_task_send(answer, req); - CS_used = 1; - XBT_INFO("CS idle. Grant immediatly"); - } - } else { - if (xbt_dynar_length(requests) > 0) { - XBT_INFO("CS release. Grant to queued requests"); - char *req; - xbt_dynar_pop(requests, &req); - MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req); - } else { - XBT_INFO("CS_realase, ressource now idle"); - CS_used = 0; + if (CS_used) { + XBT_INFO("CS already used."); + msg_task_t answer = MSG_task_create("not grant", 0, 1000, NULL); + MSG_task_send(answer, req); + MC_compare(); + } else { // can serve it immediatly + XBT_INFO("CS idle. Grant immediatly"); + msg_task_t answer = MSG_task_create("grant", 0, 1000, NULL); + MSG_task_send(answer, req); + CS_used = 1; } + } else { // that's a release. Check if someone was waiting for the lock + XBT_INFO("CS release. resource now idle"); + CS_used = 0; } - MSG_task_destroy(task); - + kind = NULL; } - - return 0; - -} - -int producer(int argc, char *argv[]) -{ - - char * my_mailbox = bprintf("%s", argv[1]); - while(1) { - - /* Create message */ - const char *mess = "message"; - - pready = 1; - XBT_INFO("pready = 1"); - - /* CS request */ - XBT_INFO("Producer ask the request"); - MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator"); - - /* Wait the answer */ - m_task_t grant = NULL; - MSG_task_receive(&grant, my_mailbox); - MSG_task_destroy(grant); - - /* Push message (size of buffer = 1) */ - buffer = strdup(mess); - - produce = 1; - XBT_INFO("produce = 1"); - - /* CS release */ - MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator"); - - produce = 0; - pready = 0; - - XBT_INFO("pready et produce = 0"); - - } - return 0; - } -int consumer(int argc, char *argv[]) +int client(int argc, char *argv[]) { + int my_pid = MSG_process_get_PID(MSG_process_self()); + char *my_mailbox = bprintf("%s", argv[1]); + const char* kind; + + while(1){ - char * my_mailbox = bprintf("%s", argv[1]); - char *mess; + XBT_INFO("Client (%s) asks the request", my_mailbox); + MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), + "coordinator"); + msg_task_t answer = NULL; + MSG_task_receive(&answer, my_mailbox); - while(1) { + kind = MSG_task_get_name(answer); - /* CS request */ - XBT_INFO("Consumer ask the request"); - MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator"); - - cready = 1; - XBT_INFO("cready = 1"); - - /* Wait the answer */ - m_task_t grant = NULL; - MSG_task_receive(&grant, my_mailbox); - MSG_task_destroy(grant); - - /* Pop message */ - mess = malloc(8*sizeof(char)); - mess = strdup(buffer); - buffer[0] = '\0'; - - /* Display message */ - XBT_INFO("Message : %s", mess); - if(strcmp(mess, "") != 0){ - consume = 1; - XBT_INFO("consume = 1"); - } - - /* CS release */ - MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator"); + if (!strcmp(kind, "grant")) { - free(mess); + XBT_INFO("Client (%s) got the answer (grant). Sleep a bit and release it", my_mailbox); - consume = 0; - cready = 0; - - XBT_INFO("cready et consume = 0"); + if(!strcmp(my_mailbox, "1")) + cs = 1; + + }else{ + + XBT_INFO("Client (%s) got the answer (not grant). Try again", my_mailbox); + + } + MSG_task_destroy(answer); + kind = NULL; + + MSG_process_sleep(my_pid); } return 0; - } - int main(int argc, char *argv[]) { + + MSG_init(&argc, argv); - buffer = malloc(8*sizeof(char)); - buffer[0]='\0'; - - xbt_automaton_t a = MC_create_automaton("promela2_bugged2_liveness"); - xbt_new_propositional_symbol(a,"pready", &predPready); - xbt_new_propositional_symbol(a,"cready", &predCready); - xbt_new_propositional_symbol(a,"consume", &predConsume); - xbt_new_propositional_symbol(a,"produce", &predProduce); + MSG_config("model-check/property","promela_bugged2_liveness"); + MC_automaton_new_propositional_symbol("cs", &predCS); - MSG_global_init(&argc, argv); MSG_create_environment("../msg_platform.xml"); MSG_function_register("coordinator", coordinator); - MSG_function_register("consumer", consumer); - MSG_function_register("producer", producer); + MSG_function_register("client", client); MSG_launch_application("deploy_bugged2_liveness.xml"); - MSG_main_liveness(a); + MSG_main(); return 0;