From: Marion Guthmuller Date: Fri, 20 Apr 2012 17:02:58 +0000 (+0200) Subject: model-checker : separate bugged1_liveness (deleted) example in two cases : finite... X-Git-Tag: v3_7~65^2~5 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d1f5e7fabd6c999c95f116c2d422d25d5f228986?hp=127880536a17bd02faba5e25df542b50c9fe72cc model-checker : separate bugged1_liveness (deleted) example in two cases : finite CS requests (bugged1_for_liveness) and infinite CS requests (bugged1_while_liveness) --- diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index dca1a849f1..eb784008ba 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -9,7 +9,8 @@ add_executable(bugged2_stateful bugged2_stateful.c) add_executable(bugged2 bugged2.c) add_executable(bugged3 bugged3.c) add_executable(random_test random_test.c) -add_executable(bugged1_liveness automaton.c automatonparse_promela.c bugged1_liveness.c) +add_executable(bugged1_for_liveness automaton.c automatonparse_promela.c bugged1_for_liveness.c) +add_executable(bugged1_while_liveness automaton.c automatonparse_promela.c bugged1_while_liveness.c) add_executable(bugged2_liveness automaton.c automatonparse_promela.c bugged2_liveness.c) add_executable(centralized_liveness automaton.c automatonparse_promela.c centralized_liveness.c) add_executable(test_snapshot automaton.c automatonparse_promela.c test_snapshot.c) @@ -21,7 +22,8 @@ target_link_libraries(bugged2_stateful simgrid m) target_link_libraries(bugged2 simgrid m ) target_link_libraries(bugged3 simgrid m ) target_link_libraries(random_test simgrid m ) -target_link_libraries(bugged1_liveness simgrid m ) +target_link_libraries(bugged1_for_liveness simgrid m ) +target_link_libraries(bugged1_while_liveness simgrid m ) target_link_libraries(bugged2_liveness simgrid m ) target_link_libraries(centralized_liveness simgrid m ) target_link_libraries(test_snapshot simgrid m ) diff --git a/examples/msg/mc/bugged1_liveness.c b/examples/msg/mc/bugged1_for_liveness.c similarity index 91% rename from examples/msg/mc/bugged1_liveness.c rename to examples/msg/mc/bugged1_for_liveness.c index eaeceb4c2b..b45f9ceafd 100644 --- a/examples/msg/mc/bugged1_liveness.c +++ b/examples/msg/mc/bugged1_for_liveness.c @@ -1,6 +1,6 @@ /***************** Centralized Mutual Exclusion Algorithm *********************/ /* This example implements a centralized mutual exclusion algorithm. */ -/* CS requests of client 2 not satisfied */ +/* CS requests of client 1 not satisfied */ /* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok) */ /******************************************************************************/ @@ -12,7 +12,7 @@ #include "y.tab.c" #define AMOUNT_OF_CLIENTS 2 -#define CS_PER_PROCESS 1 +#define CS_PER_PROCESS 2 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages"); @@ -44,7 +44,7 @@ int coordinator(int argc, char *argv[]) XBT_INFO("CS already used. Queue the request of client %d", atoi(req) +1); xbt_dynar_push(requests, &req); } else { // can serve it immediatly - if(strcmp(req, "1") == 0){ + if(strcmp(req, "2") == 0){ m_task_t answer = MSG_task_create("grant", 0, 1000, NULL); MSG_task_send(answer, req); CS_used = 1; @@ -56,7 +56,7 @@ int coordinator(int argc, char *argv[]) XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests)); char *req ; xbt_dynar_get_cpy(requests, (xbt_dynar_length(requests) - 1), &req); - if(strcmp(req, "1") == 0){ + if(strcmp(req, "2") == 0){ xbt_dynar_pop(requests, &req); MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req); todo--; @@ -85,13 +85,13 @@ int client(int argc, char *argv[]) char *my_mailbox = bprintf("%s", argv[1]); int i; - // request the CS 4 times, sleeping a bit in between + // request the CS (CS_PER_PROCESS times), sleeping a bit in between for (i = 0; i < CS_PER_PROCESS; i++) { XBT_INFO("Ask the request"); MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator"); - if(strcmp(my_mailbox, "2") == 0){ + if(strcmp(my_mailbox, "1") == 0){ r = 1; cs = 0; XBT_DEBUG("Propositions changed : r=1, cs=0"); @@ -102,7 +102,7 @@ int client(int argc, char *argv[]) MSG_task_receive(&grant, my_mailbox); const char *kind = MSG_task_get_name(grant); - if((strcmp(my_mailbox, "2") == 0) && (strcmp("grant", kind) == 0)){ + if((strcmp(my_mailbox, "1") == 0) && (strcmp("grant", kind) == 0)){ cs = 1; r = 0; XBT_DEBUG("Propositions changed : r=0, cs=1"); @@ -116,7 +116,7 @@ int client(int argc, char *argv[]) MSG_process_sleep(my_pid); - if(strcmp(my_mailbox, "2") == 0){ + if(strcmp(my_mailbox, "1") == 0){ cs=0; r=0; XBT_DEBUG("Propositions changed : r=0, cs=0"); diff --git a/examples/msg/mc/bugged1_while_liveness.c b/examples/msg/mc/bugged1_while_liveness.c new file mode 100644 index 0000000000..95b6e5be36 --- /dev/null +++ b/examples/msg/mc/bugged1_while_liveness.c @@ -0,0 +1,137 @@ +/***************** Centralized Mutual Exclusion Algorithm *********************/ +/* This example implements a centralized mutual exclusion algorithm. */ +/* CS requests of client 1 not satisfied */ +/* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok) */ +/******************************************************************************/ + +#include "msg/msg.h" +#include "mc/mc.h" +#include "xbt/automaton.h" +#include "xbt/automatonparse_promela.h" +#include "bugged1_liveness.h" +#include "y.tab.c" + +XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages"); + +int r=0; +int cs=0; + +int predR(){ + return r; +} + +int predCS(){ + return cs; +} + + +int coordinator(int argc, char *argv[]) +{ + xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL); // dynamic vector storing requests (which are char*) + int CS_used = 0; // initially the CS is idle + while (1) { + m_task_t task = NULL; + MSG_task_receive(&task, "coordinator"); + 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) { // need to push the request in the vector + XBT_INFO("CS already used. Queue the request of client %d", atoi(req) +1); + xbt_dynar_push(requests, &req); + } else { // can serve it immediatly + if(strcmp(req, "2") == 0){ + 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 { // that's a release. Check if someone was waiting for the lock + if (xbt_dynar_length(requests) > 0) { + XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests)); + char *req ; + xbt_dynar_get_cpy(requests, (xbt_dynar_length(requests) - 1), &req); + if(strcmp(req, "2") == 0){ + xbt_dynar_pop(requests, &req); + MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req); + }else{ + xbt_dynar_pop(requests, &req); + MSG_task_send(MSG_task_create("notgrant", 0, 1000, NULL), req); + CS_used = 0; + } + } else { // nobody wants it + XBT_INFO("CS release. resource now idle"); + CS_used = 0; + } + } + MSG_task_destroy(task); + } + + return 0; +} + +int client(int argc, char *argv[]) +{ + int my_pid = MSG_process_get_PID(MSG_process_self()); + + char *my_mailbox = bprintf("%s", argv[1]); + + // request the CS, sleeping a bit in between + while(1) { + + XBT_INFO("Ask the request"); + MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator"); + + if(strcmp(my_mailbox, "1") == 0){ + r = 1; + cs = 0; + XBT_DEBUG("Propositions changed : r=1, cs=0"); + } + + // wait the answer + m_task_t grant = NULL; + MSG_task_receive(&grant, my_mailbox); + const char *kind = MSG_task_get_name(grant); + + if((strcmp(my_mailbox, "1") == 0) && (strcmp("grant", kind) == 0)){ + cs = 1; + r = 0; + XBT_DEBUG("Propositions changed : r=0, cs=1"); + } + + + MSG_task_destroy(grant); + XBT_INFO("%s got the answer. Sleep a bit and release it", argv[1]); + MSG_process_sleep(1); + MSG_task_send(MSG_task_create("release", 0, 1000, NULL), "coordinator"); + + MSG_process_sleep(my_pid); + + if(strcmp(my_mailbox, "1") == 0){ + cs=0; + r=0; + XBT_DEBUG("Propositions changed : r=0, cs=0"); + } + + } + + return 0; +} + +int main(int argc, char *argv[]) +{ + init(); + yyparse(); + automaton = get_automaton(); + xbt_new_propositional_symbol(automaton,"r", &predR); + xbt_new_propositional_symbol(automaton,"cs", &predCS); + + MSG_global_init(&argc, argv); + MSG_create_environment("../msg_platform.xml"); + MSG_function_register("coordinator", coordinator); + MSG_function_register("client", client); + MSG_launch_application("deploy_bugged1_liveness.xml"); + MSG_main_liveness(automaton, argv[0]); + + return 0; +}