From 9553ec877f1dc96e9b44fbac31d47773e40adae3 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 17 Nov 2011 10:06:29 +0100 Subject: [PATCH] model-checker : examples changed --- examples/msg/mc/CMakeLists.txt | 6 +- examples/msg/mc/example_liveness_with_cycle.c | 25 ++-- .../msg/mc/example_liveness_with_cycle2.c | 140 ++++++++++++++++++ .../msg/mc/example_liveness_without_cycle.c | 101 ------------- .../msg/mc/example_liveness_without_cycle.h | 20 --- 5 files changed, 158 insertions(+), 134 deletions(-) create mode 100644 examples/msg/mc/example_liveness_with_cycle2.c delete mode 100644 examples/msg/mc/example_liveness_without_cycle.c delete mode 100644 examples/msg/mc/example_liveness_without_cycle.h diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index 40d5fdccad..30241f900b 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -9,8 +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(example_liveness_without_cycle automaton.c -automatonparse_promela.c example_liveness_without_cycle.c) +add_executable(example_liveness_with_cycle2 automaton.c +automatonparse_promela.c example_liveness_with_cycle2.c) add_executable(example_liveness_with_cycle automaton.c automatonparse_promela.c example_liveness_with_cycle.c) @@ -24,5 +24,5 @@ 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(example_liveness_without_cycle simgrid m ) +target_link_libraries(example_liveness_with_cycle2 simgrid m ) target_link_libraries(example_liveness_with_cycle simgrid m ) diff --git a/examples/msg/mc/example_liveness_with_cycle.c b/examples/msg/mc/example_liveness_with_cycle.c index 8ec9725a46..80765b7203 100644 --- a/examples/msg/mc/example_liveness_with_cycle.c +++ b/examples/msg/mc/example_liveness_with_cycle.c @@ -1,7 +1,6 @@ /***************** Centralized Mutual Exclusion Algorithm *********************/ /* This example implements a centralized mutual exclusion algorithm. */ -/* There is no bug on it, it is just provided to test the state space */ -/* reduction of DPOR. */ +/* CS requests of client 2 not satisfied */ /******************************************************************************/ #include "msg/msg.h" @@ -12,7 +11,7 @@ #include "y.tab.c" #define AMOUNT_OF_CLIENTS 2 -#define CS_PER_PROCESS 3 +#define CS_PER_PROCESS 4 XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages"); @@ -80,17 +79,20 @@ 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 3 times, sleeping a bit in between int i; - + + // request the CS 4 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){ p = 1; q = 0; + XBT_DEBUG("Propositions changed : p=1, q=0"); } + // wait the answer m_task_t grant = NULL; MSG_task_receive(&grant, my_mailbox); @@ -98,8 +100,10 @@ int client(int argc, char *argv[]) if(strcmp(my_mailbox, "2") == 0){ q = 1; p = 0; + XBT_DEBUG("Propositions changed : p=0, q=1"); } + MSG_task_destroy(grant); XBT_INFO("%s got the answer. Sleep a bit and release it", argv[1]); MSG_process_sleep(1); @@ -107,10 +111,12 @@ int client(int argc, char *argv[]) MSG_process_sleep(my_pid); - q=0; - p=0; + if(strcmp(my_mailbox, "2") == 0){ + q=0; + p=0; + XBT_DEBUG("Propositions changed : p=0, q=0"); + } - } XBT_INFO("Got all the CS I wanted (%s), quit now", my_mailbox); @@ -130,8 +136,7 @@ int main(int argc, char *argv[]) MSG_function_register("coordinator", coordinator); MSG_function_register("client", client); MSG_launch_application("deploy_mutex2.xml"); - MSG_main_liveness_stateless(automaton); - //MSG_main(); + MSG_main_liveness_stateless(automaton, argv[0]); return 0; } diff --git a/examples/msg/mc/example_liveness_with_cycle2.c b/examples/msg/mc/example_liveness_with_cycle2.c new file mode 100644 index 0000000000..f2a5dcb889 --- /dev/null +++ b/examples/msg/mc/example_liveness_with_cycle2.c @@ -0,0 +1,140 @@ +/***************** Centralized Mutual Exclusion Algorithm *********************/ +/* This example implements a centralized mutual exclusion algorithm. */ +/* CS requests of client 2 not satisfied */ +/******************************************************************************/ + +#include "msg/msg.h" +#include "mc/mc.h" +#include "xbt/automaton.h" +#include "xbt/automatonparse_promela.h" +#include "example_liveness_with_cycle.h" +#include "y.tab.c" + +#define AMOUNT_OF_CLIENTS 2 +#define CS_PER_PROCESS 3 + +XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle2, "my log messages"); + + +int p=0; +int q=0; + +int predP(){ + return p; +} + +int predQ(){ + return q; +} + + +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, "1") == 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, "1") == 0){ + xbt_dynar_pop(requests, &req); + MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req); + }else{ + CS_used = 0; + } + } else { // nobody wants it + XBT_INFO("CS release. resource now idle"); + CS_used = 0; + } + } + MSG_task_destroy(task); + } + XBT_INFO("Received all releases, quit now"); + 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("Ask the request"); + + MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator"); + + if(strcmp(my_mailbox, "2") == 0){ + p = 1; + q = 0; + XBT_INFO("Propositions changed (p=1, q=0)"); + } + + // wait the answer + + m_task_t grant = NULL; + MSG_task_receive(&grant, my_mailbox); + + if((strcmp(my_mailbox, "2") == 0) && (strcmp(MSG_task_get_name(grant), "grant") == 0)){ + q = 1; + p = 0; + XBT_INFO("Propositions changed (q=1, p=0)"); + } + + 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, "2") == 0){ + q=0; + p=0; + XBT_INFO("Propositions changed (q=0, p=0)"); + } + + } + + XBT_INFO("Got all the CS I wanted (%s), quit now", my_mailbox); + return 0; +} + +int main(int argc, char *argv[]) +{ + init(); + yyparse(); + automaton = get_automaton(); + xbt_new_propositional_symbol(automaton,"p", &predP); + xbt_new_propositional_symbol(automaton,"q", &predQ); + + 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_mutex2.xml"); + MSG_main_liveness_stateless(automaton, argv[0]); + + return 0; +} diff --git a/examples/msg/mc/example_liveness_without_cycle.c b/examples/msg/mc/example_liveness_without_cycle.c deleted file mode 100644 index 219524b010..0000000000 --- a/examples/msg/mc/example_liveness_without_cycle.c +++ /dev/null @@ -1,101 +0,0 @@ -#include "xbt/automaton.h" -#include "xbt/automatonparse_promela.h" -#include "example_liveness_without_cycle.h" -#include "msg/msg.h" -#include "mc/mc.h" - -#include "y.tab.c" - -#define N 3 - -XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_without_cycle, "Example liveness without cycle"); - -extern xbt_automaton_t automaton; - -int r=0; -int e=1; -int d=1; - -int predR(){ - return r; -} - -int predD(){ - return d; -} - -int predE(){ - return e; -} - - - -int server(int argc, char *argv[]) -{ - m_task_t task = NULL; - int count = 0; - while (count < N) { - if (task) { - MSG_task_destroy(task); - task = NULL; - } - MSG_task_receive(&task, "mymailbox"); - count++; - r=(r+1)%2; - //XBT_INFO("r (server) = %d", r); - - } - //MC_assert_pair_stateless(atoi(MSG_task_get_name(task)) == 3); - - XBT_INFO("OK"); - return 0; -} - -int client(int argc, char *argv[]) -{ - - m_task_t task = - MSG_task_create(argv[1], 0 /*comp cost */ , 10000 /*comm size */ , - NULL /*arbitrary data */ ); - - MSG_task_send(task, "mymailbox"); - - XBT_INFO("Sent!"); - - r=(r+1)%2; - //XBT_INFO("r (client) = %d", r); - - 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,"e", &predE); - xbt_new_propositional_symbol(automaton,"d", &predD); - - //display_automaton(); - - MSG_global_init(&argc, argv); - - MSG_create_environment("platform.xml"); - - MSG_function_register("server", server); - - MSG_function_register("client", client); - - MSG_launch_application("deploy_bugged1.xml"); - - //XBT_INFO("r=%d", r); - - MSG_main_liveness_stateless(automaton); - - MSG_clean(); - - return 0; - -} diff --git a/examples/msg/mc/example_liveness_without_cycle.h b/examples/msg/mc/example_liveness_without_cycle.h deleted file mode 100644 index 1667c45f65..0000000000 --- a/examples/msg/mc/example_liveness_without_cycle.h +++ /dev/null @@ -1,20 +0,0 @@ -#ifndef _EXAMPLE_LIVENESS_WITHOUT_CYCLE_H -#define _EXAMPLE_LIVENESS_WITHOUT_CYCLE_H - -int yyparse(void); -int yywrap(void); -int yylex(void); - -int predP(void); -int predR(void); -int predQ(void); -int predD(void); -int predE(void); - - - - -int server(int argc, char *argv[]); -int client(int argc, char *argv[]); - -#endif -- 2.20.1