A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Add -Wformat-signedness to warnCFLAGS for GCC >= 5.0.
[simgrid.git]
/
doc
/
doxygen
/
uhood.doc
diff --git
a/doc/doxygen/uhood.doc
b/doc/doxygen/uhood.doc
index
be3ce71
..
7a750df
100644
(file)
--- a/
doc/doxygen/uhood.doc
+++ b/
doc/doxygen/uhood.doc
@@
-205,7
+205,7
@@
The current implementation of the model-checker uses two distinct processes:
- the SimGrid model-checker (`simgrid-mc`) itself lives in the parent process;
- the SimGrid model-checker (`simgrid-mc`) itself lives in the parent process;
- - it spaws a child process for the SimGrid simulator/mastro and the simulated
+ - it spaws a child process for the SimGrid simulator/ma
e
stro and the simulated
processes.
They communicate using a `AF_UNIX` `SOCK_DGRAM` socket and exchange messages
processes.
They communicate using a `AF_UNIX` `SOCK_DGRAM` socket and exchange messages
@@
-215,15
+215,15
@@
set to the file descriptor of this socket in the child process.
The model-checker analyzes, saves and restores the state of the model-checked
process using the following techniques:
The model-checker analyzes, saves and restores the state of the model-checked
process using the following techniques:
-
*
the model-checker reads and writes in the model-checked address space;
+
-
the model-checker reads and writes in the model-checked address space;
-
*
the model-cheker `ptrace()`s the model-checked process and is thus able to
+
-
the model-cheker `ptrace()`s the model-checked process and is thus able to
know the state of the model-checked process if it crashes;
know the state of the model-checked process if it crashes;
-
*
DWARF debug informations are used to unwind the stack and identify local
+
-
DWARF debug informations are used to unwind the stack and identify local
variables;
variables;
-
*
a custom heap is enabled in the model-checked process which allows the model
+
-
a custom heap is enabled in the model-checked process which allows the model
checker to know which chunks are allocated and which are freed.
\subsection simgrid_uhood_mc_address_space Address space
checker to know which chunks are allocated and which are freed.
\subsection simgrid_uhood_mc_address_space Address space