From: Marion Guthmuller Date: Sun, 3 Jun 2012 07:45:48 +0000 (+0200) Subject: model-checker : new examples X-Git-Tag: v3_8~650 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/5ce4106d57347a7871f0f0ee39bdef5fd0c824ae model-checker : new examples --- diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index eb784008ba..aa9cbad180 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -13,6 +13,7 @@ add_executable(bugged1_for_liveness automaton.c automatonparse_promela.c bugged1 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(centralized_liveness_deadlock automaton.c automatonparse_promela.c centralized_liveness_deadlock.c) add_executable(test_snapshot automaton.c automatonparse_promela.c test_snapshot.c) target_link_libraries(centralized simgrid m ) @@ -26,4 +27,5 @@ 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(centralized_liveness_deadlock simgrid m ) target_link_libraries(test_snapshot simgrid m ) diff --git a/examples/msg/mc/centralized_liveness.c b/examples/msg/mc/centralized_liveness.c index d34bbdb5df..54804faf2f 100644 --- a/examples/msg/mc/centralized_liveness.c +++ b/examples/msg/mc/centralized_liveness.c @@ -1,3 +1,8 @@ +/***************** Centralized Mutual Exclusion Algorithm *********************/ +/* This example implements a centralized mutual exclusion algorithm. */ +/* LTL property checked : !(GFcs) */ +/******************************************************************************/ + #include "msg/msg.h" #include "mc/mc.h" #include "xbt/automaton.h" @@ -5,14 +10,12 @@ #include "centralized_liveness.h" #include "y.tab.c" -#define AMOUNT_OF_CLIENTS 2 - XBT_LOG_NEW_DEFAULT_CATEGORY(centralized, "my log messages"); -int cs2 = 0; +int cs = 0; -int predCS2(){ - return cs2; +int predCS(){ + return cs; } @@ -21,7 +24,6 @@ int client(int argc, char **argv); 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) { @@ -30,9 +32,10 @@ int coordinator(int argc, char *argv[]) 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"); - xbt_dynar_push(requests, &req); + if (CS_used) { + XBT_INFO("CS already used."); + m_task_t answer = MSG_task_create("not grant", 0, 1000, NULL); + MSG_task_send(answer, req); } else { // can serve it immediatly XBT_INFO("CS idle. Grant immediatly"); m_task_t answer = MSG_task_create("grant", 0, 1000, NULL); @@ -40,16 +43,8 @@ int coordinator(int argc, char *argv[]) CS_used = 1; } } else { // that's a release. Check if someone was waiting for the lock - if (!xbt_dynar_is_empty(requests)) { - XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", - xbt_dynar_length(requests)); - char *req; - xbt_dynar_pop(requests, &req); - MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req); - } else { // nobody wants it - XBT_INFO("CS release. resource now idle"); - CS_used = 0; - } + XBT_INFO("CS release. resource now idle"); + CS_used = 0; } MSG_task_destroy(task); } @@ -61,27 +56,42 @@ 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){ - if(!strcmp(my_mailbox, "2")) - cs2 = 0; - - XBT_INFO("Client (%s) ask the request", my_mailbox); + XBT_INFO("Client (%s) asks the request", my_mailbox); 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); - XBT_INFO("got the answer. Sleep a bit and release it"); + m_task_t answer = NULL; + MSG_task_receive(&answer, my_mailbox); - if(!strcmp(my_mailbox, "2")) - cs2 = 1; + kind = MSG_task_get_name(answer); + + if (!strcmp(kind, "grant")) { - MSG_process_sleep(1); - MSG_task_send(MSG_task_create("release", 0, 1000, NULL), - "coordinator"); + XBT_INFO("Client (%s) got the answer (grant). Sleep a bit and release it", my_mailbox); + + if(!strcmp(my_mailbox, "1")) + cs = 1; + + /*MSG_process_sleep(my_pid); + MSG_task_send(MSG_task_create("release", 0, 1000, NULL), + "coordinator"); + XBT_INFO("Client (%s) releases the CS", my_mailbox); + + if(!strcmp(my_mailbox, "1")) + cs = 0;*/ + + }else{ + + XBT_INFO("Client (%s) got the answer (not grant). Try again", my_mailbox); + + } + + MSG_task_destroy(answer); + MSG_process_sleep(my_pid); } @@ -93,7 +103,7 @@ int main(int argc, char *argv[]) init(); yyparse(); automaton = get_automaton(); - xbt_new_propositional_symbol(automaton,"cs2", &predCS2); + xbt_new_propositional_symbol(automaton,"cs", &predCS); MSG_global_init(&argc, argv); MSG_create_environment("../msg_platform.xml"); diff --git a/examples/msg/mc/centralized_liveness.h b/examples/msg/mc/centralized_liveness.h index 1c140317e3..aa796a8d2b 100644 --- a/examples/msg/mc/centralized_liveness.h +++ b/examples/msg/mc/centralized_liveness.h @@ -5,7 +5,7 @@ int yyparse(void); int yywrap(void); int yylex(void); -int predCS2(void); +int predCS(void); int coordinator(int argc, char *argv[]); int client(int argc, char *argv[]); diff --git a/examples/msg/mc/centralized_liveness_deadlock.c b/examples/msg/mc/centralized_liveness_deadlock.c new file mode 100644 index 0000000000..5f58118744 --- /dev/null +++ b/examples/msg/mc/centralized_liveness_deadlock.c @@ -0,0 +1,114 @@ +/***************** Centralized Mutual Exclusion Algorithm *********************/ +/* This example implements a centralized mutual exclusion algorithm. */ +/* LTL property checked : !(GFcs) */ +/******************************************************************************/ + +#include "msg/msg.h" +#include "mc/mc.h" +#include "xbt/automaton.h" +#include "xbt/automatonparse_promela.h" +#include "centralized_liveness.h" +#include "y.tab.c" + +XBT_LOG_NEW_DEFAULT_CATEGORY(centralized, "my log messages"); + +int cs = 0; + +int predCS(){ + return cs; +} + + +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); // 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"); + xbt_dynar_push(requests, &req); + } else { // can serve it immediatly + XBT_INFO("CS idle. Grant immediatly"); + m_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 + if (!xbt_dynar_is_empty(requests)) { + XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", + xbt_dynar_length(requests)); + char *req; + xbt_dynar_pop(requests, &req); + MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req); + } 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]); + + 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 + m_task_t grant = NULL; + MSG_task_receive(&grant, my_mailbox); + + MSG_task_destroy(grant); + XBT_INFO("Client (%s) got the answer. Sleep a bit and release it", my_mailbox); + + if(!strcmp(my_mailbox, "1")) + cs = 1; + + /*MSG_process_sleep(my_pid); + MSG_task_send(MSG_task_create("release", 0, 1000, NULL), + "coordinator"); + XBT_INFO("Client (%s) releases the CS", my_mailbox); + + if(!strcmp(my_mailbox, "1")) + cs = 0;*/ + + MSG_process_sleep(my_pid); + + } + + return 0; +} + +int main(int argc, char *argv[]) +{ + init(); + yyparse(); + automaton = get_automaton(); + 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_centralized_liveness.xml"); + MSG_main_liveness(automaton, argv[0]); + + return 0; + +}