X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/4586126e5a968926d9c937fb5b6e39eff37a2bd3..a1c2fd1f61bd5733f3ddb126713ec5da13f1e440:/examples/msg/mc/bugged2_liveness.c diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c index 03d9d6c709..2310f28163 100644 --- a/examples/msg/mc/bugged2_liveness.c +++ b/examples/msg/mc/bugged2_liveness.c @@ -1,189 +1,94 @@ -/***************** Producer/Consumer Algorithm *************************/ -/* This example implements a producer/consumer algorithm. */ -/* If consumer work before producer, message is empty */ -/***********************************************************************/ +/* Copyright (c) 2012-2015. The SimGrid Team. + * All rights reserved. */ +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ -#include "msg/msg.h" +/***************************** Bugged2 ****************************************/ +/* This example implements a centralized mutual exclusion algorithm. */ +/* One client stay always in critical section */ +/* LTL property checked : !(GFcs) */ +/******************************************************************************/ + +#include "simgrid/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 predPready(){ - return pready; -} - -int predCready(){ - return cready; -} +int cs = 0; -int predConsume(){ - return consume; -} - -int predProduce(){ - return produce; -} - -int coordinator(int argc, char *argv[]) +static int coordinator(int argc, char *argv[]) { - xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL); - int CS_used = 0; + int CS_used = 0; // initially the CS is idle - while(1) { + 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 { + 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); + } else { // can serve it immediately + XBT_INFO("CS idle. Grant immediately"); msg_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; } + } 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[]) +static int client(int argc, char *argv[]) { + int my_pid = MSG_process_get_PID(MSG_process_self()); + char *my_mailbox = xbt_strdup(argv[1]); + const char* kind; - 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"); + while(1){ + XBT_INFO("Client (%s) asks the request", my_mailbox); MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator"); - /* Wait the answer */ - msg_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"); + msg_task_t answer = NULL; + MSG_task_receive(&answer, my_mailbox); - /* CS release */ - MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator"); + kind = MSG_task_get_name(answer); - produce = 0; - pready = 0; - - XBT_INFO("pready et produce = 0"); - - } - - return 0; - -} - -int consumer(int argc, char *argv[]) -{ - - char * my_mailbox = bprintf("%s", argv[1]); - char *mess; - - - while(1) { - - /* 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 */ - msg_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"); + if (!strcmp(kind, "grant")) { + XBT_INFO("Client (%s) got the answer (grant). Sleep a bit and release it", my_mailbox); + if(!strcmp(my_mailbox, "1")) + cs = 1; + }else{ + XBT_INFO("Client (%s) got the answer (not grant). Try again", my_mailbox); } - /* CS release */ - MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator"); - - free(mess); - - consume = 0; - cready = 0; - - XBT_INFO("cready et consume = 0"); + MSG_task_destroy(answer); + kind = NULL; + MSG_process_sleep(my_pid); } - return 0; - } - int main(int argc, char *argv[]) { - - buffer = malloc(8*sizeof(char)); - buffer[0]='\0'; - MSG_init(&argc, argv); - MSG_config("model-check/property","promela2_bugged2_liveness"); - MC_automaton_new_propositional_symbol("pready", &predPready); - MC_automaton_new_propositional_symbol("cready", &predCready); - MC_automaton_new_propositional_symbol("consume", &predConsume); - MC_automaton_new_propositional_symbol("produce", &predProduce); - + MC_automaton_new_propositional_symbol_pointer("cs", &cs); + 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();