From 30ddf1eb571e00c6b6e9723d6dc69ce4632471cc Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Sat, 6 Oct 2012 11:26:11 +0200 Subject: [PATCH] model-checker : cleanup in mc examples --- buildtools/Cmake/DefinePackages.cmake | 2 +- examples/msg/mc/CMakeLists.txt | 25 +-- examples/msg/mc/bugged1_liveness.c | 2 +- examples/msg/mc/bugged1_liveness.h | 4 - examples/msg/mc/bugged2_liveness.c | 197 ++++++------------ examples/msg/mc/bugged2_liveness.h | 12 +- examples/msg/mc/centralized_liveness.c | 115 ---------- examples/msg/mc/centralized_liveness.h | 13 -- .../msg/mc/centralized_liveness_deadlock.c | 112 ---------- examples/msg/mc/deploy_bugged2_liveness.xml | 5 +- .../msg/mc/deploy_centralized_liveness.xml | 47 ----- examples/msg/mc/promela2_bugged1_liveness | 11 - examples/msg/mc/promela2_bugged2_liveness | 17 -- examples/msg/mc/promela2_centralized_liveness | 11 - ...ged1_liveness => promela_bugged1_liveness} | 0 examples/msg/mc/promela_bugged2_liveness | 25 +-- examples/msg/mc/promela_centralized_liveness | 12 -- ...pare_snapshot.c => test_heap_comparison.c} | 2 +- examples/msg/mc/test_snapshot.c | 144 ------------- examples/msg/mc/test_snapshot.h | 16 -- src/include/mc/mc.h | 2 +- .../{compare_snapshot.c => heap_comparison.c} | 16 +- 22 files changed, 86 insertions(+), 704 deletions(-) delete mode 100644 examples/msg/mc/centralized_liveness.c delete mode 100644 examples/msg/mc/centralized_liveness.h delete mode 100644 examples/msg/mc/centralized_liveness_deadlock.c delete mode 100644 examples/msg/mc/deploy_centralized_liveness.xml delete mode 100644 examples/msg/mc/promela2_bugged1_liveness delete mode 100644 examples/msg/mc/promela2_bugged2_liveness delete mode 100644 examples/msg/mc/promela2_centralized_liveness rename examples/msg/mc/{promela1_bugged1_liveness => promela_bugged1_liveness} (100%) delete mode 100644 examples/msg/mc/promela_centralized_liveness rename examples/msg/mc/test/{compare_snapshot.c => test_heap_comparison.c} (77%) delete mode 100644 examples/msg/mc/test_snapshot.c delete mode 100644 examples/msg/mc/test_snapshot.h rename src/mc/test/{compare_snapshot.c => heap_comparison.c} (86%) diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 8c2aab70cb..0a48719f07 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -388,7 +388,7 @@ set(MC_SRC src/mc/mc_request.c src/mc/mc_state.c src/mc/memory_map.c - src/mc/test/compare_snapshot.c + src/mc/test/heap_comparison.c ) set(headers_to_install diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index 9e101b442d..ccd341a862 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -12,10 +12,7 @@ if(HAVE_MC) add_executable(random_test random_test.c) add_executable(bugged1_liveness bugged1_liveness.c) add_executable(bugged2_liveness bugged2_liveness.c) - add_executable(centralized_liveness centralized_liveness.c) - add_executable(centralized_liveness_deadlock centralized_liveness_deadlock.c) - add_executable(test_snapshot test_snapshot.c) - add_executable(test/compare_snapshot test/compare_snapshot.c) + add_executable(test/test_heap_comparison test/test_heap_comparison.c) target_link_libraries(centralized simgrid m ) target_link_libraries(bugged1 simgrid m ) @@ -24,10 +21,7 @@ if(HAVE_MC) target_link_libraries(random_test simgrid m ) target_link_libraries(bugged1_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 ) - target_link_libraries(test/compare_snapshot simgrid m ) + target_link_libraries(test/test_heap_comparison simgrid m ) endif(HAVE_MC) @@ -45,7 +39,6 @@ set(xml_files ${CMAKE_CURRENT_SOURCE_DIR}/deploy_bugged2_liveness.xml ${CMAKE_CURRENT_SOURCE_DIR}/deploy_bugged2.xml ${CMAKE_CURRENT_SOURCE_DIR}/deploy_bugged3.xml - ${CMAKE_CURRENT_SOURCE_DIR}/deploy_centralized_liveness.xml ${CMAKE_CURRENT_SOURCE_DIR}/deploy_mutex.xml ${CMAKE_CURRENT_SOURCE_DIR}/deploy_random_test.xml ${CMAKE_CURRENT_SOURCE_DIR}/platform.xml @@ -57,28 +50,18 @@ set(examples_src ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.c ${CMAKE_CURRENT_SOURCE_DIR}/bugged2.c ${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.c - ${CMAKE_CURRENT_SOURCE_DIR}/bugged3.c - ${CMAKE_CURRENT_SOURCE_DIR}/centralized_liveness.c - ${CMAKE_CURRENT_SOURCE_DIR}/centralized_liveness_deadlock.c ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.c ${CMAKE_CURRENT_SOURCE_DIR}/random_test.c - ${CMAKE_CURRENT_SOURCE_DIR}/test_snapshot.c ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.h ${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.h - ${CMAKE_CURRENT_SOURCE_DIR}/centralized_liveness.h - ${CMAKE_CURRENT_SOURCE_DIR}/test_snapshot.h - ${CMAKE_CURRENT_SOURCE_DIR}/test/compare_snapshot.c + ${CMAKE_CURRENT_SOURCE_DIR}/test/test_heap_comparison.c PARENT_SCOPE ) set(bin_files ${bin_files} ${CMAKE_CURRENT_SOURCE_DIR}/parse_dwarf - ${CMAKE_CURRENT_SOURCE_DIR}/promela1_bugged1_liveness - ${CMAKE_CURRENT_SOURCE_DIR}/promela2_bugged1_liveness - ${CMAKE_CURRENT_SOURCE_DIR}/promela2_bugged2_liveness - ${CMAKE_CURRENT_SOURCE_DIR}/promela2_centralized_liveness + ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged1_liveness ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness - ${CMAKE_CURRENT_SOURCE_DIR}/promela_centralized_liveness PARENT_SCOPE ) set(txt_files diff --git a/examples/msg/mc/bugged1_liveness.c b/examples/msg/mc/bugged1_liveness.c index 8ef2d03528..37a287cdaa 100644 --- a/examples/msg/mc/bugged1_liveness.c +++ b/examples/msg/mc/bugged1_liveness.c @@ -125,7 +125,7 @@ int main(int argc, char *argv[]) MSG_init(&argc, argv); - MSG_config("model-check/property","promela1_bugged1_liveness"); + MSG_config("model-check/property","promela_bugged1_liveness"); MC_automaton_new_propositional_symbol("r", &predR); MC_automaton_new_propositional_symbol("cs", &predCS); diff --git a/examples/msg/mc/bugged1_liveness.h b/examples/msg/mc/bugged1_liveness.h index a33976881e..6ca2dfcd6f 100644 --- a/examples/msg/mc/bugged1_liveness.h +++ b/examples/msg/mc/bugged1_liveness.h @@ -1,10 +1,6 @@ #ifndef _BUGGED1_LIVENESS_H #define _BUGGED1_LIVENESS_H -int yyparse(void); -int yywrap(void); -int yylex(void); - int predR(void); int predCS(void); diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c index 03d9d6c709..fb7c2d854b 100644 --- a/examples/msg/mc/bugged2_liveness.c +++ b/examples/msg/mc/bugged2_liveness.c @@ -1,189 +1,108 @@ -/***************** 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) { + 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 { + 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; - 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[]) -{ - - 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 */ - 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"); - - /* 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 */ - 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"); - } - - /* 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[]) { - - 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); + MSG_config("model-check/property","promela_bugged2_liveness"); + MC_automaton_new_propositional_symbol("cs", &predCS); 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(); diff --git a/examples/msg/mc/bugged2_liveness.h b/examples/msg/mc/bugged2_liveness.h index 43b271bb33..b44121eff7 100644 --- a/examples/msg/mc/bugged2_liveness.h +++ b/examples/msg/mc/bugged2_liveness.h @@ -1,17 +1,9 @@ #ifndef _BUGGED2_LIVENESS_H #define _BUGGED2_LIVENESS_H -int yyparse(void); -int yywrap(void); -int yylex(void); - -int predPready(void); -int predCready(void); -int predConsume(void); -int predProduce(void); +int predCS(void); int coordinator(int argc, char *argv[]); -int producer(int argc, char *argv[]); -int consumer(int argc, char *argv[]); +int client(int argc, char *argv[]); #endif diff --git a/examples/msg/mc/centralized_liveness.c b/examples/msg/mc/centralized_liveness.c deleted file mode 100644 index 46425dedcc..0000000000 --- a/examples/msg/mc/centralized_liveness.c +++ /dev/null @@ -1,115 +0,0 @@ -/***************** 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 "centralized_liveness.h" - -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[]) -{ - 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); //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."); - msg_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"); - 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); - } - - 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]); - const char* kind; - - 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 answer = NULL; - MSG_task_receive(&answer, my_mailbox); - - kind = MSG_task_get_name(answer); - - 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; - - /*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); - } - - return 0; -} - -int main(int argc, char *argv[]) -{ - - MSG_init(&argc, argv); - - MSG_config("model-check/property","promela_centralized_liveness"); - MC_automaton_new_propositional_symbol("cs", &predCS); - - 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(); - - return 0; - -} diff --git a/examples/msg/mc/centralized_liveness.h b/examples/msg/mc/centralized_liveness.h deleted file mode 100644 index aa796a8d2b..0000000000 --- a/examples/msg/mc/centralized_liveness.h +++ /dev/null @@ -1,13 +0,0 @@ -#ifndef _CENTRALIZED_LIVENESS_H -#define _CENTRALIZED_LIVENESS_H - -int yyparse(void); -int yywrap(void); -int yylex(void); - -int predCS(void); - -int coordinator(int argc, char *argv[]); -int client(int argc, char *argv[]); - -#endif diff --git a/examples/msg/mc/centralized_liveness_deadlock.c b/examples/msg/mc/centralized_liveness_deadlock.c deleted file mode 100644 index 3e3fc3d619..0000000000 --- a/examples/msg/mc/centralized_liveness_deadlock.c +++ /dev/null @@ -1,112 +0,0 @@ -/***************** 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 "centralized_liveness.h" - -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) { - msg_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"); - 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 - 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 - msg_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[]) -{ - - MSG_init(&argc, argv); - - MSG_config("model-check/property","promela_centralized_liveness"); - MC_automaton_new_propositional_symbol("cs", &predCS); - - 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(); - - return 0; - -} diff --git a/examples/msg/mc/deploy_bugged2_liveness.xml b/examples/msg/mc/deploy_bugged2_liveness.xml index 3aa65c151c..b932a9cb52 100644 --- a/examples/msg/mc/deploy_bugged2_liveness.xml +++ b/examples/msg/mc/deploy_bugged2_liveness.xml @@ -6,13 +6,12 @@ - + - + - diff --git a/examples/msg/mc/deploy_centralized_liveness.xml b/examples/msg/mc/deploy_centralized_liveness.xml deleted file mode 100644 index bd46ad782e..0000000000 --- a/examples/msg/mc/deploy_centralized_liveness.xml +++ /dev/null @@ -1,47 +0,0 @@ - - - - - - - - - - - - - - - - - - - diff --git a/examples/msg/mc/promela2_bugged1_liveness b/examples/msg/mc/promela2_bugged1_liveness deleted file mode 100644 index febfac5aab..0000000000 --- a/examples/msg/mc/promela2_bugged1_liveness +++ /dev/null @@ -1,11 +0,0 @@ -never { /* !(G((!cs) -> F(cs))) */ -T0_init : /* init */ - if - :: (1) -> goto T0_init - :: (!cs) -> goto accept_S2 - fi; -accept_S2 : /* 1 */ - if - :: (!cs) -> goto accept_S2 - fi; -} diff --git a/examples/msg/mc/promela2_bugged2_liveness b/examples/msg/mc/promela2_bugged2_liveness deleted file mode 100644 index 1b4359d9f6..0000000000 --- a/examples/msg/mc/promela2_bugged2_liveness +++ /dev/null @@ -1,17 +0,0 @@ -never { /* !(G((pready U produce) -> F(cready U consume))) */ -T1_init : /* init */ - if - :: (1) -> goto T1_init - :: (pready && !consume) -> goto T0_S2 - :: (produce && !consume) -> goto accept_S3 - fi; -T0_S2 : /* 1 */ - if - :: (pready && !consume) -> goto T0_S2 - :: (produce && !consume) -> goto accept_S3 - fi; -accept_S3 : /* 2 */ - if - :: (!consume) -> goto accept_S3 - fi; -} diff --git a/examples/msg/mc/promela2_centralized_liveness b/examples/msg/mc/promela2_centralized_liveness deleted file mode 100644 index 94bbde252e..0000000000 --- a/examples/msg/mc/promela2_centralized_liveness +++ /dev/null @@ -1,11 +0,0 @@ -never { /* !(GFcs) */ -T0_init : /* init */ - if - :: (1) -> goto T0_init - :: (!cs) -> goto accept_S2 - fi; -accept_S2 : /* 1 */ - if - :: (!cs) -> goto accept_S2 - fi; -} diff --git a/examples/msg/mc/promela1_bugged1_liveness b/examples/msg/mc/promela_bugged1_liveness similarity index 100% rename from examples/msg/mc/promela1_bugged1_liveness rename to examples/msg/mc/promela_bugged1_liveness diff --git a/examples/msg/mc/promela_bugged2_liveness b/examples/msg/mc/promela_bugged2_liveness index 5d5edc9ddc..5361f88099 100644 --- a/examples/msg/mc/promela_bugged2_liveness +++ b/examples/msg/mc/promela_bugged2_liveness @@ -1,23 +1,12 @@ -never { /* !(GF((pready U produce) -> (cready U consume))) */ +never { /* !(!(GFcs)) */ T0_init : /* init */ if - :: (1) -> goto T1_S1 - :: (produce && !consume) -> goto accept_S5 - :: (pready && !consume) -> goto T0_S5 + :: (cs) -> goto accept_S1 + :: (1) -> goto T0_init fi; -T1_S1 : /* 1 */ +accept_S1 : /* 1 */ if - :: (1) -> goto T1_S1 - :: (produce && !consume) || (pready && !consume) -> goto accept_S5 + :: (cs) -> goto accept_S1 + :: (1) -> goto T0_init fi; -accept_S5 : /* 2 */ - if - :: (pready && !consume) -> goto T0_S5 - :: (produce && !consume) -> goto accept_S5 - fi; -T0_S5 : /* 3 */ - if - :: (pready && !consume) -> goto T0_S5 - :: (produce && !consume) -> goto accept_S5 - fi; -} \ No newline at end of file +} diff --git a/examples/msg/mc/promela_centralized_liveness b/examples/msg/mc/promela_centralized_liveness deleted file mode 100644 index 5361f88099..0000000000 --- a/examples/msg/mc/promela_centralized_liveness +++ /dev/null @@ -1,12 +0,0 @@ -never { /* !(!(GFcs)) */ -T0_init : /* init */ - if - :: (cs) -> goto accept_S1 - :: (1) -> goto T0_init - fi; -accept_S1 : /* 1 */ - if - :: (cs) -> goto accept_S1 - :: (1) -> goto T0_init - fi; -} diff --git a/examples/msg/mc/test/compare_snapshot.c b/examples/msg/mc/test/test_heap_comparison.c similarity index 77% rename from examples/msg/mc/test/compare_snapshot.c rename to examples/msg/mc/test/test_heap_comparison.c index fa3d1d2f19..c094f46eaa 100644 --- a/examples/msg/mc/test/compare_snapshot.c +++ b/examples/msg/mc/test/test_heap_comparison.c @@ -3,6 +3,6 @@ int main (int argc, char **argv){ MSG_init(&argc, argv); - MC_test_snapshot_comparison(); + MC_test_heap_comparison(); return 0; } diff --git a/examples/msg/mc/test_snapshot.c b/examples/msg/mc/test_snapshot.c deleted file mode 100644 index 32b6165d2b..0000000000 --- a/examples/msg/mc/test_snapshot.c +++ /dev/null @@ -1,144 +0,0 @@ -#include "msg/msg.h" -#include "mc/mc.h" -#include "xbt/automaton.h" -#include "test_snapshot.h" -//#include "y.tab.c" -#include - -XBT_LOG_NEW_DEFAULT_CATEGORY(test_snapshot, "my log messages"); - -int r=0; -int cs=0; - -int i = 1; -xbt_dynar_t d1 = NULL; -xbt_dynar_t d2 = NULL; -char *c1; - -int predR(){ - return r; -} - -int predCS(){ - return cs; -} - -void check(){ - XBT_INFO("*** Check ***"); - if(d1!=NULL){ - XBT_INFO("Dynar d1 (%p -> %p) length : %lu", &d1, d1, xbt_dynar_length(d1)); - unsigned int cursor = 0; - char *elem; - xbt_dynar_foreach(d1, cursor, elem){ - XBT_INFO("Elem in dynar d1 : %s", elem); - } - }else{ - XBT_INFO("Dynar d1 NULL"); - } - if(d2!=NULL){ - XBT_INFO("Dynar d2 (%p -> %p) length : %lu", &d2, d2, xbt_dynar_length(d2)); - unsigned int cursor = 0; - char *elem; - xbt_dynar_foreach(d2, cursor, elem){ - XBT_INFO("Elem in dynar d2 : %s", elem); - } - }else{ - XBT_INFO("Dynar d2 NULL"); - } -} - - -int coordinator(int argc, char *argv[]) -{ - - while(i>0){ - - msg_task_t task = NULL; - MSG_task_receive(&task, "coordinator"); - const char *kind = MSG_task_get_name(task); - - //check(); - - if (!strcmp(kind, "request")) { - char *req = MSG_task_get_data(task); - msg_task_t answer = MSG_task_create("received", 0, 1000, NULL); - MSG_task_send(answer, req); - }else{ - XBT_INFO("End of coordinator"); - } - - } - - 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(i>0){ - - XBT_INFO("Ask the request"); - MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator"); - - r = 1; - - check(); - - // wait the answer - msg_task_t task = NULL; - MSG_task_receive(&task, my_mailbox); - MSG_task_destroy(task); - - check(); - - XBT_INFO("*** Update ***"); - xbt_dynar_reset(d1); - free(c1); - xbt_dynar_free(&d1); - d2 = xbt_dynar_new(sizeof(char *), NULL); - XBT_INFO("Dynar d2 : %p -> %p", &d2, d2); - char *c2 = strdup("boooooooo"); - xbt_dynar_push(d2, &c2); - - cs = 1; - - check(); - - MSG_process_sleep(1); - MSG_task_send(MSG_task_create("release", 0, 1000, NULL), "coordinator"); - - check(); - - MSG_process_sleep(my_pid); - - i--; - } - - return 0; -} - -int main(int argc, char *argv[]) { - - MSG_init(&argc, argv); - - d1 = xbt_dynar_new(sizeof(char *), NULL); - XBT_DEBUG("Dynar d1 : %p -> %p", &d1, d1); - c1 = strdup("coucou"); - xbt_dynar_push(d1, &c1); - xbt_dynar_push(d1, &c1); - - MSG_config("model-check/property","promela_test_snapshot"); - MC_automaton_new_propositional_symbol("r", &predR); - MC_automaton_new_propositional_symbol("cs", &predCS); - - MSG_create_environment("../msg_platform.xml"); - MSG_function_register("coordinator", coordinator); - MSG_function_register("client", client); - MSG_launch_application("deploy_test_snapshot.xml"); - MSG_main(); - - return 0; -} diff --git a/examples/msg/mc/test_snapshot.h b/examples/msg/mc/test_snapshot.h deleted file mode 100644 index 118aaac6b2..0000000000 --- a/examples/msg/mc/test_snapshot.h +++ /dev/null @@ -1,16 +0,0 @@ -#ifndef _TEST_SNAPSHOT_H -#define _TEST_SNAPSHOT_H - -int yyparse(void); -int yywrap(void); -int yylex(void); - -int predCS(void); -int predR(void); - -int coordinator(int argc, char *argv[]); -int client(int argc, char *argv[]); - -void check(void); - -#endif diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 3d4647f379..0a9ae5bd84 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -49,7 +49,7 @@ XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */ XBT_PUBLIC(void) MC_memory_exit(void); /********************************* Snapshot comparison test *************************************/ -void MC_test_snapshot_comparison(void); +void MC_test_heap_comparison(void); /* Trigger for state equality detection (check potential cycle in application) */ void MC_compare(void); diff --git a/src/mc/test/compare_snapshot.c b/src/mc/test/heap_comparison.c similarity index 86% rename from src/mc/test/compare_snapshot.c rename to src/mc/test/heap_comparison.c index 5a3fdfe523..60e2222c5f 100644 --- a/src/mc/test/compare_snapshot.c +++ b/src/mc/test/heap_comparison.c @@ -10,7 +10,7 @@ static void test6(void); static void test1() { - fprintf(stderr, "\n**************** TEST 1 ****************\n\n"); + fprintf(stderr, "\n**************** TEST 1 ****************\nNo modification (successive snapshot)\n"); MC_SET_RAW_MEM; /* Save first snapshot */ @@ -38,7 +38,7 @@ static void test1() static void test2() { - fprintf(stderr, "\n**************** TEST 2 ****************\n\n"); + fprintf(stderr, "\n**************** TEST 2 ****************\nMalloc after first snapshot\n"); MC_SET_RAW_MEM; @@ -76,7 +76,7 @@ static void test2() static void test3() { - fprintf(stderr, "\n**************** TEST 3 ****************\n\n"); + fprintf(stderr, "\n**************** TEST 3 ****************\nMalloc and free after first snapshot\n"); MC_SET_RAW_MEM; @@ -113,7 +113,7 @@ static void test3() static void test4() { - fprintf(stderr, "\n**************** TEST 4 ****************\n\n"); + fprintf(stderr, "\n**************** TEST 4 ****************\nMalloc before first snapshot and free after first snapshot\n"); char *t = malloc(5); t = strdup("toto"); @@ -152,7 +152,7 @@ static void test4() static void test5() { - fprintf(stderr, "\n**************** TEST 5 ****************\n\n"); + fprintf(stderr, "\n**************** TEST 5 ****************\nMalloc before first snapshot and increment pointer after first snapshot\n"); char *ptr1 = malloc(sizeof(char *)); @@ -189,7 +189,7 @@ static void test5() static void test6() { - fprintf(stderr, "\n**************** TEST 6 ****************\n\n"); + fprintf(stderr, "\n**************** TEST 6 ****************\nMalloc before first snapshot and increment then decrement pointer after first snapshot\n"); char *ptr1 = malloc(sizeof(char *)); @@ -225,13 +225,15 @@ static void test6() } -void MC_test_snapshot_comparison(){ +void MC_test_heap_comparison(){ MC_memory_init(); MC_SET_RAW_MEM; + mc_snapshot_t initial = xbt_new0(s_mc_snapshot_t, 1); MC_take_snapshot_liveness(initial); + MC_UNSET_RAW_MEM; /* Get .plt section (start and end addresses) for data libsimgrid comparison */ -- 2.20.1