From 059291b87112991d41f426698f45afea178efb0b Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 11 Jan 2012 15:05:57 +0100 Subject: [PATCH] model-checker : new example for liveness properties --- examples/msg/mc/centralized_liveness.c | 108 ++++++++++++++++++ examples/msg/mc/centralized_liveness.h | 13 +++ .../msg/mc/deploy_centralized_liveness.xml | 47 ++++++++ examples/msg/mc/promela_centralized_liveness | 11 ++ 4 files changed, 179 insertions(+) create mode 100644 examples/msg/mc/centralized_liveness.c create mode 100644 examples/msg/mc/centralized_liveness.h create mode 100644 examples/msg/mc/deploy_centralized_liveness.xml create mode 100644 examples/msg/mc/promela_centralized_liveness diff --git a/examples/msg/mc/centralized_liveness.c b/examples/msg/mc/centralized_liveness.c new file mode 100644 index 0000000000..350c59bb85 --- /dev/null +++ b/examples/msg/mc/centralized_liveness.c @@ -0,0 +1,108 @@ +#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" + +#define AMOUNT_OF_CLIENTS 2 +#define CS_PER_PROCESS 1 + +XBT_LOG_NEW_DEFAULT_CATEGORY(centralized, "my log messages"); + +int cs2 = 0; + +int predCS2(){ + return cs2; +} + + +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){ + + if(!strcmp(my_mailbox, "2")) + cs2 = 0; + + XBT_INFO("Client (%s) ask 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"); + + if(!strcmp(my_mailbox, "2")) + cs2 = 1; + + MSG_process_sleep(1); + MSG_task_send(MSG_task_create("release", 0, 1000, NULL), + "coordinator"); + MSG_process_sleep(my_pid); + } + + return 0; +} + +int main(int argc, char *argv[]) +{ + init(); + yyparse(); + automaton = get_automaton(); + xbt_new_propositional_symbol(automaton,"cs2", &predCS2); + + 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; + +} diff --git a/examples/msg/mc/centralized_liveness.h b/examples/msg/mc/centralized_liveness.h new file mode 100644 index 0000000000..1c140317e3 --- /dev/null +++ b/examples/msg/mc/centralized_liveness.h @@ -0,0 +1,13 @@ +#ifndef _CENTRALIZED_LIVENESS_H +#define _CENTRALIZED_LIVENESS_H + +int yyparse(void); +int yywrap(void); +int yylex(void); + +int predCS2(void); + +int coordinator(int argc, char *argv[]); +int client(int argc, char *argv[]); + +#endif diff --git a/examples/msg/mc/deploy_centralized_liveness.xml b/examples/msg/mc/deploy_centralized_liveness.xml new file mode 100644 index 0000000000..bd46ad782e --- /dev/null +++ b/examples/msg/mc/deploy_centralized_liveness.xml @@ -0,0 +1,47 @@ + + + + + + + + + + + + + + + + + + + diff --git a/examples/msg/mc/promela_centralized_liveness b/examples/msg/mc/promela_centralized_liveness new file mode 100644 index 0000000000..c5169d114f --- /dev/null +++ b/examples/msg/mc/promela_centralized_liveness @@ -0,0 +1,11 @@ +never { /* !(GFcs2) */ +T0_init : /* init */ + if + :: (1) -> goto T0_init + :: (!cs2) -> goto accept_S2 + fi; +accept_S2 : /* 1 */ + if + :: (!cs2) -> goto accept_S2 + fi; +} \ No newline at end of file -- 2.20.1