1 /* Copyright (c) 2014. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
11 #include <simgrid/simix.h>
13 #include "mc_record.h"
17 #include "mc_private.h"
18 #include "mc_model_checker.h"
22 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc,
23 " Logging specific to MC record/replay facility");
25 char* MC_record_path = NULL;
27 void MC_record_replay(mc_record_item_t start, size_t len)
29 MC_wait_for_requests();
30 mc_record_item_t end = start + len;
32 // Choose the recorded simcall and execute it:
33 for (mc_record_item_t item=start;item!=end; ++item) {
35 XBT_DEBUG("Executing %i$%i", item->pid, item->value);
37 if (xbt_dynar_is_empty(simix_global->process_to_run))
38 xbt_die("Unexpected end of application.");
42 smx_process_t process = SIMIX_process_from_PID(item->pid);
44 xbt_die("Unexpected process.");
45 smx_simcall_t simcall = &(process->simcall);
46 if(!simcall || simcall->call == SIMCALL_NONE)
47 xbt_die("No simcall for this process.");
48 if (!MC_request_is_visible(simcall) || !MC_request_is_enabled(simcall))
49 xbt_die("Unexpected simcall.");
51 // Execute the request:
52 SIMIX_simcall_handle(simcall, item->value);
53 MC_wait_for_requests();
57 xbt_dynar_t MC_record_from_string(const char* data)
59 XBT_INFO("path=%s", data);
60 if (!data || !data[0])
63 xbt_dynar_t dynar = xbt_dynar_new(sizeof(s_mc_record_item_t), NULL);
65 const char* current = data;
68 s_mc_record_item_t item = { 0, 0 };
69 int count = sscanf(current, "%u/%u", &item.pid, &item.value);
70 if(count != 2 && count != 1)
72 xbt_dynar_push(dynar, &item);
75 char* end = strchr(current, ';');
85 xbt_dynar_free(&dynar);
90 char* MC_record_stack_to_string(xbt_fifo_t stack)
92 xbt_fifo_item_t start = xbt_fifo_get_last_item(stack);
95 char* res = (char*) malloc(1 * sizeof(char));
102 FILE* file = open_memstream(&buffer, &size);
104 xbt_fifo_item_t item;
105 for (item = start; item; item = xbt_fifo_get_prev_item(item)) {
107 // Find (pid, value):
108 mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item);
110 smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
111 int pid = saved_req->issuer->pid;
113 // Serialization the (pid, value) pair:
114 const char* sep = (item!=start) ? ";" : "";
116 fprintf(file, "%s%u/%u", sep, pid, value);
118 fprintf(file, "%s%u", sep, pid);
125 void MC_record_dump_path(xbt_fifo_t stack)
127 if (MC_record_is_active()) {
128 char* path = MC_record_stack_to_string(stack);
129 XBT_INFO("Path = %s", path);
135 void MC_record_replay_from_string(const char* path_string)
137 xbt_dynar_t path = MC_record_from_string(path_string);
138 mc_record_item_t start = &xbt_dynar_get_as(path, 0, s_mc_record_item_t);
139 MC_record_replay(start, xbt_dynar_length(path));
140 xbt_dynar_free(&path);
143 void MC_record_replay_init()
145 mc_time = xbt_new0(double, simix_process_maxpid);