/** Process index used when no process is available
*
- * The expected behaviour is that if a process index is needed it will fail.
+ * The expected behavior is that if a process index is needed it will fail.
* */
const int ProcessIndexMissing = -1;
/** A channel for exchanging messages between model-checker and model-checked
*
- * This hides the way the messages are transfered. Currently, they are sent
+ * This hides the way the messages are transferred. Currently, they are sent
* over a SOCK_DGRAM socket.
*/
class Channel {
/** A model-checking algorithm
*
* The goal is to move the data/state/configuration of a model-checking
- * algorihms in subclasses. Implementing this interface will probably
+ * algorithms in subclasses. Implementing this interface will probably
* not be really mandatory, you might be able to write your
* model-checking algorithm as plain imperative code instead.
*
#include <vector>
-#include <xbt/misc.h> // xbt_pagesize and friends
+#include <xbt/misc.h>
#include <xbt/asserts.h>
#include "src/mc/AddressSpace.hpp"
/** Take a per-page snapshot of a region
*
* @param data The start of the region (must be at the beginning of a page)
- * @param pag_count Number of pages of the region
+ * @param page_count Number of pages of the region
* @return Snapshot page numbers of this new snapshot
*/
ChunkedData::ChunkedData(PageStore& store, AddressSpace& as,
std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
/* If comm determinism verification, we cannot stop the exploration if
- some communications are not finished (at least, data are transfered).
+ some communications are not finished (at least, data are transferred).
These communications are incomplete and they cannot be analyzed and
compared with the initial pattern. */
bool compare_snapshots = all_communications_are_finished()
break;
}
- // Push the CFA (Canonical Frame Addresse):
+ // Push the CFA (Canonical Frame Address):
case DW_OP_call_frame_cfa:
{
/* See 6.4 of DWARF4 (http://dwarfstd.org/doc/DWARF4.pdf#page=140):
*
* An offset is applied to address found in DWARF:
*
- * * for an executable obejct, addresses are virtual address
+ * * for an executable object, addresses are virtual address
* (there is no offset) i.e.
* \f$\text{virtual address} = \{dwarf address}\f$;
*
* during the binary search (only at the end) so it is not included
* in the index entry. We could use parallel arrays as well.
*
- * We cannot really use the std:: alogrithm for this.
+ * We cannot really use the std:: algorithm for this.
* We could use std::binary_search by including the high_pc inside
* the FunctionIndexEntry.
*/
/* At this point, the search is over.
* Either we have found the correct function or we do not know
* any function corresponding to this instruction address.
- * Only at the point do we derefernce the function pointer. */
+ * Only at the point do we dereference the function pointer. */
else if ((std::uint64_t) ip < base[k].function->range.end())
return base[k].function;
else
* name.
*
* \param var_name Name of the local variable (or parameter to ignore)
- * \param subprogram_name Name of the subprogram fo ignore (nullptr for any)
+ * \param subprogram_name Name of the subprogram to ignore (nullptr for any)
* \param subprogram (possibly inlined) Subprogram of the scope
* \param scope Current scope
*/
* under the terms of the license (GNU LGPL) which comes with this package. */
#include <unistd.h>
-#include <string.h> // memcpy, memcp
+#include <string.h> // memcpy, memcmp
#include <sys/mman.h>
namespace simgrid {
namespace mc {
-/** @brief Compte a hash for the given memory page
+/** @brief Compute a hash for the given memory page
*
* The page is used before inserting the page in the page store
* in order to find duplicate of this page in the page store.
/** Refresh the information about the process
*
- * Do not use direclty, this is used by the getters when appropriate
+ * Do not use directly, this is used by the getters when appropriate
* in order to have fresh data.
*/
void Process::refresh_heap()
regfree(&res.so_re);
regfree(&res.version_re);
- // Resolve time (including accross differents objects):
+ // Resolve time (including across different objects):
for (auto const& object_info : this->object_infos)
postProcessObjectInformation(this, object_info.get());
return info ? info->find_function((void*) ip.address()) : nullptr;
}
-/** Find (one occurence of) the named variable definition
+/** Find (one occurrence of) the named variable definition
*/
simgrid::mc::Variable* Process::find_variable(const char* name) const
{
// First lookup the variable in the executable shared object.
// A global variable used directly by the executable code from a library
// is reinstanciated in the executable memory .data/.bss.
- // We need to look up the variable in the execvutable first.
+ // We need to look up the variable in the executable first.
if (this->binary_info) {
std::shared_ptr<simgrid::mc::ObjectInformation> const& info = this->binary_info;
simgrid::mc::Variable* var = info->find_variable(name);
mc_model_checker->process().read<s_smpi_privatisation_region_t>(
remote(remote_smpi_privatisation_regions + process_index));
- // Address translation in the privaization segment:
+ // Address translation in the privatization segment:
size_t offset = address.address() - (std::uint64_t)info->start_rw;
address = remote((char*)privatisation_region.address + offset);
}
/** Representation of a process
*
- * This class is mixing a lot of different responsabilities and is tied
+ * This class is mixing a lot of different responsibilities and is tied
* to SIMIX. It should probably be split into different classes.
*
- * Responsabilities:
+ * Responsibilities:
*
* - reading from the process memory (`AddressSpace`);
- * - accessing the system state of the porcess (heap, …);
+ * - accessing the system state of the process (heap, …);
* - storing the SIMIX state of the process;
* - privatization;
* - communication with the model-checked process;
*/
unw_addr_space_t unw_addr_space;
- /** Underlying libunwind addres-space
+ /** Underlying libunwind address-space
*
* The `find_proc_info`, `put_unwind_info`, `get_dyn_info_list_addr`
* operations of the native MC address space is currently delegated
void *start_addr, void* permanent_addr, size_t size)
{
// When KSM support is enables, we allocate memory using mmap:
- // * we don't want to madvise bits of the heap;
+ // * we don't want to advise bits of the heap as mergable;
// * mmap gives data aligned on page boundaries which is merge friendly.
simgrid::mc::Buffer data;
if (_sg_mc_ksm)
*
* * privatized (SMPI global variable privatisation).
*
- * This is handled with a variant based approch:
+ * This is handled with a variant based approach:
*
* * `storage_type` identified the type of storage;
*
/** An element in the recorded path
*
* At each decision point, we need to record which process transition
- * is trigerred and potentially which value is associated with this
- * transition. The value is used to find which communication is triggerred
+ * is triggered and potentially which value is associated with this
+ * transition. The value is used to find which communication is triggered
* in things like waitany and for associating a given value of MC_random()
* calls.
*/
#include "src/mc/Client.hpp"
#include "src/mc/ModelChecker.hpp"
-/** \file mc_client_api.cpp
+/** @file mc_client_api.cpp
*
* This is the implementation of the API used by the user simulated program to
* communicate with the MC (declared in modelchecker.h).
/** @brief Register a stack in the model checker
*
* The stacks are allocated in the heap. The MC handle them especially
- * when we analyse/compare the content of the heap so it must be told where
+ * when we analyze/compare the content of the heap so it must be told where
* they are with this function.
*
* @param stack
SG_BEGIN_DECL()
/**
- * Type: `xbt_dynar_t<mc_list_comm_pattenr_t>`
+ * Type: `xbt_dynar_t<mc_list_comm_pattern_t>`
*/
extern XBT_PRIVATE xbt_dynar_t initial_communications_pattern;
*
* The default for a given language is defined in the DWARF spec.
*
- * \param language consant as defined by the DWARf spec
+ * \param language constant as defined by the DWARf spec
*/
static uint64_t MC_dwarf_default_lower_bound(int lang);
* \param info the resulting object fot the library/binary file (output)
* \param die the current DIE
* \param unit the DIE of the compile unit of the current DIE
- * \param frame containg frame if any
+ * \param frame containing frame if any
*/
static void MC_dwarf_handle_die(simgrid::mc::ObjectInformation* info, Dwarf_Die * die,
Dwarf_Die * unit, simgrid::mc::Frame* frame,
Dwarf_Die * unit, simgrid::mc::Frame* frame,
const char *ns);
-/** \brief Calls MC_dwarf_handle_die on all childrend of the given die
+/** \brief Calls MC_dwarf_handle_die on all children of the given die
*
* \param info the resulting object fot the library/binary file (output)
* \param die the current DIE
* \param unit the DIE of the compile unit of the current DIE
- * \param frame containg frame if any
+ * \param frame containing frame if any
*/
static void MC_dwarf_handle_children(simgrid::mc::ObjectInformation* info, Dwarf_Die * die,
Dwarf_Die * unit, simgrid::mc::Frame* frame,
* \param info the resulting object fot the library/binary file (output)
* \param die the current DIE
* \param unit the DIE of the compile unit of the current DIE
- * \param frame containg frame if any
+ * \param frame containing frame if any
*/
static void MC_dwarf_handle_variable_die(simgrid::mc::ObjectInformation* info, Dwarf_Die * die,
Dwarf_Die * unit, simgrid::mc::Frame* frame,
if (boost::algorithm::starts_with(member.name, "__vptr$") ||
boost::algorithm::starts_with(member.name, "__vptr."))
member.flags |= simgrid::mc::Member::VIRTUAL_POINTER_FLAG;
- // A cleaner stolution would be to check against the type:
+ // A cleaner solution would be to check against the type:
// ---
// tag: DW_TAG_member
// name: "_vptr$Foo"
*
* DWARF and libunwind does not use the same convention for numbering the
* registers on some architectures. The function makes the necessary
- * convertion.
+ * conversion.
*/
int dwarf_register_to_libunwind(int dwarf_register)
{
// It seems for this arch, DWARF and libunwind agree in the numbering:
return dwarf_register;
#elif defined(__i386__)
- // Could't find the authoritative source of information for this.
+ // Couldn't find the authoritative source of information for this.
// This is inspired from http://source.winehq.org/source/dlls/dbghelp/cpu_i386.c#L517.
switch (dwarf_register) {
case 0:
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
-/** \file mc_forward.hpp
+/** @file mc_forward.hpp
*
* Forward definitions for MC types
*/
if (r1->issuer == r2->issuer)
return false;
- /* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */
+ /* Wait with timeout transitions are not considered by the independence theorem, thus we consider them as dependant with all other transitions */
if ((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0)
|| (r2->call == SIMCALL_COMM_WAIT
&& simcall_comm_wait__get__timeout(r2) > 0))
/* HACK, Horrible hack to find the offset of the id in the simgrid::s4u::Host.
Offsetof is not supported for non-POD types but this should
- work in pratice for the targets currently supported by the MC
+ work in practice for the targets currently supported by the MC
as long as we do not add funny features to the Host class
(such as virtual base).
#ifndef SIMGRID_MC_UNW_H
#define SIMGRID_MC_UNW_H
-/** \file
+/** @file
* Libunwind implementation for the model-checker
*
* Libunwind provides an pluggable stack unwinding API: the way the current
* Copies noncontiguous data into contiguous memory.
* @param contiguous_vector - output vector
* @param noncontiguous_vector - input vector
- * @param type - pointer contening :
+ * @param type - pointer containing :
* - stride - stride of between noncontiguous data
* - block_length - the width or height of blocked matrix
* - count - the number of rows of matrix
}
/* Create a Sub type contiguous to be able to serialize and unserialize it the structure s_smpi_mpi_contiguous_t is
- * erived from s_smpi_subtype which required the functions unserialize and serialize */
+ * derived from s_smpi_subtype which required the functions unserialize and serialize */
s_smpi_mpi_contiguous_t* smpi_datatype_contiguous_create( MPI_Aint lb, int block_count, MPI_Datatype old_type,
int size_oldtype){
if(block_count==0)
DT_FLAG_VECTOR);
retval=MPI_SUCCESS;
}else{
- /* in this situation the data are contignous thus it's not required to serialize and unserialize it*/
+ /* in this situation the data are contiguous thus it's not required to serialize and unserialize it*/
smpi_datatype_create(new_type, count * blocklen * smpi_datatype_size(old_type), 0, ((count -1) * stride + blocklen)*
smpi_datatype_size(old_type), 0, nullptr, DT_FLAG_VECTOR|DT_FLAG_CONTIGUOUS);
retval=MPI_SUCCESS;
+ABI
addtogroup
+addr
API
+api
argc
argv
atof
callgrind
calloc
cfg
+comm
const
cplusplus
+cpp
+cpu
defgroup
dict
dicts
GPU
hideinitializer
hpp
+http
+https
inlining
ingroup
int
KILLME
lat
LGPL
+libdw
+libunwind
lmm
LTL
malloc
Mbytes
mc
+MCed
+MCer
+memcpy
+memcmp
Mflops
+mmap
+ModelChecker
+modelchecker
MPI
msg
+mutex
nullptr
ok
Paje
param
pid
printf
+proc
pstate
RngStream
SD
SIMIX
sizeof
SMPI
+smpi
smx
src
+std
struct
syscall
+syscalls
tesh
+testany
todo
TODO
valgrind
VM
VMs
+waitany
xbt
XBT
xml
