Marion Guthmuller [Tue, 25 Oct 2011 12:36:24 +0000 (14:36 +0200)]
model-checker : remove unused variables
Marion Guthmuller [Tue, 25 Oct 2011 11:21:28 +0000 (13:21 +0200)]
model-checker : function to compare propositional symbol values
Marion Guthmuller [Tue, 25 Oct 2011 08:47:11 +0000 (10:47 +0200)]
model-checker : change printf for size_t variables
Marion Guthmuller [Fri, 21 Oct 2011 12:27:46 +0000 (14:27 +0200)]
model-checker : test data in libsimgrid memory region between each state
Marion Guthmuller [Wed, 12 Oct 2011 15:06:29 +0000 (17:06 +0200)]
model-checker : new functions to compare mmalloc in std_heap
Marion Guthmuller [Tue, 4 Oct 2011 07:52:30 +0000 (09:52 +0200)]
model-checker : add type in s_mc_mem_region (0=std_heap, 1=libsimgrid)
Marion Guthmuller [Thu, 22 Sep 2011 16:12:01 +0000 (18:12 +0200)]
model-checker : add files for examples
Marion Guthmuller [Thu, 22 Sep 2011 16:05:17 +0000 (18:05 +0200)]
model-checker : nettoyage du code
Marion Guthmuller [Wed, 21 Sep 2011 14:59:05 +0000 (16:59 +0200)]
model-checker : new comparison for reached pairs (automaton state + values of propositional symbols + snapshot of system state)
Marion Guthmuller [Thu, 15 Sep 2011 15:40:24 +0000 (17:40 +0200)]
model-checker : new comparison of pair reached (automaton state + values of propositional symbols)
Marion Guthmuller [Tue, 13 Sep 2011 15:56:54 +0000 (17:56 +0200)]
model-checker : delete visited in struct xbt_state_t (unused)
Marion Guthmuller [Mon, 12 Sep 2011 13:24:43 +0000 (15:24 +0200)]
model-checker : delete struct reached_pair_stateless unused
Marion Guthmuller [Mon, 12 Sep 2011 12:58:30 +0000 (14:58 +0200)]
model-checker : delete num in struct mc_pair_t
Marion Guthmuller [Fri, 9 Sep 2011 15:52:13 +0000 (17:52 +0200)]
model-checker : empty pair for stateless ddfs fixed
Marion Guthmuller [Tue, 23 Aug 2011 16:46:29 +0000 (18:46 +0200)]
model-checker : ddfs stateless and stateful fixed
Marion Guthmuller [Mon, 22 Aug 2011 09:27:09 +0000 (11:27 +0200)]
model-checker : update ddfs stateful model checking for liveness properties, bug with stateless mode
Marion Guthmuller [Sun, 21 Aug 2011 11:02:18 +0000 (13:02 +0200)]
model-checker : new structure reached_pair_stateless for acceptance cyle detection
Marion Guthmuller [Sun, 21 Aug 2011 09:37:04 +0000 (11:37 +0200)]
model-checker : stateless model checking for liveness properties
Marion Guthmuller [Sat, 20 Aug 2011 15:24:24 +0000 (17:24 +0200)]
model-checker : separate informations for safety stateful/stateless and liveness stateful/stateless
Marion Guthmuller [Tue, 16 Aug 2011 14:01:23 +0000 (16:01 +0200)]
model-checker : new example bugged1 for stateful dpor
Marion Guthmuller [Wed, 20 Jul 2011 12:57:24 +0000 (14:57 +0200)]
model-checker : one more condition before interleaving process in state
Marion Guthmuller [Tue, 19 Jul 2011 16:10:51 +0000 (18:10 +0200)]
model-checker : add condition of invisibility to reduce transitions
Marion Guthmuller [Tue, 5 Jul 2011 10:20:04 +0000 (12:20 +0200)]
model-checker : new structure mc_pair_prop_t and backup of the values of atomic propositions for each state
Marion Guthmuller [Tue, 5 Jul 2011 09:16:08 +0000 (11:16 +0200)]
model-checker : DPOR (independant transitions) algorithm for liveness properties
Marion Guthmuller [Fri, 1 Jul 2011 15:02:03 +0000 (17:02 +0200)]
model-checker : separate dfs and dpor algorithms with restore snapshot/replay or visited states
Marion Guthmuller [Fri, 24 Jun 2011 15:20:26 +0000 (17:20 +0200)]
model-checker : example changed
Marion Guthmuller [Fri, 24 Jun 2011 13:44:19 +0000 (15:44 +0200)]
model-checker : 128bits->160bits for hash of visited pair
Marion Guthmuller [Fri, 24 Jun 2011 12:30:42 +0000 (14:30 +0200)]
model-checker : restore interleaved process when restore snapshot
Marion Guthmuller [Fri, 24 Jun 2011 12:24:47 +0000 (14:24 +0200)]
model-checker : dfs with good restore snapshot
Marion Guthmuller [Fri, 24 Jun 2011 09:51:08 +0000 (11:51 +0200)]
model-checker : correction of dfs algorithm for liveness properties
Marion Guthmuller [Mon, 20 Jun 2011 14:00:37 +0000 (16:00 +0200)]
model-checker : test dpor without replay from initial state but with
restore snapshot -> ok for safety properties, need more specifications
for liveness
Marion Guthmuller [Fri, 17 Jun 2011 07:13:40 +0000 (09:13 +0200)]
model-checker : rename file mc_dfs -> mc_liveness
Marion Guthmuller [Fri, 20 May 2011 16:14:01 +0000 (18:14 +0200)]
MC LTL : last version dfs algorithm before reduction
Marion Guthmuller [Fri, 20 May 2011 08:41:01 +0000 (10:41 +0200)]
MC LTL : add statistics
Marion Guthmuller [Thu, 19 May 2011 15:41:45 +0000 (17:41 +0200)]
model checker : dfs algorithm corrected
Marion Guthmuller [Wed, 4 May 2011 14:26:47 +0000 (16:26 +0200)]
model-check : show stack when property not valid
Marion Guthmuller [Wed, 4 May 2011 14:18:02 +0000 (16:18 +0200)]
model-check : dump stack for acceptance cycle
Marion Guthmuller [Wed, 4 May 2011 14:07:05 +0000 (16:07 +0200)]
model-check : show stack for acceptance cycle
Marion Guthmuller [Wed, 4 May 2011 11:45:41 +0000 (13:45 +0200)]
model check : acceptance cycle detection with automaton (depth first search without dpor)
Marion Guthmuller [Fri, 29 Apr 2011 08:31:48 +0000 (10:31 +0200)]
détection de cycle d'acceptation ok mais boucle infinie en cas d'absence de cycle
Marion Guthmuller [Thu, 21 Apr 2011 09:32:22 +0000 (11:32 +0200)]
correction compile warnings
Marion Guthmuller [Thu, 21 Apr 2011 08:44:17 +0000 (10:44 +0200)]
start new example with parsing lex/yacc of automaton in promela
Marion Guthmuller [Thu, 21 Apr 2011 08:35:11 +0000 (10:35 +0200)]
include new files struct automaton for cmake
Marion Guthmuller [Thu, 21 Apr 2011 08:25:50 +0000 (10:25 +0200)]
new dfs algorithm with automaton of LTL formula
Marion Guthmuller [Thu, 21 Apr 2011 08:10:51 +0000 (10:10 +0200)]
new struct automaton
Navarrop [Fri, 21 Oct 2011 11:07:27 +0000 (13:07 +0200)]
You can now specify if you want sleep to see memory usage.
Navarrop [Fri, 21 Oct 2011 10:32:56 +0000 (12:32 +0200)]
Optimize bprintf during cluster loop.
Navarrop [Fri, 21 Oct 2011 10:32:35 +0000 (12:32 +0200)]
Add optimization flag with gcc46.
Martin Quinson [Thu, 20 Oct 2011 14:17:35 +0000 (16:17 +0200)]
use more consistently the resource create of models, killing some useless/borken forwarder methods
Martin Quinson [Thu, 20 Oct 2011 14:15:56 +0000 (16:15 +0200)]
save some useless strdups
Martin Quinson [Thu, 20 Oct 2011 13:20:32 +0000 (15:20 +0200)]
reduce the amount of damn paranoid checks in simdag. Valgrind is here to report the errors, nowadays
Navarrop [Thu, 20 Oct 2011 12:42:56 +0000 (14:42 +0200)]
Fix memoryleak.
Navarrop [Thu, 20 Oct 2011 12:42:33 +0000 (14:42 +0200)]
Need to set state_file and availability file into the loop.
Christophe Thiéry [Thu, 20 Oct 2011 12:02:25 +0000 (14:02 +0200)]
There is no contexts in SimDag
Navarrop [Thu, 20 Oct 2011 11:22:19 +0000 (13:22 +0200)]
Rewrite perl script for optorsim
Navarrop [Thu, 20 Oct 2011 11:21:56 +0000 (13:21 +0200)]
Update include tag.
Navarrop [Thu, 20 Oct 2011 11:21:18 +0000 (13:21 +0200)]
Move arguments outside of the loop of hosts.
Navarrop [Thu, 20 Oct 2011 09:14:17 +0000 (11:14 +0200)]
Remove unused and old function.
Navarrop [Thu, 20 Oct 2011 09:11:25 +0000 (11:11 +0200)]
Remove supernovae mode for SimGrid v3.7
Navarrop [Thu, 20 Oct 2011 09:10:23 +0000 (11:10 +0200)]
Test the help command.
Navarrop [Mon, 17 Oct 2011 15:35:37 +0000 (17:35 +0200)]
Update tag include
Martin Quinson [Thu, 20 Oct 2011 11:26:50 +0000 (13:26 +0200)]
Merge branch 'master' of scm.gforge.inria.fr:/gitroot/simgrid/simgrid
Martin Quinson [Thu, 20 Oct 2011 11:26:28 +0000 (13:26 +0200)]
setup a mallocator for the simdag tasks. The gain is quite disapointing, but not null
Martin Quinson [Thu, 20 Oct 2011 11:24:15 +0000 (13:24 +0200)]
memory cleanups
Arnaud Giersch [Tue, 18 Oct 2011 07:41:02 +0000 (09:41 +0200)]
s/GRAS_STUB_GENERATOR/SIMGRID_LUA/ to actually match file name.
Arnaud Giersch [Tue, 18 Oct 2011 07:40:24 +0000 (09:40 +0200)]
Guard against multiple inclusion.
Arnaud Giersch [Fri, 14 Oct 2011 11:38:25 +0000 (13:38 +0200)]
Fix race condition with gras-mmrpc test.
Register messages before opening the sockets, to avoid to receive
unknown messages.
Arnaud Giersch [Tue, 11 Oct 2011 11:17:40 +0000 (13:17 +0200)]
Figlet for 3.7 was incomplete.
Also do some whitespace cleanup (and save up to 247 bytes!).
Arnaud Giersch [Thu, 20 Oct 2011 09:21:18 +0000 (11:21 +0200)]
tesh: add tests with empty output.
Arnaud Giersch [Thu, 20 Oct 2011 09:20:58 +0000 (11:20 +0200)]
tesh: do not fail on empty output, when sorting is enabled.
Martin Quinson [Thu, 20 Oct 2011 08:27:04 +0000 (10:27 +0200)]
Merge stuff again. Damn, I should pull before changing stuff
Martin Quinson [Thu, 20 Oct 2011 08:25:30 +0000 (10:25 +0200)]
merge branches
Martin Quinson [Thu, 20 Oct 2011 08:19:18 +0000 (10:19 +0200)]
use a user level mallocator on the task content
Martin Quinson [Thu, 20 Oct 2011 08:17:59 +0000 (10:17 +0200)]
enlarge my cluster once again
Martin Quinson [Thu, 20 Oct 2011 08:11:44 +0000 (10:11 +0200)]
Performance boost by using a swag internally in SD_simulate
Martin Quinson [Thu, 20 Oct 2011 07:47:59 +0000 (09:47 +0200)]
Use the partial invalidation optimization by default for the network too
Christophe Thiéry [Thu, 20 Oct 2011 06:39:27 +0000 (08:39 +0200)]
This memory leak fix did not work with complex simulations.
Christophe Thiéry [Thu, 20 Oct 2011 06:39:03 +0000 (08:39 +0200)]
SIMIX_CANCELED is a more adapted state in SIMIX_comm_cancel()
Martin Quinson [Wed, 19 Oct 2011 19:48:16 +0000 (21:48 +0200)]
restore some stuff that got killed from the gitignore during some sort of cleanup
Martin Quinson [Wed, 19 Oct 2011 19:47:44 +0000 (21:47 +0200)]
enlarge my cluster
Martin Quinson [Wed, 19 Oct 2011 19:47:23 +0000 (21:47 +0200)]
first prealpha not working prototype (please public keep away) version of what could be a GOAL loader using simdag
Martin Quinson [Wed, 19 Oct 2011 19:43:59 +0000 (21:43 +0200)]
typo--
Navarrop [Mon, 17 Oct 2011 13:59:15 +0000 (15:59 +0200)]
Add example to kill a process.
Christophe Thiéry [Fri, 14 Oct 2011 15:57:31 +0000 (17:57 +0200)]
Timings have changed: comms cannot continue when a process is dead
Christophe Thiéry [Fri, 14 Oct 2011 15:54:51 +0000 (17:54 +0200)]
Now that processes are terminated cleanly, this recv can fail
Christophe Thiéry [Fri, 14 Oct 2011 15:46:45 +0000 (17:46 +0200)]
In case of failures, a process may become runnable without time step
Since commit
e5922b4 (clean unfinished comms when terminating a process),
the test msg-actions was failing on a deadlock instead of waking up
the last process (who can terminate normally after a failed recv).
Christophe Thiéry [Fri, 14 Oct 2011 15:46:08 +0000 (17:46 +0200)]
Improve debug messages
Christophe Thiéry [Fri, 14 Oct 2011 15:09:29 +0000 (17:09 +0200)]
Revalidate Chord tesh output (the end of the simulation is clean now)
Christophe Thiéry [Fri, 14 Oct 2011 15:09:00 +0000 (17:09 +0200)]
Make cancelling a non-running task a no-op
Christophe Thiéry [Fri, 14 Oct 2011 15:04:28 +0000 (17:04 +0200)]
Fix remaining memory leaks in MSG
Christophe Thiéry [Fri, 14 Oct 2011 13:38:20 +0000 (15:38 +0200)]
Simix: clean unfinished comms when terminating a process
Christophe Thiéry [Thu, 13 Oct 2011 15:44:57 +0000 (17:44 +0200)]
Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot//simgrid/simgrid
Christophe Thiéry [Thu, 13 Oct 2011 14:45:05 +0000 (16:45 +0200)]
Fighting more memory leaks in Chord
Lucas Schnorr [Thu, 13 Oct 2011 13:21:59 +0000 (15:21 +0200)]
[trace] fix tesh'es to follow recent changes in the paje header
Navarrop [Thu, 13 Oct 2011 13:14:29 +0000 (15:14 +0200)]
Reorganize platforms for optorsim.
Add scripts into the right directory.
Christophe Thiéry [Thu, 13 Oct 2011 13:05:35 +0000 (15:05 +0200)]
Fix a memory leak in chord
Navarrop [Thu, 13 Oct 2011 13:00:08 +0000 (15:00 +0200)]
Update index.doc to have the right references to url.
Navarrop [Thu, 13 Oct 2011 12:59:21 +0000 (14:59 +0200)]
Add host core to "1.0" for tag peer.
Christophe Thiéry [Thu, 13 Oct 2011 12:01:15 +0000 (14:01 +0200)]
Revert msg-actions to an older and more stable version
Christophe Thiéry [Thu, 13 Oct 2011 11:47:21 +0000 (13:47 +0200)]
Merge branch 'lua'
Conflicts:
buildtools/Cmake/AddTests.cmake