@CMAKE_HOME_DIRECTORY@/examples/msg/icomms/peer2.c \
@CMAKE_HOME_DIRECTORY@/examples/msg/icomms/peer3.c \
@CMAKE_HOME_DIRECTORY@/examples/msg/process-suspend/process-suspend.c \
+ @CMAKE_HOME_DIRECTORY@/examples/msg/process-kill/process-kill.c \
@CMAKE_HOME_DIRECTORY@/examples/msg/process-migration/process-migration.c \
@CMAKE_HOME_DIRECTORY@/examples/msg/task-priority/task-priority.c \
@CMAKE_HOME_DIRECTORY@/examples/msg/properties \
#include "simgrid/msg.h"
-XBT_LOG_NEW_DEFAULT_CATEGORY(msg_test, "Messages specific for this msg example");
+XBT_LOG_NEW_DEFAULT_CATEGORY(msg_process_kill, "Messages specific for this msg example");
+/** @addtogroup MSG_examples
+ *
+ * - <b>Process Killing: process-kill/process-kill.c</b>. Processes can also be killed by another if needed thanks to
+ * the @ref MSG_process_kill function.
+ */
static int victim(int argc, char *argv[])
{
XBT_INFO("Hello!");
XBT_INFO("Suspending myself");
- MSG_process_suspend(MSG_process_self());
- XBT_INFO("OK, OK. Let's work");
+ MSG_process_suspend(MSG_process_self()); /** - First suspend itself */
+ XBT_INFO("OK, OK. Let's work"); /** - Then is resumed and start to execute a task */
MSG_task_execute(MSG_task_create("work", 1e9, 0, NULL));
- XBT_INFO("Bye!");
+ XBT_INFO("Bye!"); /** - But will never reach the end of it */
return 0;
}
static int killer(int argc, char *argv[])
{
- msg_process_t poor_victim = NULL;
-
- XBT_INFO("Hello!");
- poor_victim = MSG_process_create("victim", victim, NULL, MSG_host_by_name("Fafard"));
+ XBT_INFO("Hello!"); /** - First start a @ref victim process */
+ msg_process_t poor_victim = MSG_process_create("victim", victim, NULL, MSG_host_by_name("Fafard"));
MSG_process_sleep(10.0);
- XBT_INFO("Resume process");
+ XBT_INFO("Resume process"); /** - Resume it from its suspended state */
MSG_process_resume(poor_victim);
- XBT_INFO("Kill process");
+ XBT_INFO("Kill process"); /** - and then kill it */
MSG_process_kill(poor_victim);
XBT_INFO("OK, goodbye now.");
MSG_init(&argc, argv);
xbt_assert(argc == 2, "Usage: %s platform_file\n\tExample: %s msg_platform.xml\n", argv[0], argv[0]);
- MSG_create_environment(argv[1]);
-
+ MSG_create_environment(argv[1]); /** - Load the platform description */
+ /** - Create and deploy @ref killer process */
MSG_function_register("killer", killer);
MSG_function_register("victim", victim);
MSG_process_create("killer", killer, NULL, MSG_host_by_name("Tremblay"));
- res = MSG_main();
+ res = MSG_main(); /** - Run the simulation */
XBT_INFO("Simulation time %g", MSG_get_clock());
-
return res != MSG_OK;
}
p Testing a MSG_process_kill function
-$ $SG_TEST_EXENV ${bindir:=.}/process-kill ${srcdir:=.}/small_platform.xml --log=surf_maxmin.thres:error
-> [Tremblay:killer:(1) 0.000000] [msg_test/INFO] Hello!
-> [Fafard:victim:(2) 0.000000] [msg_test/INFO] Hello!
-> [Fafard:victim:(2) 0.000000] [msg_test/INFO] Suspending myself
-> [Tremblay:killer:(1) 10.000000] [msg_test/INFO] Resume process
-> [Tremblay:killer:(1) 10.000000] [msg_test/INFO] Kill process
-> [Tremblay:killer:(1) 10.000000] [msg_test/INFO] OK, goodbye now.
-> [10.000000] [msg_test/INFO] Simulation time 10
+$ $SG_TEST_EXENV ${bindir:=.}/process-kill ${srcdir:=.}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
+> [ 0.000000] (1:killer@Tremblay) Hello!
+> [ 0.000000] (2:victim@Fafard) Hello!
+> [ 0.000000] (2:victim@Fafard) Suspending myself
+> [ 10.000000] (1:killer@Tremblay) Resume process
+> [ 10.000000] (1:killer@Tremblay) Kill process
+> [ 10.000000] (1:killer@Tremblay) OK, goodbye now.
+> [ 10.000000] (0:maestro@) Simulation time 10
extern XBT_PRIVATE int _sg_mc_checkpoint;
extern XBT_PUBLIC(int) _sg_mc_sparse_checkpoint;
extern XBT_PUBLIC(int) _sg_mc_ksm;
-extern XBT_PUBLIC(int) _sg_mc_soft_dirty;
extern XBT_PUBLIC(char*) _sg_mc_property_file;
extern XBT_PRIVATE int _sg_mc_timeout;
extern XBT_PRIVATE int _sg_mc_hash;
XBT_PRIVATE void _mc_cfg_cb_checkpoint(const char *name);
XBT_PRIVATE void _mc_cfg_cb_sparse_checkpoint(const char *name);
XBT_PRIVATE void _mc_cfg_cb_ksm(const char *name);
-XBT_PRIVATE void _mc_cfg_cb_soft_dirty(const char *name);
XBT_PRIVATE void _mc_cfg_cb_property(const char *name);
XBT_PRIVATE void _mc_cfg_cb_timeout(const char *name);
XBT_PRIVATE void _mc_cfg_cb_snapshot_fds(const char *name);
#include "src/mc/ChunkedData.hpp"
#include "src/mc/PageStore.hpp"
-#define SOFT_DIRTY_BIT_NUMBER 55
-#define SOFT_DIRTY (((uint64_t)1) << SOFT_DIRTY_BIT_NUMBER)
-
namespace simgrid {
namespace mc {
* @return Snapshot page numbers of this new snapshot
*/
ChunkedData::ChunkedData(PageStore& store, AddressSpace& as,
- RemotePtr<void> addr, std::size_t page_count,
- const std::size_t* ref_page_numbers, const std::uint64_t* pagemap)
+ RemotePtr<void> addr, std::size_t page_count)
{
store_ = &store;
this->pagenos_.resize(page_count);
for (size_t i = 0; i != page_count; ++i) {
- // We don't have to compare soft-clean pages:
- if (ref_page_numbers && pagemap && !(pagemap[i] & SOFT_DIRTY)) {
- pagenos_[i] = ref_page_numbers[i];
- store_->ref_page(ref_page_numbers[i]);
- continue;
- }
-
RemotePtr<void> page = remote((void*)
simgrid::mc::mmu::join(i, addr.address()));
xbt_assert(simgrid::mc::mmu::split(page.address()).second == 0,
}
ChunkedData(PageStore& store, AddressSpace& as,
- RemotePtr<void> addr, std::size_t page_count,
- const std::size_t* ref_page_numbers, const std::uint64_t* pagemap);
+ RemotePtr<void> addr, std::size_t page_count);
};
}
}
}
-static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
+namespace simgrid {
+namespace mc {
+
+void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
simgrid::mc::PatternCommunicationList* list =
xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
if (diff != NONE_DIFF) {
if (comm->type == SIMIX_COMM_SEND){
- simgrid::mc::initial_global_state->send_deterministic = 0;
- if(simgrid::mc::initial_global_state->send_diff != nullptr)
- xbt_free(simgrid::mc::initial_global_state->send_diff);
- simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
+ this->send_deterministic = 0;
+ if (this->send_diff != nullptr)
+ xbt_free(this->send_diff);
+ this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
}else{
- simgrid::mc::initial_global_state->recv_deterministic = 0;
- if(simgrid::mc::initial_global_state->recv_diff != nullptr)
- xbt_free(simgrid::mc::initial_global_state->recv_diff);
- simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
+ this->recv_deterministic = 0;
+ if (this->recv_diff != nullptr)
+ xbt_free(this->recv_diff);
+ this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
}
- if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){
+ if(_sg_mc_send_determinism && !this->send_deterministic){
XBT_INFO("*********************************************************");
XBT_INFO("***** Non-send-deterministic communications pattern *****");
XBT_INFO("*********************************************************");
- XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
- xbt_free(simgrid::mc::initial_global_state->send_diff);
- simgrid::mc::initial_global_state->send_diff = nullptr;
+ XBT_INFO("%s", this->send_diff);
+ xbt_free(this->send_diff);
+ this->send_diff = nullptr;
simgrid::mc::session->logState();
mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
}else if(_sg_mc_comms_determinism
- && (!simgrid::mc::initial_global_state->send_deterministic
- && !simgrid::mc::initial_global_state->recv_deterministic)) {
+ && (!this->send_deterministic && !this->recv_deterministic)) {
XBT_INFO("****************************************************");
XBT_INFO("***** Non-deterministic communications pattern *****");
XBT_INFO("****************************************************");
- XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
- XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
- xbt_free(simgrid::mc::initial_global_state->send_diff);
- simgrid::mc::initial_global_state->send_diff = nullptr;
- xbt_free(simgrid::mc::initial_global_state->recv_diff);
- simgrid::mc::initial_global_state->recv_diff = nullptr;
+ XBT_INFO("%s", this->send_diff);
+ XBT_INFO("%s", this->recv_diff);
+ xbt_free(this->send_diff);
+ this->send_diff = nullptr;
+ xbt_free(this->recv_diff);
+ this->recv_diff = nullptr;
simgrid::mc::session->logState();
mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
}
/********** Non Static functions ***********/
-void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
+void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
{
const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
remote(synchro.comm.src_buff));
}
if(mpi_request.detached){
- if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
+ if (!this->initial_communications_pattern_done) {
/* Store comm pattern */
simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
initial_communications_pattern, pattern->src_proc,
list->list.push_back(std::move(pattern));
} else {
/* Evaluate comm determinism */
- deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
+ this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
xbt_dynar_get_as(
initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
)->index_comm++;
xbt_dynar_push(dynar, &pattern2);
}
-void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
+
+void CommunicationDeterminismChecker::complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking)
+{
simgrid::mc::PatternCommunication* current_comm_pattern;
unsigned int cursor = 0;
std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
- if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
+ if (!this->initial_communications_pattern_done)
/* Store comm pattern */
pattern->list.push_back(std::move(comm_pattern));
else {
/* Evaluate comm determinism */
- deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
+ this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
pattern->index_comm++;
}
}
-
-/************************ Main algorithm ************************/
-
-namespace simgrid {
-namespace mc {
-
CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
: Checker(session)
{
{
Checker::logState();
if (_sg_mc_comms_determinism &&
- !simgrid::mc::initial_global_state->recv_deterministic &&
- simgrid::mc::initial_global_state->send_deterministic) {
+ !this->recv_deterministic &&
+ this->send_deterministic) {
XBT_INFO("******************************************************");
XBT_INFO("**** Only-send-deterministic communication pattern ****");
XBT_INFO("******************************************************");
- XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
+ XBT_INFO("%s", this->recv_diff);
} else if(_sg_mc_comms_determinism &&
- !simgrid::mc::initial_global_state->send_deterministic &&
- simgrid::mc::initial_global_state->recv_deterministic) {
+ !this->send_deterministic &&
+ this->recv_deterministic) {
XBT_INFO("******************************************************");
XBT_INFO("**** Only-recv-deterministic communication pattern ****");
XBT_INFO("******************************************************");
- XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
+ XBT_INFO("%s", this->send_diff);
}
XBT_INFO("Expanded states = %lu", expandedStatesCount_);
XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
- if (simgrid::mc::initial_global_state != nullptr)
- XBT_INFO("Send-deterministic : %s",
- !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes");
- if (simgrid::mc::initial_global_state != nullptr && _sg_mc_comms_determinism)
+ XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
+ if (_sg_mc_comms_determinism)
XBT_INFO("Recv-deterministic : %s",
- !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes");
+ !this->recv_deterministic ? "No" : "Yes");
}
void CommunicationDeterminismChecker::prepare()
return true;
}
+void CommunicationDeterminismChecker::restoreState()
+{
+ /* Intermediate backtracking */
+ {
+ simgrid::mc::State* state = stack_.back().get();
+ if (state->system_state) {
+ simgrid::mc::restore_snapshot(state->system_state);
+ MC_restore_communications_pattern(state);
+ return;
+ }
+ }
+
+ /* Restore the initial state */
+ simgrid::mc::session->restoreInitialState();
+
+ // int n = xbt_dynar_length(incomplete_communications_pattern);
+ unsigned n = MC_smx_get_maxpid();
+ assert(n == xbt_dynar_length(incomplete_communications_pattern));
+ assert(n == xbt_dynar_length(initial_communications_pattern));
+ for (unsigned j=0; j < n ; j++) {
+ xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
+ xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
+ }
+
+ /* Traverse the stack from the state at position start and re-execute the transitions */
+ for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
+ if (state == stack_.back())
+ break;
+
+ int req_num = state->transition.argument;
+ smx_simcall_t saved_req = &state->executed_req;
+ xbt_assert(saved_req);
+
+ /* because we got a copy of the executed request, we have to fetch the
+ real one, pointed by the request field of the issuer process */
+
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ smx_simcall_t req = &issuer->simcall;
+
+ /* TODO : handle test and testany simcalls */
+ e_mc_call_type_t call = MC_get_call_type(req);
+ mc_model_checker->handle_simcall(state->transition);
+ MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
+ mc_model_checker->wait_for_requests();
+
+ /* Update statistics */
+ mc_model_checker->visited_states++;
+ mc_model_checker->executed_transitions++;
+ }
+}
+
int CommunicationDeterminismChecker::main(void)
{
std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
mc_model_checker->handle_simcall(state->transition);
/* After this call req is no longer useful */
- if(!initial_global_state->initial_communications_pattern_done)
+ if (!this->initial_communications_pattern_done)
MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
else
MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
These communications are incomplete and they cannot be analyzed and
compared with the initial pattern. */
bool compare_snapshots = all_communications_are_finished()
- && initial_global_state->initial_communications_pattern_done;
+ && this->initial_communications_pattern_done;
if (_sg_mc_visited == 0
|| (visited_state = visitedStates_.addVisitedState(
XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
stack_.size());
- if (!initial_global_state->initial_communications_pattern_done)
- initial_global_state->initial_communications_pattern_done = 1;
+ if (!this->initial_communications_pattern_done)
+ this->initial_communications_pattern_done = 1;
/* Trash the current state, no longer needed */
XBT_DEBUG("Delete state %d at depth %zi",
state->num, stack_.size() + 1);
stack_.push_back(std::move(state));
- simgrid::mc::replay(stack_);
+ this->restoreState();
XBT_DEBUG("Back-tracking to state %d at depth %zi done",
stack_.back()->num, stack_.size());
int CommunicationDeterminismChecker::run()
{
XBT_INFO("Check communication determinism");
- mc_model_checker->wait_for_requests();
+ simgrid::mc::session->initialize();
this->prepare();
- initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
- initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
- initial_global_state->initial_communications_pattern_done = 0;
- initial_global_state->recv_deterministic = 1;
- initial_global_state->send_deterministic = 1;
- initial_global_state->recv_diff = nullptr;
- initial_global_state->send_diff = nullptr;
+ this->initial_communications_pattern_done = 0;
+ this->recv_deterministic = 1;
+ this->send_deterministic = 1;
+ this->recv_diff = nullptr;
+ this->send_diff = nullptr;
int res = this->main();
- initial_global_state = nullptr;
return res;
}
void prepare();
int main();
void logState() override;
+ void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking);
+ void restoreState();
+public:
+ // These are used by functions which should be moved in CommunicationDeterminismChecker:
+ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking);
+ void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
private:
/** Stack representing the position in the exploration graph */
std::list<std::unique_ptr<simgrid::mc::State>> stack_;
simgrid::mc::VisitedStates visitedStates_;
unsigned long expandedStatesCount_ = 0;
+
+ int initial_communications_pattern_done = 0;
+ int recv_deterministic = 0;
+ int send_deterministic = 0;
+ char *send_diff = nullptr;
+ char *recv_diff = nullptr;
};
#endif
explorationStack_.pop_back();
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
- initial_global_state->prev_pair, pair_test->num,
- initial_global_state->prev_req.c_str());
+ this->previousPair_, pair_test->num,
+ this->previousRequest_.c_str());
return nullptr;
}
void LivenessChecker::prepare(void)
{
- initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
- initial_global_state->prev_pair = 0;
+ this->previousPair_ = 0;
std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
}
/* Restore the initial state */
- simgrid::mc::restore_snapshot(initial_global_state->snapshot);
+ simgrid::mc::session->restoreInitialState();
/* Traverse the stack from the initial state and re-execute the transitions */
int depth = 1;
reached_pair, current_pair.get())) != -1) {
if (dot_output != nullptr){
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
- initial_global_state->prev_pair, visited_num,
- initial_global_state->prev_req.c_str());
+ this->previousPair_, visited_num,
+ this->previousRequest_.c_str());
fflush(dot_output);
}
XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
int req_num = current_pair->graph_state->transition.argument;
if (dot_output != nullptr) {
- if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
+ if (this->previousPair_ != 0 && this->previousPair_ != current_pair->num) {
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
- initial_global_state->prev_pair, current_pair->num,
- initial_global_state->prev_req.c_str());
- initial_global_state->prev_req.clear();
+ this->previousPair_, current_pair->num,
+ this->previousRequest_.c_str());
+ this->previousRequest_.clear();
}
- initial_global_state->prev_pair = current_pair->num;
- initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, req_num);
+ this->previousPair_ = current_pair->num;
+ this->previousRequest_ = simgrid::mc::request_get_dot_output(req, req_num);
if (current_pair->search_cycle)
fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
fflush(dot_output);
{
XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
MC_automaton_load(_sg_mc_property_file);
- mc_model_checker->wait_for_requests();
XBT_DEBUG("Starting the liveness algorithm");
-
- /* Create the initial state */
- simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
-
+ simgrid::mc::session->initialize();
this->prepare();
+
int res = this->main();
- simgrid::mc::initial_global_state = nullptr;
return res;
}
unsigned long visitedPairsCount_ = 0;
unsigned long expandedPairsCount_ = 0;
unsigned long expandedStatesCount_ = 0;
+ int previousPair_ = 0;
+ std::string previousRequest_;
};
}
* The first (lower) layer of the per-page snapshot mechanism is a page
* store: its responsibility is to store immutable shareable
* reference-counted memory pages independently of the snapshotting
- * logic. Snapshot management and representation, soft-dirty tracking is
+ * logic. Snapshot management and representation is
* handled to an higher layer. READMORE
*
* Data structure:
close(fd);
}
-static
-int open_process_file(pid_t pid, const char* file, int flags)
-{
- char buff[50];
- snprintf(buff, sizeof(buff), "/proc/%li/%s", (long) pid, file);
- return open(buff, flags);
-}
-
int open_vm(pid_t pid, int flags)
{
const size_t buffer_size = 30;
}
unw_destroy_addr_space(this->unw_addr_space);
-
- if (this->clear_refs_fd_ >= 0)
- close(this->clear_refs_fd_);
- if (this->pagemap_fd_ >= 0)
- close(this->pagemap_fd_);
}
/** Refresh the information about the process
ignored_regions_.begin() + position, region);
}
-void Process::reset_soft_dirty()
-{
- if (this->clear_refs_fd_ < 0) {
- this->clear_refs_fd_ = open_process_file(pid_, "clear_refs", O_WRONLY|O_CLOEXEC);
- if (this->clear_refs_fd_ < 0)
- xbt_die("Could not open clear_refs file for soft-dirty tracking. Run as root?");
- }
- if(::write(this->clear_refs_fd_, "4\n", 2) != 2)
- xbt_die("Could not reset softdirty bits");
-}
-
-void Process::read_pagemap(uint64_t* pagemap, size_t page_start, size_t page_count)
-{
- if (pagemap_fd_ < 0) {
- pagemap_fd_ = open_process_file(pid_, "pagemap", O_RDONLY|O_CLOEXEC);
- if (pagemap_fd_ < 0)
- xbt_die("Could not open pagemap file for soft-dirty tracking. Run as root?");
- }
- ssize_t bytesize = sizeof(uint64_t) * page_count;
- off_t offset = sizeof(uint64_t) * page_start;
- if (pread_whole(pagemap_fd_, pagemap, bytesize, offset) != bytesize)
- xbt_die("Could not read pagemap");
-}
-
void Process::ignore_heap(IgnoredHeapRegion const& region)
{
if (ignored_heap_.empty()) {
running_ = false;
}
- void reset_soft_dirty();
- void read_pagemap(uint64_t* pagemap, size_t start_page, size_t page_count);
-
bool privatized(ObjectInformation const& info) const
{
return privatized_ && info.executable();
RemotePtr<void> maestro_stack_start_, maestro_stack_end_;
int memory_file = -1;
std::vector<IgnoredRegion> ignored_regions_;
- int clear_refs_fd_ = -1;
- int pagemap_fd_ = -1;
bool privatized_ = false;
std::vector<s_stack_region_t> stack_areas_;
std::vector<IgnoredHeapRegion> ignored_heap_;
* @param size Size of the data*
*/
RegionSnapshot region(
- RegionType type, void *start_addr, void* permanent_addr, size_t size,
- RegionSnapshot const* ref_region)
+ RegionType type, void *start_addr, void* permanent_addr, size_t size)
{
if (_sg_mc_sparse_checkpoint)
- return sparse_region(type, start_addr, permanent_addr, size, ref_region);
+ return sparse_region(type, start_addr, permanent_addr, size);
else
return dense_region(type, start_addr, permanent_addr, size);
}
RegionSnapshot sparse_region(RegionType region_type,
- void *start_addr, void* permanent_addr, size_t size,
- RegionSnapshot const* ref_region)
+ void *start_addr, void* permanent_addr, size_t size)
{
simgrid::mc::Process* process = &mc_model_checker->process();
assert(process != nullptr);
- bool use_soft_dirty = _sg_mc_sparse_checkpoint && _sg_mc_soft_dirty
- && ref_region != nullptr
- && ref_region->storage_type() == simgrid::mc::StorageType::Chunked;
-
xbt_assert((((uintptr_t)start_addr) & (xbt_pagesize-1)) == 0,
"Not at the beginning of a page");
xbt_assert((((uintptr_t)permanent_addr) & (xbt_pagesize-1)) == 0,
"Not at the beginning of a page");
size_t page_count = simgrid::mc::mmu::chunkCount(size);
- std::vector<std::uint64_t> pagemap;
- const size_t* ref_page_numbers = nullptr;
- if (use_soft_dirty) {
- pagemap.resize(page_count);
- process->read_pagemap(pagemap.data(),
- simgrid::mc::mmu::split((std::size_t) permanent_addr).first, page_count);
- ref_page_numbers = ref_region->page_data().pagenos();
- }
-
simgrid::mc::ChunkedData page_data(
- mc_model_checker->page_store(), *process, permanent_addr, page_count,
- ref_page_numbers,
- use_soft_dirty ? pagemap.data() : nullptr);
+ mc_model_checker->page_store(), *process, permanent_addr, page_count);
simgrid::mc::RegionSnapshot region(
region_type, start_addr, permanent_addr, size);
RegionSnapshot privatized_region(
RegionType region_type, void *start_addr, void* permanent_addr,
- std::size_t size, const RegionSnapshot* ref_region);
+ std::size_t size);
RegionSnapshot dense_region(
RegionType type, void *start_addr, void* data_addr, std::size_t size);
simgrid::mc::RegionSnapshot sparse_region(
- RegionType type, void *start_addr, void* data_addr, std::size_t size,
- RegionSnapshot const* ref_region);
+ RegionType type, void *start_addr, void* data_addr, std::size_t size);
simgrid::mc::RegionSnapshot region(
- RegionType type, void *start_addr, void* data_addr, std::size_t size,
- RegionSnapshot const* ref_region);
+ RegionType type, void *start_addr, void* data_addr, std::size_t size);
}
}
XBT_INFO("No property violation found.");
simgrid::mc::session->logState();
- initial_global_state = nullptr;
return SIMGRID_MC_EXIT_SUCCESS;
}
XBT_DEBUG("Back-tracking to state %d at depth %zi",
state->num, stack_.size() + 1);
stack_.push_back(std::move(state));
- simgrid::mc::replay(stack_);
+ this->restoreState();
XBT_DEBUG("Back-tracking to state %d at depth %zi done",
stack_.back()->num, stack_.size());
break;
return SIMGRID_MC_EXIT_SUCCESS;
}
+void SafetyChecker::restoreState()
+{
+ /* Intermediate backtracking */
+ {
+ simgrid::mc::State* state = stack_.back().get();
+ if (state->system_state) {
+ simgrid::mc::restore_snapshot(state->system_state);
+ return;
+ }
+ }
+
+ /* Restore the initial state */
+ simgrid::mc::session->restoreInitialState();
+
+ /* Traverse the stack from the state at position start and re-execute the transitions */
+ for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
+ if (state == stack_.back())
+ break;
+ session->execute(state->transition);
+ /* Update statistics */
+ mc_model_checker->visited_states++;
+ mc_model_checker->executed_transitions++;
+ }
+}
+
void SafetyChecker::init()
{
reductionMode_ = simgrid::mc::reduction_mode;
XBT_INFO("Check non progressive cycles");
else
XBT_INFO("Check a safety property");
- mc_model_checker->wait_for_requests();
+ simgrid::mc::session->initialize();
XBT_DEBUG("Starting the safety algorithm");
}
stack_.push_back(std::move(initial_state));
-
- /* Save the initial state */
- initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
- initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
}
SafetyChecker::SafetyChecker(Session& session) : Checker(session)
void init();
bool checkNonTermination(simgrid::mc::State* current_state);
int backtrack();
+ void restoreState();
private:
/** Stack representing the position in the exploration graph */
std::list<std::unique_ptr<simgrid::mc::State>> stack_;
this->close();
}
+void Session::initialize()
+{
+ xbt_assert(initialSnapshot_ == nullptr);
+ mc_model_checker->wait_for_requests();
+ initialSnapshot_ = simgrid::mc::take_snapshot(0);
+}
+
void Session::execute(Transition const& transition)
{
modelChecker_->handle_simcall(transition);
modelChecker_->wait_for_requests();
}
+void Session::restoreInitialState()
+{
+ simgrid::mc::restore_snapshot(this->initialSnapshot_);
+}
+
void Session::logState()
{
mc_model_checker->getChecker()->logState();
void Session::close()
{
+ initialSnapshot_ = nullptr;
if (modelChecker_) {
modelChecker_->shutdown();
modelChecker_ = nullptr;
class Session {
private:
std::unique_ptr<ModelChecker> modelChecker_;
+ std::shared_ptr<simgrid::mc::Snapshot> initialSnapshot_;
private:
Session(pid_t pid, int socket);
void close();
public:
+ void initialize();
void execute(Transition const& transition);
void logState();
+ void restoreInitialState();
+
public: // static constructors
/** Create a new session by forking
#if HAVE_SMPI
RegionSnapshot privatized_region(
RegionType region_type, void *start_addr, void* permanent_addr,
- std::size_t size, const RegionSnapshot* ref_region
+ std::size_t size
)
{
size_t process_count = MC_smpi_process_count();
std::vector<simgrid::mc::RegionSnapshot> data;
data.reserve(process_count);
- for (size_t i = 0; i < process_count; i++) {
- const simgrid::mc::RegionSnapshot* ref_privatized_region = nullptr;
- if (ref_region && ref_region->storage_type() == StorageType::Privatized)
- ref_privatized_region = &ref_region->privatized_data()[i];
+ for (size_t i = 0; i < process_count; i++)
data.push_back(simgrid::mc::region(region_type, start_addr,
- privatisation_regions[i].address, size, ref_privatized_region));
- }
+ privatisation_regions[i].address, size));
simgrid::mc::RegionSnapshot region = simgrid::mc::RegionSnapshot(
region_type, start_addr, permanent_addr, size);
else if (type == simgrid::mc::RegionType::Heap)
xbt_assert(!object_info, "Unexpected object info for heap region.");
- simgrid::mc::RegionSnapshot const* ref_region = nullptr;
- if (mc_model_checker->parent_snapshot_)
- ref_region = mc_model_checker->parent_snapshot_->snapshot_regions[index].get();
-
simgrid::mc::RegionSnapshot region;
#if HAVE_SMPI
const bool privatization_aware = object_info
&& mc_model_checker->process().privatized(*object_info);
if (privatization_aware && MC_smpi_process_count())
region = simgrid::mc::privatized_region(
- type, start_addr, permanent_addr, size, ref_region);
+ type, start_addr, permanent_addr, size);
else
#endif
- region = simgrid::mc::region(type, start_addr, permanent_addr, size, ref_region);
+ region = simgrid::mc::region(type, start_addr, permanent_addr, size);
region.object_info(object_info);
snapshot->snapshot_regions[index]
if (_sg_mc_snapshot_fds)
snapshot->current_fds = get_current_fds(mc_model_checker->process().pid());
- const bool use_soft_dirty = _sg_mc_sparse_checkpoint && _sg_mc_soft_dirty;
-
/* Save the std heap and the writable mapped pages of libsimgrid and binary */
get_memory_regions(mc_process, snapshot.get());
- if (use_soft_dirty)
- mc_process->reset_soft_dirty();
snapshot->to_ignore = mc_model_checker->process().ignored_heap();
snapshot->hash = 0;
snapshot_ignore_restore(snapshot.get());
- if (use_soft_dirty)
- mc_model_checker->parent_snapshot_ = snapshot;
return snapshot;
}
void restore_snapshot(std::shared_ptr<simgrid::mc::Snapshot> snapshot)
{
XBT_DEBUG("Restore snapshot %i", snapshot->num_state);
- const bool use_soft_dirty = _sg_mc_sparse_checkpoint && _sg_mc_soft_dirty;
restore_snapshot_regions(snapshot.get());
if (_sg_mc_snapshot_fds)
restore_snapshot_fds(snapshot.get());
- if (use_soft_dirty)
- mc_model_checker->process().reset_soft_dirty();
snapshot_ignore_restore(snapshot.get());
mc_model_checker->process().clear_cache();
- if (use_soft_dirty)
- mc_model_checker->parent_snapshot_ = snapshot;
}
}
#include "src/mc/mc_comm_pattern.h"
#include "src/mc/mc_smx.h"
#include "src/mc/mc_xbt.hpp"
+#include "src/mc/Checker.hpp"
+#include "src/mc/CommunicationDeterminismChecker.hpp"
using simgrid::mc::remote;
e_mc_call_type_t call_type, smx_simcall_t req,
int value, xbt_dynar_t pattern, int backtracking)
{
+ // HACK, do not rely on the Checker implementation outside of it
+ simgrid::mc::CommunicationDeterminismChecker* checker =
+ (simgrid::mc::CommunicationDeterminismChecker*) mc_model_checker->getChecker();
switch(call_type) {
case MC_CALL_TYPE_NONE:
break;
case MC_CALL_TYPE_SEND:
case MC_CALL_TYPE_RECV:
- MC_get_comm_pattern(pattern, req, call_type, backtracking);
+ checker->get_comm_pattern(pattern, req, call_type, backtracking);
break;
case MC_CALL_TYPE_WAIT:
case MC_CALL_TYPE_WAITANY:
// comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)):
simgrid::mc::read_element(mc_model_checker->process(), &comm_addr,
remote(simcall_comm_waitany__get__comms(req)), value, sizeof(comm_addr));
- MC_complete_comm_pattern(pattern, comm_addr,
+ checker->complete_comm_pattern(pattern, comm_addr,
MC_smx_simcall_get_issuer(req)->pid, backtracking);
}
break;
}
}
-XBT_PRIVATE void MC_get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking);
XBT_PRIVATE void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t request, int value, xbt_dynar_t current_pattern, int backtracking);
-XBT_PRIVATE void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
XBT_PRIVATE void MC_restore_communications_pattern(simgrid::mc::State* state);
int _sg_do_model_check_record = 0;
int _sg_mc_checkpoint = 0;
int _sg_mc_sparse_checkpoint = 0;
-int _sg_mc_soft_dirty = 0;
int _sg_mc_ksm = 0;
char *_sg_mc_property_file = nullptr;
int _sg_mc_hash = 0;
_sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(name);
}
-void _mc_cfg_cb_soft_dirty(const char *name) {
- if (_sg_cfg_init_status && !_sg_do_model_check)
- xbt_die("You are specifying a soft dirty value after the initialization "
- "(through MSG_config?), but model-checking was not activated "
- "at config time (through --cfg=model-check:1). "
- "This won't work, sorry.");
-
- _sg_mc_soft_dirty = xbt_cfg_get_boolean(name);
-}
-
void _mc_cfg_cb_ksm(const char *name)
{
if (_sg_cfg_init_status && !_sg_do_model_check)
#if HAVE_MC
-/* MC global data structures */
-simgrid::mc::State* mc_current_state = nullptr;
-char mc_replay_mode = false;
-
/* Liveness */
namespace simgrid {
namespace mc {
-std::unique_ptr<s_mc_global_t> initial_global_state = nullptr;
xbt_automaton_t property_automaton = nullptr;
}
simgrid::mc::processes_time.clear();
}
-namespace simgrid {
-namespace mc {
-
-/**
- * \brief Re-executes from the state at position start all the transitions indicated by
- * a given model-checker stack.
- * \param stack The stack with the transitions to execute.
- * \param start Start index to begin the re-execution.
- */
-void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack)
-{
- XBT_DEBUG("**** Begin Replay ****");
-
- /* Intermediate backtracking */
- if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) {
- simgrid::mc::State* state = stack.back().get();
- if (state->system_state) {
- simgrid::mc::restore_snapshot(state->system_state);
- if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
- MC_restore_communications_pattern(state);
- return;
- }
- }
-
-
- /* Restore the initial state */
- simgrid::mc::restore_snapshot(simgrid::mc::initial_global_state->snapshot);
-
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- // int n = xbt_dynar_length(incomplete_communications_pattern);
- unsigned n = MC_smx_get_maxpid();
- assert(n == xbt_dynar_length(incomplete_communications_pattern));
- assert(n == xbt_dynar_length(initial_communications_pattern));
- for (unsigned j=0; j < n ; j++) {
- xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
- xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
- }
- }
-
- int count = 1;
-
- /* Traverse the stack from the state at position start and re-execute the transitions */
- for (std::unique_ptr<simgrid::mc::State> const& state : stack) {
- if (state == stack.back())
- break;
-
- int req_num = state->transition.argument;
- smx_simcall_t saved_req = &state->executed_req;
-
- if (saved_req) {
- /* because we got a copy of the executed request, we have to fetch the
- real one, pointed by the request field of the issuer process */
-
- const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
- smx_simcall_t req = &issuer->simcall;
-
- /* Debug information */
- XBT_DEBUG("Replay: %s (%p)",
- simgrid::mc::request_to_string(
- req, req_num, simgrid::mc::RequestType::simix).c_str(),
- state.get());
-
- /* TODO : handle test and testany simcalls */
- e_mc_call_type_t call = MC_CALL_TYPE_NONE;
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- call = MC_get_call_type(req);
-
- mc_model_checker->handle_simcall(state->transition);
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
- mc_model_checker->wait_for_requests();
-
- count++;
- }
-
- /* Update statistics */
- mc_model_checker->visited_states++;
- mc_model_checker->executed_transitions++;
-
- }
-
- XBT_DEBUG("**** End Replay ****");
-}
-
-}
-}
-
void MC_show_deadlock(void)
{
XBT_INFO("**************************");
// Init memory and take snapshots:
init_memory(source, byte_size);
simgrid::mc::RegionSnapshot region0 = simgrid::mc::sparse_region(
- simgrid::mc::RegionType::Unknown, source, source, byte_size, nullptr);
+ simgrid::mc::RegionType::Unknown, source, source, byte_size);
for(int i=0; i<n; i+=2) {
init_memory((char*) source + i*xbt_pagesize, xbt_pagesize);
}
simgrid::mc::RegionSnapshot region = simgrid::mc::sparse_region(
- simgrid::mc::RegionType::Unknown, source, source, byte_size, nullptr);
+ simgrid::mc::RegionType::Unknown, source, source, byte_size);
void* destination = mmap(nullptr, byte_size, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0);
xbt_assert(source!=MAP_FAILED, "Could not allocate destination memory");
xbt_test_add("Read pointer for %i page(s)", n);
memcpy(source, &mc_model_checker, sizeof(void*));
simgrid::mc::RegionSnapshot region2 = simgrid::mc::sparse_region(
- simgrid::mc::RegionType::Unknown, source, source, byte_size, nullptr);
+ simgrid::mc::RegionType::Unknown, source, source, byte_size);
xbt_test_assert(MC_region_read_pointer(®ion2, source) == mc_model_checker,
"Mismtach in MC_region_read_pointer()");
}
int process_index;
} s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
-typedef struct s_mc_global_t {
- std::shared_ptr<simgrid::mc::Snapshot> snapshot;
- int prev_pair = 0;
- std::string prev_req;
- int initial_communications_pattern_done = 0;
- int recv_deterministic = 0;
- int send_deterministic = 0;
- char *send_diff = nullptr;
- char *recv_diff = nullptr;
-}s_mc_global_t, *mc_global_t;
-
namespace simgrid {
namespace mc {
namespace simgrid {
namespace mc {
-extern XBT_PRIVATE std::unique_ptr<s_mc_global_t> initial_global_state;
-
struct PatternCommunication {
int num = 0;
smx_synchro_t comm_addr;
Transition getTransition() const;
};
-XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
-
}
}
"If value=1, one checkpoint is saved for each step => faster verification, but huge memory consumption; higher values are good compromises between speed and memory consumption.");
xbt_cfg_register_boolean("model-check/sparse_checkpoint", "no", _mc_cfg_cb_sparse_checkpoint, "Use sparse per-page snapshots.");
- xbt_cfg_register_boolean("model-check/soft-dirty", "no", _mc_cfg_cb_soft_dirty, "Use sparse per-page snapshots.");
xbt_cfg_register_boolean("model-check/ksm", "no", _mc_cfg_cb_ksm, "Kernel same-page merging");
xbt_cfg_register_string("model-check/property","", _mc_cfg_cb_property,
