throw simgrid::xbt::errno_error(errno);
return handle_message(buffer, size);
}
- if (socket_pollfd->revents & POLLERR) {
+ if (socket_pollfd->revents & POLLERR)
throw_socket_error(socket_pollfd->fd);
- }
if (socket_pollfd->revents & POLLHUP)
xbt_die("Socket hang up?");
}
this->handle_signals();
return true;
}
- if (signalfd_pollfd->revents & POLLERR) {
+ if (signalfd_pollfd->revents & POLLERR)
throw_socket_error(signalfd_pollfd->fd);
- }
if (signalfd_pollfd->revents & POLLHUP)
xbt_die("Signalfd hang up?");
}
void ModelChecker::wait_client(simgrid::mc::Process& process)
{
this->resume(process);
- while (this->process().running()) {
+ while (this->process().running())
if (!this->handle_events())
return;
- }
}
void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
m.value = value;
process.send_message(m);
process.cache_flags = (mc_process_cache_flags_t) 0;
- while (process.running()) {
+ while (process.running())
if (!this->handle_events())
return;
- }
}
}
// This djb2:
std::uint64_t hash = 5381;
- for (std::size_t i = 0; i != n; ++i) {
+ for (std::size_t i = 0; i != n; ++i)
hash = ((hash << 5) + hash) + values[i];
- }
return hash;
}
// by relocating it somewhere else in the virtual memory
// space:
void* memory = ::mmap(nullptr, size << xbt_pagebits, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS|MAP_POPULATE, -1, 0);
- if (memory == MAP_FAILED) {
+ if (memory == MAP_FAILED)
xbt_die("Could not mmap initial snapshot pages.");
- }
this->top_index_ = 0;
this->capacity_ = size;
// Expand the memory region by moving it into another
// virtual memory address if necessary:
void* new_memory = mremap(this->memory_, old_bytesize, new_bytesize, MREMAP_MAYMOVE);
- if (new_memory == MAP_FAILED) {
+ if (new_memory == MAP_FAILED)
xbt_die("Could not mremap snapshot pages.");
- }
this->capacity_ = size;
this->memory_ = new_memory;
if (this->free_pages_.empty()) {
// Expand the region:
- if (this->top_index_ == this->capacity_) {
+ if (this->top_index_ == this->capacity_)
// All the pages are allocated, we need add more pages:
this->resize(2 * this->capacity_);
- }
// Use a page from the top:
return this->top_index_++;
this->maestro_stack_start_ = nullptr;
this->maestro_stack_end_ = nullptr;
- if (this->memory_file >= 0) {
+ if (this->memory_file >= 0)
close(this->memory_file);
- }
if (this->unw_underlying_addr_space != unw_local_addr_space) {
unw_destroy_addr_space(this->unw_underlying_addr_space);
RegionType type, void *start_addr, void* permanent_addr, size_t size,
RegionSnapshot const* ref_region)
{
- if (_sg_mc_sparse_checkpoint) {
+ if (_sg_mc_sparse_checkpoint)
return sparse_region(type, start_addr, permanent_addr, size, ref_region);
- } else {
+ else
return dense_region(type, start_addr, permanent_addr, size);
- }
}
RegionSnapshot sparse_region(RegionType region_type,
MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
smx_process_t process;
- xbt_swag_foreach(process, simix_global->process_list) {
+ xbt_swag_foreach(process, simix_global->process_list)
MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
- }
}
}
smx_process_t process;
if (xbt_swag_size(simix_global->process_list)) {
deadlock = TRUE;
- xbt_swag_foreach(process, simix_global->process_list) {
+ xbt_swag_foreach(process, simix_global->process_list)
if (MC_process_is_enabled(process)) {
deadlock = FALSE;
break;
}
- }
}
return deadlock;
}
return mc_time[process->pid];
else
return -1;
- } else {
+ } else
return 0;
- }
}
void MC_process_clock_add(smx_process_t process, double amount)
((char *) stack -
(char *) heap->heapbase) / BLOCKSIZE + 1;
#ifdef HAVE_SMPI
- if (smpi_privatize_global_variables && process) {
+ if (smpi_privatize_global_variables && process)
region.process_index = smpi_process_index_of_smx_process(process);
- } else
+ else
#endif
region.process_index = -1;
new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
new_pair->acceptance_pair = 1;
- if (xbt_dynar_is_empty(acceptance_pairs)) {
-
+ if (xbt_dynar_is_empty(acceptance_pairs))
xbt_dynar_push(acceptance_pairs, &new_pair);
-
- } else {
+ else {
int min = -1, max = -1, index;
//int res;
xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
} else {
pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
- if (pair_test->nb_processes < new_pair->nb_processes) {
+ if (pair_test->nb_processes < new_pair->nb_processes)
xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
- } else {
- if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
- xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
- else
- xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
- }
+ else if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
+ xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
+ else
+ xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
}
}
return new_pair;
mc_visited_pair_t pair_test = nullptr;
int pair_found = 0;
- xbt_dynar_foreach(acceptance_pairs, cursor, pair_test) {
+ xbt_dynar_foreach(acceptance_pairs, cursor, pair_test)
if (pair_test->num == pair_num) {
pair_found = 1;
break;
}
- }
if(pair_found == 1) {
xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
}
return -1;
}
- case 4:{
- return 2;
- }
+ case 4:
+ return 2;
default:
return -1;
}
/* It creates the two heap regions: std_heap and mc_heap */
void MC_memory_init()
{
- if (!malloc_use_mmalloc()) {
+ if (!malloc_use_mmalloc())
xbt_die("Model-checking support is not enabled: run with simgrid-mc.");
- }
}
/* Finalize the memory subsystem */
size_t mc_page_count(size_t size)
{
size_t page_count = size >> xbt_pagebits;
- if (size & (xbt_pagesize-1)) {
+ if (size & (xbt_pagesize-1))
page_count ++;
- }
return page_count;
}
MC_mode_name(mc_mode),
MC_message_type_name(*(e_mc_message_type*) message));
- while (send(socket, message, size, 0) == -1) {
+ while (send(socket, message, size, 0) == -1)
if (errno == EINTR)
continue;
else
return errno;
- }
return 0;
}
ssize_t MC_receive_message(int socket, void* message, size_t size, int options)
{
int res = recv(socket, message, size, options);
- if (res != -1) {
+ if (res != -1)
XBT_DEBUG("Protocol [%s] received %s",
MC_mode_name(mc_mode),
MC_message_type_name(*(e_mc_message_type*) message));
- }
return res;
}
args = bprintf("comm=%s (%d of %lu)",
p, value + 1, xbt_dynar_length(&comms));
xbt_free(p);
- } else {
+ } else
args = bprintf("comm at idx %d", value);
- }
break;
}
}
char* str;
- if (args != nullptr) {
+ if (args != nullptr)
str =
bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
MC_smx_process_get_host_name(issuer),
MC_smx_process_get_name(issuer),
type, args);
- } else {
+ else
str =
bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
MC_smx_process_get_host_name(issuer),
MC_smx_process_get_name(issuer),
type);
- }
xbt_free(args);
return str;
}
XBT_DEBUG("Execute: %s", req_str);
xbt_free(req_str);
- if (dot_output != nullptr) {
+ if (dot_output != nullptr)
req_str = MC_request_get_dot_output(req, value);
- }
MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
if (dot_output != nullptr)
std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
- } else {
-
- if (dot_output != nullptr)
- std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
+ } else if (dot_output != nullptr)
+ std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
- }
xbt_fifo_unshift(mc_stack, next_state);
else
XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
- } else {
-
+ } else
XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
- }
-
/* Trash the current state, no longer needed */
xbt_fifo_shift(mc_stack);
XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
{
if (mc_mode == MC_MODE_CLIENT)
return smpi_process_count();
- else {
- int res;
- mc_model_checker->process().read_variable("process_count",
- &res, sizeof(res));
- return res;
- }
+ int res;
+ mc_model_checker->process().read_variable("process_count",
+ &res, sizeof(res));
+ return res;
}
#endif
if (region->storage_type() == simgrid::mc::StorageType::Privatized) {
#ifdef HAVE_SMPI
// Use the current process index of the snapshot:
- if (process_index == simgrid::mc::ProcessIndexDisabled) {
+ if (process_index == simgrid::mc::ProcessIndexDisabled)
process_index = snapshot->privatization_index;
- }
- if (process_index < 0) {
+ if (process_index < 0)
xbt_die("Missing process index");
- }
- if (process_index >= (int) region->privatized_data().size()) {
+ if (process_index >= (int) region->privatized_data().size())
xbt_die("Invalid process index");
- }
simgrid::mc::RegionSnapshot& priv_region = region->privatized_data()[process_index];
xbt_assert(priv_region.contain(simgrid::mc::remote(addr)));
return &priv_region;
void* dest = target;
- if (dest==nullptr) {
+ if (dest==nullptr)
xbt_die("Missing destination buffer for fragmented memory access");
- }
// Read each page:
while (mc_page_number(nullptr, addr) != page_end) {
const void* buffer1 = MC_region_read(region1, buffer1a, addr1, size);
const void* buffer2 = MC_region_read(region2, buffer2a, addr2, size);
int res;
- if (buffer1 == buffer2) {
+ if (buffer1 == buffer2)
res = 0;
- } else {
+ else
res = memcmp(buffer1, buffer2, size);
- }
if (!stack_alloc) {
free(buffer1a);
free(buffer2a);
* \param trans The state to be deleted
*/
void MC_state_delete(mc_state_t state, int free_snapshot){
- if (state->system_state && free_snapshot){
+ if (state->system_state && free_snapshot)
delete state->system_state;
- }
if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
xbt_free(state->index_comm);
xbt_free(state->incomplete_comm_pattern);
unsigned int MC_state_interleave_size(mc_state_t state)
{
unsigned int i, size = 0;
-
- for (i = 0; i < state->max_pid; i++) {
+ for (i = 0; i < state->max_pid; i++)
if ((state->proc_status[i].state == MC_INTERLEAVE)
|| (state->proc_status[i].state == MC_MORE_INTERLEAVE))
size++;
- }
-
return size;
}
case SIMCALL_MC_RANDOM: {
state->internal_req = *req;
int random_max = simcall_mc_random__get__max(req);
- if (value != random_max) {
+ if (value != random_max)
for (auto& p : mc_model_checker->process().simix_processes()) {
mc_procstate_t procstate = &state->proc_status[p.copy.pid];
const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
break;
}
}
- }
break;
}
*value = -1;
while (procstate->interleave_count <
read_length(mc_model_checker->process(),
- remote(simcall_comm_testany__get__comms(&process->simcall)))) {
+ remote(simcall_comm_testany__get__comms(&process->simcall))))
if (MC_request_is_enabled_by_idx
(&process->simcall, procstate->interleave_count++)) {
*value = procstate->interleave_count - 1;
break;
}
- }
if (procstate->interleave_count >=
read_length(mc_model_checker->process(),
s_smx_synchro_t act;
mc_model_checker->process().read_bytes(
&act, sizeof(act), remote(remote_act));
- if (act.comm.src_proc && act.comm.dst_proc) {
+ if (act.comm.src_proc && act.comm.dst_proc)
*value = 0;
- } else {
- if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
+ else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
&& act.comm.detached == 1)
- *value = 0;
- else
- *value = -1;
- }
+ *value = 0;
+ else
+ *value = -1;
procstate->state = MC_DONE;
return &process->simcall;
}
case SIMCALL_MC_RANDOM:
if (procstate->state == MC_INTERLEAVE)
*value = simcall_mc_random__get__min(&process->simcall);
- else {
- if (state->req_num < simcall_mc_random__get__max(&process->simcall))
- *value = state->req_num + 1;
- }
+ else if (state->req_num < simcall_mc_random__get__max(&process->simcall))
+ *value = state->req_num + 1;
procstate->state = MC_DONE;
return &process->simcall;