Some of them cannot be hidden because they are used in the unit tests.
#endif
+#ifdef _XBT_WIN32
+#define XBT_INTERNAL
+#else
+#define XBT_INTERNAL __attribute__((visibility ("hidden")))
+#endif
+
#if !defined (max) && !defined(__cplusplus)
# define max(a,b) (((a) > (b)) ? (a) : (b))
#endif
XBT_PUBLIC_DATA(int) xbt_pagesize;
/** Cache the number of bits of addresses inside a given page, log2(xbt_pagesize). */
- XBT_PUBLIC_DATA(int) xbt_pagebits;
+XBT_PUBLIC_DATA(int) xbt_pagebits;
XBT_PUBLIC(const char *) xbt_procname(void);
#include "internal_config.h"
#include "../simix/smx_private.h"
+// Marker for symbols which should be defined as XBT_PRIVATE but are used in
+// unit tests:
+#define MC_SHOULD_BE_INTERNAL
+
SG_BEGIN_DECL()
/** Check if the given simcall can be resolved
*/
void MC_wait_for_requests(void);
-extern double *mc_time;
+XBT_INTERNAL extern double *mc_time;
SG_END_DECL()
int fd;
} s_mc_client_t, *mc_client_t;
-extern mc_client_t mc_client;
+extern XBT_INTERNAL mc_client_t mc_client;
-void MC_client_init(void);
-void MC_client_hello(void);
-void MC_client_handle_messages(void);
-void MC_client_send_message(void* message, size_t size);
-void MC_client_send_simple_message(e_mc_message_type type);
+XBT_INTERNAL void MC_client_init(void);
+XBT_INTERNAL void MC_client_hello(void);
+XBT_INTERNAL void MC_client_handle_messages(void);
+XBT_INTERNAL void MC_client_send_message(void* message, size_t size);
+XBT_INTERNAL void MC_client_send_simple_message(e_mc_message_type type);
#ifdef HAVE_MC
void MC_ignore(void* addr, size_t size);
/**
* Type: `xbt_dynar_t<mc_list_comm_pattenr_t>`
*/
-extern xbt_dynar_t initial_communications_pattern;
+extern XBT_INTERNAL xbt_dynar_t initial_communications_pattern;
/**
* Type: `xbt_dynar_t<xbt_dynar_t<mc_comm_pattern_t>>`
*/
-extern xbt_dynar_t incomplete_communications_pattern;
+extern XBT_INTERNAL xbt_dynar_t incomplete_communications_pattern;
typedef enum {
MC_CALL_TYPE_NONE,
}
}
-void MC_get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking);
-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);
-void MC_comm_pattern_free_voidp(void *p);
-void MC_list_comm_pattern_free_voidp(void *p);
-void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
+XBT_INTERNAL void MC_get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking);
+XBT_INTERNAL 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_INTERNAL void MC_comm_pattern_free_voidp(void *p);
+XBT_INTERNAL void MC_list_comm_pattern_free_voidp(void *p);
+XBT_INTERNAL void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
void MC_modelcheck_comm_determinism(void);
-void MC_restore_communications_pattern(mc_state_t state);
+XBT_INTERNAL void MC_restore_communications_pattern(mc_state_t state);
-mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm);
-xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t state);
+XBT_INTERNAL mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm);
+XBT_INTERNAL xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t state);
-void MC_state_copy_incomplete_communications_pattern(mc_state_t state);
-void MC_state_copy_index_communications_pattern(mc_state_t state);
+XBT_INTERNAL void MC_state_copy_incomplete_communications_pattern(mc_state_t state);
+XBT_INTERNAL void MC_state_copy_index_communications_pattern(mc_state_t state);
-void MC_comm_pattern_free(mc_comm_pattern_t p);
+XBT_INTERNAL void MC_comm_pattern_free(mc_comm_pattern_t p);
SG_END_DECL()
* \param tag tag code (see the DWARF specification)
* \return name of the tag
*/
+XBT_INTERNAL
const char *MC_dwarf_tagname(int tag)
{
switch (tag) {
SG_BEGIN_DECL();
-void MC_stack_area_add(stack_region_t stack_area);
+XBT_INTERNAL void MC_stack_area_add(stack_region_t stack_area);
-xbt_dynar_t MC_checkpoint_ignore_new(void);
+XBT_INTERNAL xbt_dynar_t MC_checkpoint_ignore_new(void);
SG_END_DECL();
SG_BEGIN_DECL()
-extern xbt_automaton_t _mc_property_automaton;
+extern XBT_INTERNAL xbt_automaton_t _mc_property_automaton;
typedef struct s_mc_pair{
int num;
int visited_removed;
} s_mc_visited_pair_t, *mc_visited_pair_t;
-mc_pair_t MC_pair_new(void);
-void MC_pair_delete(mc_pair_t);
-void mc_pair_free_voidp(void *p);
-mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state);
-void MC_visited_pair_delete(mc_visited_pair_t p);
+XBT_INTERNAL mc_pair_t MC_pair_new(void);
+XBT_INTERNAL void MC_pair_delete(mc_pair_t);
+XBT_INTERNAL void mc_pair_free_voidp(void *p);
+XBT_INTERNAL mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state);
+XBT_INTERNAL void MC_visited_pair_delete(mc_visited_pair_t p);
void MC_modelcheck_liveness(void);
-void MC_show_stack_liveness(xbt_fifo_t stack);
-void MC_dump_stack_liveness(xbt_fifo_t stack);
+XBT_INTERNAL void MC_show_stack_liveness(xbt_fifo_t stack);
+XBT_INTERNAL void MC_dump_stack_liveness(xbt_fifo_t stack);
-extern xbt_dynar_t visited_pairs;
-int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair);
+XBT_INTERNAL extern xbt_dynar_t visited_pairs;
+XBT_INTERNAL int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair);
SG_END_DECL()
#include <elfutils/libdw.h>
#include <simgrid_config.h>
+#include "mc_base.h"
#include "mc_forward.h"
#include "mc_object_info.h"
#include "mc_forward.h"
}
}
-void mc_dwarf_resolve_location(mc_location_t location, mc_expression_t expression, mc_object_info_t object_info, unw_cursor_t* c, void* frame_pointer_address, mc_address_space_t address_space, int process_index);
-void mc_dwarf_resolve_locations(mc_location_t location, mc_location_list_t locations, mc_object_info_t object_info, unw_cursor_t* c, void* frame_pointer_address, mc_address_space_t address_space, int process_index);
+XBT_INTERNAL void mc_dwarf_resolve_location(mc_location_t location, mc_expression_t expression, mc_object_info_t object_info, unw_cursor_t* c, void* frame_pointer_address, mc_address_space_t address_space, int process_index);
+MC_SHOULD_BE_INTERNAL void mc_dwarf_resolve_locations(mc_location_t location, mc_location_list_t locations, mc_object_info_t object_info, unw_cursor_t* c, void* frame_pointer_address, mc_address_space_t address_space, int process_index);
-void mc_dwarf_expression_clear(mc_expression_t expression);
-void mc_dwarf_expression_init(mc_expression_t expression, size_t len, Dwarf_Op* ops);
+XBT_INTERNAL void mc_dwarf_expression_clear(mc_expression_t expression);
+XBT_INTERNAL void mc_dwarf_expression_init(mc_expression_t expression, size_t len, Dwarf_Op* ops);
-void mc_dwarf_location_list_clear(mc_location_list_t list);
+XBT_INTERNAL void mc_dwarf_location_list_clear(mc_location_list_t list);
-void mc_dwarf_location_list_init_from_expression(mc_location_list_t target, size_t len, Dwarf_Op* ops);
-void mc_dwarf_location_list_init(mc_location_list_t target, mc_object_info_t info, Dwarf_Die* die, Dwarf_Attribute* attr);
+XBT_INTERNAL void mc_dwarf_location_list_init_from_expression(mc_location_list_t target, size_t len, Dwarf_Op* ops);
+XBT_INTERNAL void mc_dwarf_location_list_init(mc_location_list_t target, mc_object_info_t info, Dwarf_Die* die, Dwarf_Attribute* attr);
#define MC_EXPRESSION_STACK_SIZE 64
int process_index;
} s_mc_expression_state_t, *mc_expression_state_t;
-int mc_dwarf_execute_expression(size_t n, const Dwarf_Op* ops, mc_expression_state_t state);
+MC_SHOULD_BE_INTERNAL int mc_dwarf_execute_expression(
+ size_t n, const Dwarf_Op* ops, mc_expression_state_t state);
-void* mc_find_frame_base(dw_frame_t frame, mc_object_info_t object_info, unw_cursor_t* unw_cursor);
+MC_SHOULD_BE_INTERNAL void* mc_find_frame_base(
+ dw_frame_t frame, mc_object_info_t object_info, unw_cursor_t* unw_cursor);
SG_END_DECL()
};
-memory_map_t MC_get_memory_map(pid_t pid);
-void MC_free_memory_map(memory_map_t map);
+XBT_INTERNAL memory_map_t MC_get_memory_map(pid_t pid);
+XBT_INTERNAL void MC_free_memory_map(memory_map_t map);
SG_END_DECL()
#include <stdint.h>
#include <stdbool.h>
+#include <xbt/misc.h>
+
#include <simgrid_config.h>
SG_BEGIN_DECL()
-extern int xbt_pagesize;
-extern int xbt_pagebits;
-
/** @brief How many memory pages are necessary to store size bytes?
*
* @param size Byte size
dw_type_t full_type; // The same (but more complete) type
};
-void dw_type_free(dw_type_t t);
-void dw_variable_free(dw_variable_t v);
-void dw_variable_free_voidp(void *t);
+XBT_INTERNAL void dw_type_free(dw_type_t t);
+XBT_INTERNAL void dw_variable_free(dw_variable_t v);
+XBT_INTERNAL void dw_variable_free_voidp(void *t);
// ***** Object info
* + \text{dwarf address}\f$.</li>
*
*/
-void* MC_object_base_address(mc_object_info_t info);
+XBT_INTERNAL void* MC_object_base_address(mc_object_info_t info);
-mc_object_info_t MC_new_object_info(void);
-mc_object_info_t MC_find_object_info(memory_map_t maps, const char* name, int executable);
-void MC_free_object_info(mc_object_info_t* p);
+XBT_INTERNAL mc_object_info_t MC_new_object_info(void);
+XBT_INTERNAL mc_object_info_t MC_find_object_info(memory_map_t maps, const char* name, int executable);
+XBT_INTERNAL void MC_free_object_info(mc_object_info_t* p);
-dw_frame_t MC_file_object_info_find_function(mc_object_info_t info, const void *ip);
-dw_variable_t MC_file_object_info_find_variable_by_name(mc_object_info_t info, const char* name);
+XBT_INTERNAL dw_frame_t MC_file_object_info_find_function(mc_object_info_t info, const void *ip);
+MC_SHOULD_BE_INTERNAL dw_variable_t MC_file_object_info_find_variable_by_name(mc_object_info_t info, const char* name);
-void MC_post_process_object_info(mc_process_t process, mc_object_info_t info);
+XBT_INTERNAL void MC_post_process_object_info(mc_process_t process, mc_object_info_t info);
-void MC_dwarf_get_variables(mc_object_info_t info);
-void MC_dwarf_get_variables_libdw(mc_object_info_t info);
-const char* MC_dwarf_attrname(int attr);
-const char* MC_dwarf_tagname(int tag);
+XBT_INTERNAL void MC_dwarf_get_variables(mc_object_info_t info);
+XBT_INTERNAL void MC_dwarf_get_variables_libdw(mc_object_info_t info);
+XBT_INTERNAL const char* MC_dwarf_attrname(int attr);
+XBT_INTERNAL const char* MC_dwarf_tagname(int tag);
// Not used:
-char* get_type_description(mc_object_info_t info, char *type_name);
+XBT_INTERNAL char* get_type_description(mc_object_info_t info, char *type_name);
-void* mc_member_resolve(const void* base, dw_type_t type, dw_type_t member, mc_address_space_t snapshot, int process_index);
+XBT_INTERNAL void* mc_member_resolve(const void* base, dw_type_t type, dw_type_t member, mc_address_space_t snapshot, int process_index);
struct s_dw_variable{
Dwarf_Off dwarf_offset; /* Global offset of the field. */
dw_frame_t function;
};
-void mc_frame_free(dw_frame_t freme);
+XBT_INTERNAL void mc_frame_free(dw_frame_t freme);
SG_END_DECL()
*/
void MC_init_model_checker(pid_t pid, int socket);
-extern FILE *dot_output;
-extern const char* colors[13];
-extern xbt_parmap_t parmap;
+XBT_INTERNAL extern FILE *dot_output;
+XBT_INTERNAL extern const char* colors[13];
+XBT_INTERNAL extern xbt_parmap_t parmap;
-extern int user_max_depth_reached;
+XBT_INTERNAL extern int user_max_depth_reached;
-int MC_deadlock_check(void);
-void MC_replay(xbt_fifo_t stack);
-void MC_replay_liveness(xbt_fifo_t stack);
-void MC_show_deadlock(smx_simcall_t req);
-void MC_show_stack_safety(xbt_fifo_t stack);
-void MC_dump_stack_safety(xbt_fifo_t stack);
-void MC_show_non_termination(void);
+XBT_INTERNAL int MC_deadlock_check(void);
+XBT_INTERNAL void MC_replay(xbt_fifo_t stack);
+XBT_INTERNAL void MC_replay_liveness(xbt_fifo_t stack);
+XBT_INTERNAL void MC_show_deadlock(smx_simcall_t req);
+XBT_INTERNAL void MC_show_stack_safety(xbt_fifo_t stack);
+XBT_INTERNAL void MC_dump_stack_safety(xbt_fifo_t stack);
+XBT_INTERNAL void MC_show_non_termination(void);
/** Stack (of `mc_state_t`) representing the current position of the
* the MC in the exploration graph
*
* It is managed by its head (`xbt_fifo_shift` and `xbt_fifo_unshift`).
*/
-extern xbt_fifo_t mc_stack;
+XBT_INTERNAL extern xbt_fifo_t mc_stack;
-int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max);
+XBT_INTERNAL int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max);
/****************************** Statistics ************************************/
unsigned long executed_transitions;
} s_mc_stats_t, *mc_stats_t;
-extern mc_stats_t mc_stats;
+XBT_INTERNAL extern mc_stats_t mc_stats;
-void MC_print_statistics(mc_stats_t stats);
+XBT_INTERNAL void MC_print_statistics(mc_stats_t stats);
/********************************** Snapshot comparison **********************************/
double stacks_comparison_time;
}s_mc_comparison_times_t, *mc_comparison_times_t;
-extern __thread mc_comparison_times_t mc_comp_times;
-extern __thread double mc_snapshot_comparison_time;
+extern XBT_INTERNAL __thread mc_comparison_times_t mc_comp_times;
+extern XBT_INTERNAL __thread double mc_snapshot_comparison_time;
-int snapshot_compare(void *state1, void *state2);
-void print_comparison_times(void);
+XBT_INTERNAL int snapshot_compare(void *state1, void *state2);
+XBT_INTERNAL void print_comparison_times(void);
//#define MC_DEBUG 1
#define MC_VERBOSE 1
/********************************** Variables with DWARF **********************************/
-void MC_find_object_address(memory_map_t maps, mc_object_info_t result);
+XBT_INTERNAL void MC_find_object_address(memory_map_t maps, mc_object_info_t result);
/********************************** Miscellaneous **********************************/
dw_type_t type;
void *address;
int region;
-}s_local_variable_t, *local_variable_t;
+} s_local_variable_t, *local_variable_t;
/* *********** Hash *********** */
* \param stacks stacks (mc_snapshot_stak_t) used fot the stack unwinding informations
* \result resulting hash
* */
-uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks);
+XBT_INTERNAL uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks);
/** @brief Dump the stacks of the application processes
*
*
* Does not work when an application thread is running.
*/
-void MC_dump_stacks(FILE* file);
+XBT_INTERNAL void MC_dump_stacks(FILE* file);
-void MC_report_assertion_error(void);
+XBT_INTERNAL void MC_report_assertion_error(void);
-void MC_invalidate_cache(void);
+XBT_INTERNAL void MC_invalidate_cache(void);
SG_END_DECL()
#include "simix/smx_private.h"
#include "mc_forward.h"
+#include "mc_base.h"
#include "mc_mmalloc.h" // std_heap
#include "mc_memory_map.h"
#include "mc_address_space.h"
xbt_dynar_t checkpoint_ignore;
};
-bool MC_is_process(mc_address_space_t p);
+XBT_INTERNAL bool MC_is_process(mc_address_space_t p);
-void MC_process_init(mc_process_t process, pid_t pid, int sockfd);
-void MC_process_clear(mc_process_t process);
+MC_SHOULD_BE_INTERNAL void MC_process_init(mc_process_t process, pid_t pid, int sockfd);
+XBT_INTERNAL void MC_process_clear(mc_process_t process);
/** Refresh the information about the process
*
* Do not use direclty, this is used by the getters when appropriate
* in order to have fresh data.
*/
-void MC_process_refresh_heap(mc_process_t process);
+XBT_INTERNAL void MC_process_refresh_heap(mc_process_t process);
/** Refresh the information about the process
*
* Do not use direclty, this is used by the getters when appropriate
* in order to have fresh data.
* */
-void MC_process_refresh_malloc_info(mc_process_t process);
+XBT_INTERNAL void MC_process_refresh_malloc_info(mc_process_t process);
static inline
bool MC_process_is_self(mc_process_t process)
* @param remote target process memory address (source)
* @param len data size
*/
-const void* MC_process_read(mc_process_t process,
+XBT_INTERNAL const void* MC_process_read(mc_process_t process,
adress_space_read_flags_t flags,
void* local, const void* remote, size_t len,
int process_index);
// Simplified versions/wrappers (whould be moved in mc_address_space):
-const void* MC_process_read_simple(mc_process_t process,
+XBT_INTERNAL const void* MC_process_read_simple(mc_process_t process,
void* local, const void* remote, size_t len);
-const void* MC_process_read_dynar_element(mc_process_t process,
+XBT_INTERNAL const void* MC_process_read_dynar_element(mc_process_t process,
void* local, const void* remote_dynar, size_t i, size_t len);
-unsigned long MC_process_read_dynar_length(mc_process_t process, const void* remote_dynar);
+XBT_INTERNAL unsigned long MC_process_read_dynar_length(mc_process_t process,
+ const void* remote_dynar);
/** Write data to a process memory
*
* @param remote target process memory address (target)
* @param len data size
*/
-void MC_process_write(mc_process_t process, const void* local, void* remote, size_t len);
+XBT_INTERNAL void MC_process_write(mc_process_t process,
+ const void* local, void* remote, size_t len);
-void MC_process_clear_memory(mc_process_t process, void* remote, size_t len);
+XBT_INTERNAL void MC_process_clear_memory(mc_process_t process,
+ void* remote, size_t len);
/* Functions, variables of the process: */
-mc_object_info_t MC_process_find_object_info(mc_process_t process, const void* addr);
-mc_object_info_t MC_process_find_object_info_exec(mc_process_t process, const void* addr);
-mc_object_info_t MC_process_find_object_info_rw(mc_process_t process, const void* addr);
+XBT_INTERNAL mc_object_info_t MC_process_find_object_info(mc_process_t process, const void* addr);
+XBT_INTERNAL mc_object_info_t MC_process_find_object_info_exec(mc_process_t process, const void* addr);
+XBT_INTERNAL mc_object_info_t MC_process_find_object_info_rw(mc_process_t process, const void* addr);
-dw_frame_t MC_process_find_function(mc_process_t process, const void* ip);
+XBT_INTERNAL dw_frame_t MC_process_find_function(mc_process_t process, const void* ip);
-void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size);
-char* MC_process_read_string(mc_process_t, void* address);
+XBT_INTERNAL void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size);
+XBT_INTERNAL char* MC_process_read_string(mc_process_t, void* address);
static inline xbt_mheap_t MC_process_get_heap(mc_process_t process)
{
/** Find (one occurence of) the named variable definition
*/
-dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name);
+XBT_INTERNAL dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name);
-void MC_invalidate_cache(void);
+XBT_INTERNAL void MC_invalidate_cache(void);
SG_END_DECL()
void* data;
} s_mc_register_symbol_message_t, * mc_register_symbol_message_t;
-int MC_protocol_send(int socket, void* message, size_t size);
-int MC_protocol_send_simple_message(int socket, e_mc_message_type type);
-int MC_protocol_hello(int socket);
-ssize_t MC_receive_message(int socket, void* message, size_t size, int options);
+XBT_INTERNAL int MC_protocol_send(int socket, void* message, size_t size);
+XBT_INTERNAL int MC_protocol_send_simple_message(int socket, e_mc_message_type type);
+XBT_INTERNAL int MC_protocol_hello(int socket);
+XBT_INTERNAL ssize_t MC_receive_message(int socket, void* message, size_t size, int options);
-const char* MC_message_type_name(e_mc_message_type type);
-const char* MC_mode_name(e_mc_mode_t mode);
+XBT_INTERNAL const char* MC_message_type_name(e_mc_message_type type);
+XBT_INTERNAL const char* MC_mode_name(e_mc_mode_t mode);
SG_END_DECL()
/** Convert a string representation of the path into a array of `s_mc_record_item_t`
*/
-xbt_dynar_t MC_record_from_string(const char* data);
+XBT_INTERNAL xbt_dynar_t MC_record_from_string(const char* data);
/** Generate a string representation
*
* "pid0,value0;pid2,value2;pid3,value3". The value can be
* omitted is it is null.
*/
-char* MC_record_stack_to_string(xbt_fifo_t stack);
+XBT_INTERNAL char* MC_record_stack_to_string(xbt_fifo_t stack);
/** Dump the path represented by a given stack in the log
*/
-void MC_record_dump_path(xbt_fifo_t stack);
+XBT_INTERNAL void MC_record_dump_path(xbt_fifo_t stack);
// ***** Replay
* \param start Array of record item
* \item count Number of record items
*/
-void MC_record_replay(mc_record_item_t start, size_t count);
+XBT_INTERNAL void MC_record_replay(mc_record_item_t start, size_t count);
/** Replay a path represented by a string
*
* \param data String representation of the path
*/
-void MC_record_replay_from_string(const char* data);
+XBT_INTERNAL void MC_record_replay_from_string(const char* data);
-void MC_record_replay_init(void);
+XBT_INTERNAL void MC_record_replay_init(void);
SG_END_DECL()
MC_REQUEST_INTERNAL,
} e_mc_request_type_t;
-int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
-char* MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t type);
-unsigned int MC_request_testany_fail(smx_simcall_t req);
+XBT_INTERNAL int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
+XBT_INTERNAL char* MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t type);
+XBT_INTERNAL unsigned int MC_request_testany_fail(smx_simcall_t req);
/*int MC_waitany_is_enabled_by_comm(smx_req_t req, unsigned int comm);*/
-int MC_request_is_visible(smx_simcall_t req);
+XBT_INTERNAL int MC_request_is_visible(smx_simcall_t req);
/** Can this requests can be executed.
*
* have both a source and a destination yet is not enabled
* (unless timeout is enabled in the wait and enabeld in SimGridMC).
*/
-int MC_request_is_enabled(smx_simcall_t req);
-int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx);
+XBT_INTERNAL int MC_request_is_enabled(smx_simcall_t req);
+XBT_INTERNAL int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx);
/** Is the process ready to execute its simcall?
*
* This is true if the request associated with the process is ready.
*/
-int MC_process_is_enabled(smx_process_t process);
+XBT_INTERNAL int MC_process_is_enabled(smx_process_t process);
-char *MC_request_get_dot_output(smx_simcall_t req, int value);
+XBT_INTERNAL char *MC_request_get_dot_output(smx_simcall_t req, int value);
SG_END_DECL()
e_mc_reduce_dpor
} e_mc_reduce_t;
-extern e_mc_reduce_t mc_reduce_kind;
+extern XBT_INTERNAL e_mc_reduce_t mc_reduce_kind;
void MC_modelcheck_safety(void);
int other_num; // dot_output for
}s_mc_visited_state_t, *mc_visited_state_t;
-extern xbt_dynar_t visited_states;
-mc_visited_state_t is_visited_state(mc_state_t graph_state);
-void visited_state_free(mc_visited_state_t state);
-void visited_state_free_voidp(void *s);
+extern XBT_INTERNAL xbt_dynar_t visited_states;
+XBT_INTERNAL mc_visited_state_t is_visited_state(mc_state_t graph_state);
+XBT_INTERNAL void visited_state_free(mc_visited_state_t state);
+XBT_INTERNAL void visited_state_free_voidp(void *s);
SG_END_DECL()
extern mc_server_t mc_server;
-void MC_server_wait_client(mc_process_t process);
-void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value);
+XBT_INTERNAL void MC_server_wait_client(mc_process_t process);
+XBT_INTERNAL void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value);
-void MC_server_loop(mc_server_t server);
+XBT_INTERNAL void MC_server_loop(mc_server_t server);
SG_END_DECL()
char* name;
};
-xbt_dynar_t MC_smx_process_info_list_new(void);
+XBT_INTERNAL xbt_dynar_t MC_smx_process_info_list_new(void);
-void MC_process_smx_refresh(mc_process_t process);
+XBT_INTERNAL void MC_process_smx_refresh(mc_process_t process);
/** Get the issuer of a simcall (`req->issuer`)
*
* @param process the MCed process
* @param req the simcall (copied in the local process)
*/
-smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req);
+XBT_INTERNAL smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req);
-const char* MC_smx_process_get_name(smx_process_t p);
-const char* MC_smx_process_get_host_name(smx_process_t p);
+XBT_INTERNAL const char* MC_smx_process_get_name(smx_process_t p);
+XBT_INTERNAL const char* MC_smx_process_get_host_name(smx_process_t p);
#define MC_EACH_SIMIX_PROCESS(process, code) \
if (mc_mode == MC_MODE_CLIENT) { \
}
/** Execute a given simcall */
-void MC_simcall_handle(smx_simcall_t req, int value);
+XBT_INTERNAL void MC_simcall_handle(smx_simcall_t req, int value);
-int MC_smpi_process_count(void);
+XBT_INTERNAL int MC_smpi_process_count(void);
/* ***** Resolve (local/MCer structure from remote/MCed addresses) ***** */
/** Get a local copy of the process from the process remote address */
-smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address);
+XBT_INTERNAL smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address);
/** Get the process info structure from the process remote address */
-mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address);
+XBT_INTERNAL mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address);
-unsigned long MC_smx_get_maxpid(void);
+XBT_INTERNAL unsigned long MC_smx_get_maxpid(void);
SG_END_DECL()
};
-mc_mem_region_t mc_region_new_sparse(
+MC_SHOULD_BE_INTERNAL mc_mem_region_t mc_region_new_sparse(
mc_region_type_t type, void *start_addr, void* data_addr, size_t size);
-void MC_region_destroy(mc_mem_region_t reg);
-void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg);
+MC_SHOULD_BE_INTERNAL void MC_region_destroy(mc_mem_region_t reg);
+XBT_INTERNAL void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg);
static inline __attribute__ ((always_inline))
bool mc_region_contain(mc_mem_region_t region, const void* p)
return (char*) snapshot_page + mc_page_offset((void*) addr);
}
-mc_mem_region_t mc_get_snapshot_region(const void* addr, mc_snapshot_t snapshot, int process_index);
+XBT_INTERNAL mc_mem_region_t mc_get_snapshot_region(
+ const void* addr, mc_snapshot_t snapshot, int process_index);
/** \brief Translate a pointer from process address space to snapshot address space
*
static const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot);
-mc_snapshot_t MC_take_snapshot(int num_state);
-void MC_restore_snapshot(mc_snapshot_t);
-void MC_free_snapshot(mc_snapshot_t);
+XBT_INTERNAL mc_snapshot_t MC_take_snapshot(int num_state);
+XBT_INTERNAL void MC_restore_snapshot(mc_snapshot_t);
+XBT_INTERNAL void MC_free_snapshot(mc_snapshot_t);
-size_t* mc_take_page_snapshot_region(mc_process_t process,
+XBT_INTERNAL size_t* mc_take_page_snapshot_region(mc_process_t process,
void* data, size_t page_count);
-void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
-void mc_restore_page_snapshot_region(
+XBT_INTERNAL void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
+XBT_INTERNAL void mc_restore_page_snapshot_region(
mc_process_t process,
void* start_addr, size_t page_count, size_t* pagenos);
-const void* MC_region_read_fragmented(mc_mem_region_t region, void* target, const void* addr, size_t size);
+MC_SHOULD_BE_INTERNAL const void* MC_region_read_fragmented(
+ mc_mem_region_t region, void* target, const void* addr, size_t size);
-const void* MC_snapshot_read(mc_snapshot_t snapshot, adress_space_read_flags_t flags,
+XBT_INTERNAL const void* MC_snapshot_read(mc_snapshot_t snapshot,
+ adress_space_read_flags_t flags,
void* target, const void* addr, size_t size, int process_index);
-int MC_snapshot_region_memcmp(
+MC_SHOULD_BE_INTERNAL int MC_snapshot_region_memcmp(
const void* addr1, mc_mem_region_t region1,
const void* addr2, mc_mem_region_t region2, size_t size);
-int MC_snapshot_memcmp(
+XBT_INTERNAL int MC_snapshot_memcmp(
const void* addr1, mc_snapshot_t snapshot1,
const void* addr2, mc_snapshot_t snapshot2, int process_index, size_t size);
SG_BEGIN_DECL()
-extern mc_global_t initial_global_state;
+extern XBT_INTERNAL mc_global_t initial_global_state;
/* Possible exploration status of a process in a state */
typedef enum {
xbt_dynar_t index_comm; // comm determinism verification
} s_mc_state_t, *mc_state_t;
-mc_state_t MC_state_new(void);
-void MC_state_delete(mc_state_t state, int free_snapshot);
-void MC_state_interleave_process(mc_state_t state, smx_process_t process);
-unsigned int MC_state_interleave_size(mc_state_t state);
-int MC_state_process_is_done(mc_state_t state, smx_process_t process);
-void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int value);
-smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value);
-smx_simcall_t MC_state_get_internal_request(mc_state_t state);
-smx_simcall_t MC_state_get_request(mc_state_t state, int *value);
-void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process);
+XBT_INTERNAL mc_state_t MC_state_new(void);
+XBT_INTERNAL void MC_state_delete(mc_state_t state, int free_snapshot);
+XBT_INTERNAL void MC_state_interleave_process(mc_state_t state, smx_process_t process);
+XBT_INTERNAL unsigned int MC_state_interleave_size(mc_state_t state);
+XBT_INTERNAL int MC_state_process_is_done(mc_state_t state, smx_process_t process);
+XBT_INTERNAL void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int value);
+XBT_INTERNAL smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value);
+XBT_INTERNAL smx_simcall_t MC_state_get_internal_request(mc_state_t state);
+XBT_INTERNAL smx_simcall_t MC_state_get_request(mc_state_t state, int *value);
+XBT_INTERNAL void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process);
SG_END_DECL()
*
* It works with the `s_mc_unw_context_t` context.
*/
-extern unw_accessors_t mc_unw_accessors;
+extern XBT_INTERNAL unw_accessors_t mc_unw_accessors;
// ***** Libunwind context
} s_mc_unw_context_t, *mc_unw_context_t;
/** Initialises an already allocated context */
-int mc_unw_init_context(
+XBT_INTERNAL int mc_unw_init_context(
mc_unw_context_t context, mc_process_t process, unw_context_t* c);
/** Destroys (but not not `free`) a context */
-int mc_unw_destroy_context(mc_unw_context_t context);
+XBT_INTERNAL int mc_unw_destroy_context(mc_unw_context_t context);
// ***** Libunwind cursor
/** Initialises a `libunwind` cursor */
-int mc_unw_init_cursor(unw_cursor_t *cursor, mc_unw_context_t context);
+XBT_INTERNAL int mc_unw_init_cursor(unw_cursor_t *cursor, mc_unw_context_t context);
SG_END_DECL()
SG_BEGIN_DECL();
-void MCer_ignore_global_variable(const char *var_name);
-void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
-void MC_heap_region_ignore_remove(void *address, size_t size);
-void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size);
+XBT_INTERNAL void MCer_ignore_global_variable(const char *var_name);
+XBT_INTERNAL void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
+XBT_INTERNAL void MC_heap_region_ignore_remove(void *address, size_t size);
+XBT_INTERNAL void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size);
SG_END_DECL();
