From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Fri, 28 Feb 2014 08:33:45 +0000 (+0100)
Subject: Merge branch 'mc++' into mc-merge
X-Git-Tag: v3_11~199^2~2^2~22
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/6de03ecc4e630732984a0673512a5d15fd75e270?hp=45c3f1cfee86fb48c96d53f8267f99b6db6e3d7a

Merge branch 'mc++' into mc-merge
---

diff --git a/examples/msg/mc/bugged1.tesh b/examples/msg/mc/bugged1.tesh
index bcebdf8c9d..504b90e1ad 100644
--- a/examples/msg/mc/bugged1.tesh
+++ b/examples/msg/mc/bugged1.tesh
@@ -24,16 +24,16 @@ $ ${bindir:=.}/bugged1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%
 > [  0.000000] (1:server@HostA) *** PROPERTY NOT VALID ***
 > [  0.000000] (1:server@HostA) **************************
 > [  0.000000] (1:server@HostA) Counter-example execution trace:
-> [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (1:server@HostA) [(2)HostB (client)] iSend(src=(2)HostB (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)]) (62)
-> [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (1:server@HostA) [(2)HostB (client)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)]) (62)
-> [  0.000000] (1:server@HostA) [(4)HostD (client)] iSend(src=(4)HostD (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(4)HostD (client)-> (1)HostA (server)]) (62)
-> [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)]) (62)
+> [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (1:server@HostA) [(2)HostB (client)] iSend(src=(2)HostB (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)])
+> [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (1:server@HostA) [(2)HostB (client)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)])
+> [  0.000000] (1:server@HostA) [(4)HostD (client)] iSend(src=(4)HostD (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(4)HostD (client)-> (1)HostA (server)])
+> [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
 > [  0.000000] (1:server@HostA) Expanded states = 22
 > [  0.000000] (1:server@HostA) Visited states = 56
 > [  0.000000] (1:server@HostA) Executed transitions = 52
diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh
index 37652b8a59..fd34555a56 100644
--- a/examples/msg/mc/bugged1_liveness.tesh
+++ b/examples/msg/mc/bugged1_liveness.tesh
@@ -20,26 +20,26 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../msg_platform.xml ${srcdir:=.}/de
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) Counter-example that violates formula :
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(3)Fafard (client)] iRecv(dst=(3)Fafard (client), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (3)Fafard (client)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (3)Fafard (client)]) (62)
-> [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) (62)
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(3)Fafard (client)] iRecv(dst=(3)Fafard (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (3)Fafard (client)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (3)Fafard (client)])
+> [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
 > [  0.000000] (0:@) Expanded pairs = 21
 > [  0.000000] (0:@) Visited pairs = 21
 > [  0.000000] (0:@) Executed transitions = 20
diff --git a/examples/msg/mc/bugged1_liveness_visited.tesh b/examples/msg/mc/bugged1_liveness_visited.tesh
index f8042cb656..f117bb4b22 100644
--- a/examples/msg/mc/bugged1_liveness_visited.tesh
+++ b/examples/msg/mc/bugged1_liveness_visited.tesh
@@ -78,56 +78,56 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../msg_platform.xml ${srcdir:=.}/de
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) Counter-example that violates formula :
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
+> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
 > [  0.000000] (0:@) Expanded pairs = 57
 > [  0.000000] (0:@) Visited pairs = 208
 > [  0.000000] (0:@) Executed transitions = 207
diff --git a/examples/msg/mc/bugged2.tesh b/examples/msg/mc/bugged2.tesh
index df06aafaaf..3d65e677e7 100644
--- a/examples/msg/mc/bugged2.tesh
+++ b/examples/msg/mc/bugged2.tesh
@@ -889,13 +889,13 @@ $ ${bindir:=.}/bugged2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%
 > [  0.000000] (1:server@HostA) *** PROPERTY NOT VALID ***
 > [  0.000000] (1:server@HostA) **************************
 > [  0.000000] (1:server@HostA) Counter-example execution trace:
-> [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)]) (62)
-> [  0.000000] (1:server@HostA) [(3)HostC (client)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)]) (62)
-> [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)]) (62)
+> [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [  0.000000] (1:server@HostA) [(3)HostC (client)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [  0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
 > [  0.000000] (1:server@HostA) Expanded states = 461
 > [  0.000000] (1:server@HostA) Visited states = 2271
 > [  0.000000] (1:server@HostA) Executed transitions = 2117
diff --git a/examples/smpi/CMakeLists.txt b/examples/smpi/CMakeLists.txt
index 154b3d585b..9afad64a60 100644
--- a/examples/smpi/CMakeLists.txt
+++ b/examples/smpi/CMakeLists.txt
@@ -23,10 +23,14 @@ if(enable_smpi)
     add_executable(mc/bugged1 mc/bugged1.c)
     add_executable(mc/bugged2 mc/bugged2.c)
     add_executable(mc/bugged1_liveness mc/bugged1_liveness.c)
+    add_executable(mc/send_deterministic mc/send_deterministic.c)
+    add_executable(mc/non_deterministic mc/non_deterministic.c)
   
     target_link_libraries(mc/bugged1 simgrid)
     target_link_libraries(mc/bugged2 simgrid)
     target_link_libraries(mc/bugged1_liveness simgrid)
+    target_link_libraries(mc/send_deterministic simgrid)
+    target_link_libraries(mc/non_deterministic simgrid)
   endif()
   
   target_link_libraries(bcbench simgrid)
@@ -58,6 +62,8 @@ set(examples_src
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged2.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1_liveness.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/send_deterministic.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_deterministic.c
   PARENT_SCOPE
   )
 set(bin_files
@@ -67,6 +73,8 @@ set(bin_files
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1_liveness
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged2
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_send_deterministic
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_non_deterministic
   PARENT_SCOPE
   )
 set(txt_files
diff --git a/examples/smpi/mc/hostfile_non_deterministic b/examples/smpi/mc/hostfile_non_deterministic
new file mode 100644
index 0000000000..b6d1c07b45
--- /dev/null
+++ b/examples/smpi/mc/hostfile_non_deterministic
@@ -0,0 +1,3 @@
+c-1.me
+c-2.me
+c-3.me
diff --git a/examples/smpi/mc/hostfile_send_deterministic b/examples/smpi/mc/hostfile_send_deterministic
new file mode 100644
index 0000000000..b6d1c07b45
--- /dev/null
+++ b/examples/smpi/mc/hostfile_send_deterministic
@@ -0,0 +1,3 @@
+c-1.me
+c-2.me
+c-3.me
diff --git a/examples/smpi/mc/non_deterministic.c b/examples/smpi/mc/non_deterministic.c
new file mode 100644
index 0000000000..b73cbd2e67
--- /dev/null
+++ b/examples/smpi/mc/non_deterministic.c
@@ -0,0 +1,54 @@
+/* ../../../smpi_script/bin/smpirun -hostfile hostfile_send_deterministic -platform ../../platforms/cluster.xml -np 3 --cfg=model-check:1 --cfg=smpi/send_is_detached_thres:0 gdb\ --args\ ./send_deterministic */
+
+/* Copyright (c) 2009 - 2014. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* 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. */
+
+#include <stdio.h>
+#include <mpi.h>
+#include <simgrid/modelchecker.h>
+
+
+int main(int argc, char **argv)
+{
+  int recv_buff, err, size, rank, i;
+  MPI_Status status;
+
+  /* Initialize MPI */
+  err = MPI_Init(&argc, &argv);
+  if (err != MPI_SUCCESS) {
+    printf("MPI initialization failed!\n");
+    exit(1);
+  }
+
+  err = MPI_Comm_size(MPI_COMM_WORLD, &size);   /* Get nr of tasks */
+  err = MPI_Comm_rank(MPI_COMM_WORLD, &rank);   /* Get id of this process */
+  if (size < 2) {
+    printf("run this program with at least 2 processes \n");
+    MPI_Finalize();
+    exit(0);
+  }
+
+  if (rank == 0) {
+    printf("MPI_ISend / MPI_IRecv Test \n");
+
+    for(i=0; i < size - 1; i++){
+      MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
+      printf("Message received from %d\n", recv_buff);
+      MPI_Send(&recv_buff, 1, MPI_INT, status.MPI_SOURCE, 42, MPI_COMM_WORLD);
+      // printf("Sent %d to rank %d\n", status.MPI_SOURCE);
+    }
+
+  }else{
+    MPI_Send(&rank, 1, MPI_INT, 0, 42, MPI_COMM_WORLD);
+    printf("Sent %d to rank 0\n", rank);
+    MPI_Recv(&recv_buff, 1, MPI_INT, 0, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
+    printf("Message received from %d\n", recv_buff);
+  }
+
+  MPI_Finalize();
+
+  return 0;
+}
diff --git a/examples/smpi/mc/send_deterministic.c b/examples/smpi/mc/send_deterministic.c
new file mode 100644
index 0000000000..ecbcc49426
--- /dev/null
+++ b/examples/smpi/mc/send_deterministic.c
@@ -0,0 +1,50 @@
+/* ../../../smpi_script/bin/smpirun -hostfile hostfile_send_deterministic -platform ../../platforms/cluster.xml -np 3 --cfg=model-check:1 --cfg=smpi/send_is_detached_thres:0 gdb\ --args\ ./send_deterministic */
+
+/* Copyright (c) 2009 - 2014. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* 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. */
+
+#include <stdio.h>
+#include <mpi.h>
+#include <simgrid/modelchecker.h>
+
+
+int main(int argc, char **argv)
+{
+  int recv_buff, err, size, rank, i;
+  MPI_Status status;
+
+  /* Initialize MPI */
+  err = MPI_Init(&argc, &argv);
+  if (err != MPI_SUCCESS) {
+    printf("MPI initialization failed!\n");
+    exit(1);
+  }
+
+  err = MPI_Comm_size(MPI_COMM_WORLD, &size);   /* Get nr of tasks */
+  err = MPI_Comm_rank(MPI_COMM_WORLD, &rank);   /* Get id of this process */
+  if (size < 2) {
+    printf("run this program with at least 2 processes \n");
+    MPI_Finalize();
+    exit(0);
+  }
+
+  if (rank == 0) {
+    printf("MPI_ISend / MPI_IRecv Test \n");
+
+    for(i=0; i < size - 1; i++){
+      MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
+      printf("Message received from %d\n", recv_buff);
+    }
+
+  }else{
+    MPI_Send(&rank, 1, MPI_INT, 0, 42, MPI_COMM_WORLD);
+    printf("Sent %d to rank 0\n", rank);
+  }
+
+  MPI_Finalize();
+
+  return 0;
+}
diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h
index 9cdea6cc82..2c4f48d47f 100644
--- a/src/include/mc/datatypes.h
+++ b/src/include/mc/datatypes.h
@@ -60,7 +60,7 @@ struct s_dw_type{
   int byte_size; /* Size in bytes */
   int element_count; /* Number of elements for array type */
   char *dw_type_id; /* DW_AT_type */
-  xbt_dynar_t members; /* if DW_TAG_structure_type, DW_TAG_union_type*/
+  xbt_dynar_t members; /* if DW_TAG_structure_type, DW_TAG_class_type, DW_TAG_union_type*/
   int is_pointer_type;
   int offset;
   dw_type_t subtype;
diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index d00a13d580..21d00c1a70 100644
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -31,6 +31,7 @@ extern int _sg_mc_max_depth;
 extern int _sg_mc_visited;
 extern char* _sg_mc_dot_output_file;
 extern int _sg_mc_comms_determinism;
+extern int _sg_mc_send_determinism;
 
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
@@ -47,6 +48,7 @@ void _mc_cfg_cb_max_depth(const char *name, int pos);
 void _mc_cfg_cb_visited(const char *name, int pos);
 void _mc_cfg_cb_dot_output(const char *name, int pos);
 void _mc_cfg_cb_comms_determinism(const char *name, int pos);
+void _mc_cfg_cb_send_determinism(const char *name, int pos);
 
 XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
 
diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index d534d891d7..3e1f4cb203 100644
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -236,6 +236,14 @@ void MC_find_object_address(memory_map_t maps, mc_object_info_t result) {
 /************************************* Take Snapshot ************************************/
 /****************************************************************************************/
 
+static bool mc_valid_variable(dw_variable_t var, dw_frame_t frame, const void* ip) {
+  // The variable is not yet valid:
+  if((const void*)((const char*) frame->low_pc + var->start_scope) > ip)
+    return false;
+  else
+    return true;
+}
+
 static xbt_dynar_t MC_get_local_variables_values(xbt_dynar_t stack_frames){
 
   unsigned cursor1 = 0;
@@ -248,6 +256,9 @@ static xbt_dynar_t MC_get_local_variables_values(xbt_dynar_t stack_frames){
     dw_variable_t current_variable;
     xbt_dynar_foreach(stack_frame->frame->variables, cursor2, current_variable){
       
+      if(!mc_valid_variable(current_variable, stack_frame->frame, (void*) stack_frame->ip))
+        continue;
+
       int region_type;
       if((long)stack_frame->ip > (long)mc_libsimgrid_info->start_exec)
         region_type = 1;
diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 5352c52c62..3b0cd331d0 100644
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -123,7 +123,10 @@ static int compare_areas_with_type(void *area1, void *area2, mc_object_info_t in
     case DW_TAG_base_type:
     case DW_TAG_enumeration_type:
     case DW_TAG_pointer_type:
+    case DW_TAG_reference_type:
+    case DW_TAG_rvalue_reference_type:
     case DW_TAG_structure_type:
+    case DW_TAG_class_type:
     case DW_TAG_union_type:
       if(subtype->byte_size == 0){ /*declaration of the type, need the complete description */
           subtype = subtype->other_object_same_type;
@@ -155,6 +158,8 @@ static int compare_areas_with_type(void *area1, void *area2, mc_object_info_t in
     }
     break;
   case DW_TAG_pointer_type:
+  case DW_TAG_reference_type:
+  case DW_TAG_rvalue_reference_type:
     if(type->subtype && type->subtype->type == DW_TAG_subroutine_type){
       addr_pointed1 = *((void **)(area1)); 
       addr_pointed2 = *((void **)(area2));
@@ -198,6 +203,7 @@ static int compare_areas_with_type(void *area1, void *area2, mc_object_info_t in
     }
     break;
   case DW_TAG_structure_type:
+  case DW_TAG_class_type:
     xbt_dynar_foreach(type->members, cursor, member){
       XBT_DEBUG("Compare member %s", member->name);
       res = compare_areas_with_type((char *)area1 + member->offset, (char *)area2 + member->offset, info, other_info, member->subtype, region_size, region_type, start_data, pointer_level);
@@ -220,7 +226,6 @@ static int compare_global_variables(int region_type, mc_mem_region_t r1, mc_mem_
 
   if(!compared_pointers){
     compared_pointers = xbt_dynar_new(sizeof(pointers_pair_t), pointers_pair_free_voidp);
-    MC_ignore_global_variable("compared_pointers");
   }else{
     xbt_dynar_reset(compared_pointers);
   }
@@ -282,7 +287,6 @@ static int compare_local_variables(mc_snapshot_stack_t stack1, mc_snapshot_stack
 
   if(!compared_pointers){
     compared_pointers = xbt_dynar_new(sizeof(pointers_pair_t), pointers_pair_free_voidp);
-    MC_ignore_global_variable("compared_pointers");
   }else{
     xbt_dynar_reset(compared_pointers);
   }
@@ -620,8 +624,7 @@ int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall,
 }
 
 int MC_compare_snapshots(void *s1, void *s2){
-  
-  MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
+
   return simcall_mc_compare_snapshots(s1, s2);
 
 }
diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 1d102d3d90..5ab8aed15e 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -92,7 +92,6 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte
     recv_index = 0;
     current_process++;
   }
-  // XBT_DEBUG("Communication-deterministic : %d, Send-deterministic : %d", initial_state_safety->comm_deterministic, initial_state_safety->send_deterministic);
 }
 
 static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
@@ -102,7 +101,9 @@ static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
     if(current_pattern->comm == pattern->comm){
       if(!current_pattern->completed){
         current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
+        current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host);
         current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
+        current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
         current_pattern->data_size = pattern->comm->comm.src_buff_size;
         current_pattern->data = xbt_malloc0(current_pattern->data_size);
         current_pattern->matched_comm = pattern->num;
@@ -123,13 +124,14 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
   if(call == 1){ // ISEND
     pattern->comm = simcall_comm_isend__get__result(request);
     pattern->type = SIMIX_COMM_SEND;
-    if(pattern->comm->comm.dst_proc != NULL){
- 
+    if(pattern->comm->comm.dst_proc != NULL){ 
       pattern->matched_comm = complete_comm_pattern(list, pattern);
       pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
       pattern->completed = 1;
+      pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
     }
     pattern->src_proc = pattern->comm->comm.src_proc->pid;
+    pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
     pattern->data_size = pattern->comm->comm.src_buff_size;
     pattern->data=xbt_malloc0(pattern->data_size);
     memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
@@ -139,12 +141,14 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
     if(pattern->comm->comm.src_proc != NULL){
       pattern->matched_comm = complete_comm_pattern(list, pattern);
       pattern->src_proc = pattern->comm->comm.src_proc->pid;
+      pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host);
       pattern->completed = 1;
       pattern->data_size = pattern->comm->comm.src_buff_size;
       pattern->data=xbt_malloc0(pattern->data_size);
       memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
     }
     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
+    pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
   }
   if(pattern->comm->comm.rdv != NULL)
     pattern->rdv = strdup(pattern->comm->comm.rdv->name);
@@ -157,7 +161,10 @@ static void print_communications_pattern(xbt_dynar_t comms_pattern){
   unsigned int cursor = 0;
   mc_comm_pattern_t current_comm;
   xbt_dynar_foreach(comms_pattern, cursor, current_comm){
-    // fprintf(stderr, "%s (%d - comm %p, src : %lu, dst %lu, rdv name %s, data %p, matched with %d)\n", current_comm->type == SIMIX_COMM_SEND ? "iSend" : "iRecv", current_comm->num, current_comm->comm, current_comm->src_proc, current_comm->dst_proc, current_comm->rdv, current_comm->data, current_comm->matched_comm);
+    if(current_comm->type == SIMIX_COMM_SEND)
+      XBT_INFO("[(%lu) %s -> %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_host, "iSend");
+    else
+      XBT_INFO("[(%lu) %s <- %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_host, "iRecv");
   }
 }
 
@@ -207,6 +214,8 @@ static mc_visited_state_t visited_state_new(){
  *  The subrange is the subrange of "equivalence" of the given state.
  */
 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
+  XBT_VERB("Searching interval for state %i: nd_processes=%zu heap_bytes_used=%zu",
+    state->num, (size_t)state->nb_processes, (size_t)state->heap_bytes_used);
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
@@ -517,7 +526,7 @@ void MC_dpor(void)
       xbt_free(key);
       MC_UNSET_RAW_MEM;
       
-      if(_sg_mc_comms_determinism){
+      if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
         if(req->call == SIMCALL_COMM_ISEND)
           comm_pattern = 1;
         else if(req->call == SIMCALL_COMM_IRECV)
@@ -527,7 +536,7 @@ void MC_dpor(void)
       /* Answer the request */
       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 
-      if(_sg_mc_comms_determinism){
+      if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
         MC_SET_RAW_MEM;
         if(comm_pattern != 0){
           if(!initial_state_safety->initial_communications_pattern_done)
@@ -632,16 +641,36 @@ void MC_dpor(void)
 
       MC_SET_RAW_MEM;
 
-      if(_sg_mc_comms_determinism){
-        if(!initial_state_safety->initial_communications_pattern_done){
-          //print_communications_pattern(initial_communications_pattern);
-        }else{
+      if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+        if(initial_state_safety->initial_communications_pattern_done){
           if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
             //print_communications_pattern(communications_pattern);
             deterministic_pattern(initial_communications_pattern, communications_pattern);
+            if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
+              XBT_INFO("****************************************************");
+              XBT_INFO("***** Non-deterministic communications pattern *****");
+              XBT_INFO("****************************************************");
+              XBT_INFO("Initial communications pattern:");
+              print_communications_pattern(initial_communications_pattern);
+              XBT_INFO("Communications pattern counter-example:");
+              print_communications_pattern(communications_pattern);
+              MC_print_statistics(mc_stats);
+              return;
+            }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
+              XBT_INFO("****************************************************");
+              XBT_INFO("***** Non-send-deterministic communications pattern *****");
+              XBT_INFO("****************************************************");
+              XBT_INFO("Initial communications pattern:");
+              print_communications_pattern(initial_communications_pattern);
+              XBT_INFO("Communications pattern counter-example:");
+              print_communications_pattern(communications_pattern);
+              MC_print_statistics(mc_stats);
+              return;
+            }
           }
+        }else{
+          initial_state_safety->initial_communications_pattern_done = 1;
         }
-        initial_state_safety->initial_communications_pattern_done = 1;
       }
 
       /* Trash the current state, no longer needed */
diff --git a/src/mc/mc_dwarf.c b/src/mc/mc_dwarf.c
index 3107c9d7ba..c4c00ba078 100644
--- a/src/mc/mc_dwarf.c
+++ b/src/mc/mc_dwarf.c
@@ -50,11 +50,11 @@ static uint64_t MC_dwarf_array_element_count(Dwarf_Die* die, Dwarf_Die* unit);
  *  \param unit the DIE of the compile unit of the current DIE
  *  \param frame containg frame if any
  */
-static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame);
+static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace);
 
 /** \brief Process a type DIE
  */
-static void MC_dwarf_handle_type_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit);
+static void MC_dwarf_handle_type_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace);
 
 /** \brief Calls MC_dwarf_handle_die on all childrend of the given die
  *
@@ -63,7 +63,7 @@ static void MC_dwarf_handle_type_die(mc_object_info_t info, Dwarf_Die* die, Dwar
  *  \param unit the DIE of the compile unit of the current DIE
  *  \param frame containg frame if any
  */
-static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame);
+static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace);
 
 /** \brief Handle a variable (DW_TAG_variable or other)
  *
@@ -72,7 +72,7 @@ static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die* die, Dwar
  *  \param unit the DIE of the compile unit of the current DIE
  *  \param frame containg frame if any
  */
-static void MC_dwarf_handle_variable_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame);
+static void MC_dwarf_handle_variable_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace);
 
 /** \brief Convert a libdw DWARF expression into a MC representation of the location
  *
@@ -98,7 +98,7 @@ const char* MC_dwarf_attrname(int attr) {
   switch (attr) {
 #include "mc_dwarf_attrnames.h"
   default:
-    return "DW_AT_unkown";
+    return "DW_AT_unknown";
   }
 }
 
@@ -113,7 +113,68 @@ const char* MC_dwarf_tagname(int tag) {
   case DW_TAG_invalid:
     return "DW_TAG_invalid";
   default:
-    return "DW_TAG_unkown";
+    return "DW_TAG_unknown";
+  }
+}
+
+/** \brief A class of DWARF tags (DW_TAG_*)
+ */
+typedef enum mc_tag_class {
+  mc_tag_unknown,
+  mc_tag_type,
+  mc_tag_subprogram,
+  mc_tag_variable,
+  mc_tag_scope,
+  mc_tag_namespace
+} mc_tag_class;
+
+static mc_tag_class MC_dwarf_tag_classify(int tag) {
+  switch (tag) {
+
+    case DW_TAG_array_type:
+    case DW_TAG_class_type:
+    case DW_TAG_enumeration_type:
+    case DW_TAG_typedef:
+    case DW_TAG_pointer_type:
+    case DW_TAG_reference_type:
+    case DW_TAG_rvalue_reference_type:
+    case DW_TAG_string_type:
+    case DW_TAG_structure_type:
+    case DW_TAG_subroutine_type:
+    case DW_TAG_union_type:
+    case DW_TAG_ptr_to_member_type:
+    case DW_TAG_set_type:
+    case DW_TAG_subrange_type:
+    case DW_TAG_base_type:
+    case DW_TAG_const_type:
+    case DW_TAG_file_type:
+    case DW_TAG_packed_type:
+    case DW_TAG_volatile_type:
+    case DW_TAG_restrict_type:
+    case DW_TAG_interface_type:
+    case DW_TAG_unspecified_type:
+    case DW_TAG_mutable_type:
+    case DW_TAG_shared_type:
+      return mc_tag_type;
+
+    case DW_TAG_subprogram:
+      return mc_tag_subprogram;
+
+    case DW_TAG_variable:
+    case DW_TAG_formal_parameter:
+      return mc_tag_variable;
+
+    case DW_TAG_lexical_block:
+    case DW_TAG_try_block:
+    case DW_TAG_inlined_subroutine:
+      return mc_tag_scope;
+
+    case DW_TAG_namespace:
+      return mc_tag_namespace;
+
+    default:
+      return mc_tag_unknown;
+
   }
 }
 
@@ -139,6 +200,7 @@ static int MC_dwarf_form_get_class(int form) {
   case DW_FORM_block:
   case DW_FORM_block1:
     return MC_DW_CLASS_BLOCK;
+  case DW_FORM_data1:
   case DW_FORM_data2:
   case DW_FORM_data4:
   case DW_FORM_data8:
@@ -301,6 +363,7 @@ static dw_location_t MC_dwarf_get_location(mc_object_info_t info, Dwarf_Die* die
 
   // The attribute is a reference to a location list entry:
   case DW_FORM_sec_offset:
+  case DW_FORM_data1:
   case DW_FORM_data2:
   case DW_FORM_data4:
   case DW_FORM_data8:
@@ -506,7 +569,8 @@ static void MC_dwarf_fill_member_location(dw_type_t type, dw_type_t member, Dwar
 
   Dwarf_Attribute attr;
   dwarf_attr_integrate(child, DW_AT_data_member_location, &attr);
-  int klass = MC_dwarf_form_get_class(dwarf_whatform(&attr));
+  int form  = dwarf_whatform(&attr);
+  int klass = MC_dwarf_form_get_class(form);
   switch (klass) {
   case MC_DW_CLASS_EXPRLOC:
   case MC_DW_CLASS_BLOCK:
@@ -546,7 +610,9 @@ static void MC_dwarf_fill_member_location(dw_type_t type, dw_type_t member, Dwar
     // It's supposed to be possible in DWARF2 but I couldn't find its semantic
     // in the spec.
   default:
-    xbt_die("Can't handle form class 0x%x (%i) as DW_AT_member_location", klass, klass);
+    xbt_die(
+      "Can't handle form class (%i) / form 0x%x as DW_AT_member_location",
+      klass, form);
   }
 
 }
@@ -558,6 +624,15 @@ static void MC_dwarf_add_members(mc_object_info_t info, Dwarf_Die* die, Dwarf_Di
   type->members = xbt_dynar_new(sizeof(dw_type_t), (void(*)(void*))dw_type_free);
   for (res=dwarf_child(die, &child); res==0; res=dwarf_siblingof(&child,&child)) {
     if (dwarf_tag(&child)==DW_TAG_member) {
+
+      // Skip declarations:
+      if (MC_dwarf_attr_flag(&child, DW_AT_declaration, false))
+        continue;
+
+      // Skip compile time constants:
+      if(dwarf_hasattr(&child, DW_AT_const_value))
+        continue;
+
       // TODO, we should use another type (because is is not a type but a member)
       dw_type_t member = xbt_new0(s_dw_type_t, 1);
       member->type = -1;
@@ -598,7 +673,7 @@ static void MC_dwarf_add_members(mc_object_info_t info, Dwarf_Die* die, Dwarf_Di
  *  \param unit compilation unit of the current DIE
  *  \return MC representation of the type
  */
-static dw_type_t MC_dwarf_die_to_type(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit) {
+static dw_type_t MC_dwarf_die_to_type(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace) {
 
   dw_type_t type = xbt_new0(s_dw_type_t, 1);
   type->type = -1;
@@ -651,13 +726,18 @@ static dw_type_t MC_dwarf_die_to_type(mc_object_info_t info, Dwarf_Die* die, Dwa
   case DW_TAG_union_type:
   case DW_TAG_class_type:
 	  MC_dwarf_add_members(info, die, unit, type);
+	  char* new_namespace = namespace == NULL ? xbt_strdup(type->name)
+	    : bprintf("%s::%s", namespace, type->name);
+	  MC_dwarf_handle_children(info, die, unit, frame, new_namespace);
+	  free(new_namespace);
+	  break;
   }
 
   return type;
 }
 
-static void MC_dwarf_handle_type_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit) {
-  dw_type_t type = MC_dwarf_die_to_type(info, die, unit);
+static void MC_dwarf_handle_type_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace) {
+  dw_type_t type = MC_dwarf_die_to_type(info, die, unit, frame, namespace);
 
   char* key = bprintf("%" PRIx64, (uint64_t) type->id);
   xbt_dict_set(info->types, key, type, NULL);
@@ -828,11 +908,15 @@ static dw_location_t MC_dwarf_get_expression(Dwarf_Op* expr,  size_t len) {
 
 static int mc_anonymous_variable_index = 0;
 
-static dw_variable_t MC_die_to_variable(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame) {
-  // Drop declaration:
+static dw_variable_t MC_die_to_variable(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace) {
+  // Skip declarations:
   if (MC_dwarf_attr_flag(die, DW_AT_declaration, false))
     return NULL;
 
+  // Skip compile time constants:
+  if(dwarf_hasattr(die, DW_AT_const_value))
+    return NULL;
+
   Dwarf_Attribute attr_location;
   if (dwarf_attr(die, DW_AT_location, &attr_location)==NULL) {
     // No location: do not add it ?
@@ -842,7 +926,10 @@ static dw_variable_t MC_die_to_variable(mc_object_info_t info, Dwarf_Die* die, D
   dw_variable_t variable = xbt_new0(s_dw_variable_t, 1);
   variable->dwarf_offset = dwarf_dieoffset(die);
   variable->global = frame == NULL; // Can be override base on DW_AT_location
-  variable->name = xbt_strdup(MC_dwarf_attr_string(die, DW_AT_name));
+
+  const char* name = MC_dwarf_attr_string(die, DW_AT_name);
+  variable->name = xbt_strdup(name);
+
   variable->type_origin = MC_dwarf_at_type(die);
 
   int klass = MC_dwarf_form_get_class(dwarf_whatform(&attr_location));
@@ -881,6 +968,31 @@ static dw_variable_t MC_die_to_variable(mc_object_info_t info, Dwarf_Die* die, D
       klass, klass, (void*) variable->dwarf_offset, variable->name);
   }
 
+  // Handle start_scope:
+  if (dwarf_hasattr(die, DW_AT_start_scope)) {
+    Dwarf_Attribute attr;
+    dwarf_attr(die, DW_AT_start_scope, &attr);
+    int form  = dwarf_whatform(&attr);
+    int klass = MC_dwarf_form_get_class(form);
+    switch(klass) {
+    case MC_DW_CLASS_CONSTANT:
+    {
+      Dwarf_Word value;
+      variable->start_scope = dwarf_formudata(&attr, &value) == 0 ? (size_t) value : 0;
+      break;
+    }
+    default:
+      xbt_die("Unhandled form 0x%x, class 0x%X for DW_AT_start_scope of variable %s",
+        form, klass, name==NULL ? "?" : name);
+    }
+  }
+
+  if(namespace && variable->global) {
+    char* old_name = variable->name;
+    variable->name = bprintf("%s::%s", namespace, old_name);
+    free(old_name);
+  }
+
   // The current code needs a variable name,
   // generate a fake one:
   if(!variable->name) {
@@ -890,22 +1002,20 @@ static dw_variable_t MC_die_to_variable(mc_object_info_t info, Dwarf_Die* die, D
   return variable;
 }
 
-static void MC_dwarf_handle_variable_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame) {
-  dw_variable_t variable = MC_die_to_variable(info, die, unit, frame);
+static void MC_dwarf_handle_variable_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace) {
+  dw_variable_t variable = MC_die_to_variable(info, die, unit, frame, namespace);
   if(variable==NULL)
       return;
   MC_dwarf_register_variable(info, frame, variable);
 }
 
-static void MC_dwarf_handle_subprogram_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t parent_frame) {
+static void MC_dwarf_handle_subprogram_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t parent_frame, const char* namespace) {
   dw_frame_t frame = xbt_new0(s_dw_frame_t, 1);
 
   frame->start = dwarf_dieoffset(die);
 
-  const char* name = MC_dwarf_at_linkage_name(die);
-  if (name==NULL)
-    name = MC_dwarf_attr_string(die, DW_AT_name);
-  frame->name = xbt_strdup(name);
+  const char* name = MC_dwarf_attr_string(die, DW_AT_name);
+  frame->name = namespace ? bprintf("%s::%s", namespace, name) : xbt_strdup(name);
 
   // This is the base address for DWARF addresses.
   // Relocated addresses are offset from this base address.
@@ -919,60 +1029,64 @@ static void MC_dwarf_handle_subprogram_die(mc_object_info_t info, Dwarf_Die* die
   frame->frame_base = MC_dwarf_at_location(info, die, DW_AT_frame_base);
   frame->end = -1; // This one is now useless:
 
+  // Register it:
+  xbt_dynar_push(info->subprograms, &frame);
+
   // Handle children:
-  MC_dwarf_handle_children(info, die, unit, frame);
+  MC_dwarf_handle_children(info, die, unit, frame, namespace);
+}
 
-  // Register it:
-  xbt_dict_set(info->local_variables, frame->name, frame, NULL);
+static void mc_dwarf_handle_namespace_die(
+    mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace) {
+  const char* name = MC_dwarf_attr_string(die, DW_AT_name);
+  if(frame)
+    xbt_die("Unexpected namespace in a subprogram");
+  char* new_namespace = namespace == NULL ? xbt_strdup(name)
+    : bprintf("%s::%s", namespace, name);
+  MC_dwarf_handle_children(info, die, unit, frame, new_namespace);
 }
 
-static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame) {
+static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace) {
   Dwarf_Die child;
   int res;
   for (res=dwarf_child(die, &child); res==0; res=dwarf_siblingof(&child,&child)) {
-    MC_dwarf_handle_die(info, &child, unit, frame);
+    MC_dwarf_handle_die(info, &child, unit, frame, namespace);
   }
 }
 
-static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame) {
+static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame, const char* namespace) {
   int tag = dwarf_tag(die);
-  switch (tag) {
-    case DW_TAG_array_type:
-    case DW_TAG_class_type:
-    case DW_TAG_enumeration_type:
-    case DW_TAG_typedef:
-    case DW_TAG_pointer_type:
-    case DW_TAG_string_type:
-    case DW_TAG_structure_type:
-    case DW_TAG_subroutine_type:
-    case DW_TAG_union_type:
-    case DW_TAG_ptr_to_member_type:
-    case DW_TAG_set_type:
-    case DW_TAG_subrange_type:
-    case DW_TAG_base_type:
-    case DW_TAG_const_type:
-    case DW_TAG_file_type:
-    case DW_TAG_packed_type:
-    case DW_TAG_volatile_type:
-    case DW_TAG_restrict_type:
-    case DW_TAG_interface_type:
-    case DW_TAG_unspecified_type:
-    case DW_TAG_mutable_type:
-    case DW_TAG_shared_type:
-      MC_dwarf_handle_type_die(info, die, unit);
+  mc_tag_class klass = MC_dwarf_tag_classify(tag);
+  switch (klass) {
+
+    // Type:
+    case mc_tag_type:
+      MC_dwarf_handle_type_die(info, die, unit, frame, namespace);
       break;
-    case DW_TAG_subprogram:
-      MC_dwarf_handle_subprogram_die(info, die, unit, frame);
+
+    // Program:
+    case mc_tag_subprogram:
+      MC_dwarf_handle_subprogram_die(info, die, unit, frame, namespace);
       return;
-    // case DW_TAG_formal_parameter:
-    case DW_TAG_variable:
-    case DW_TAG_formal_parameter:
-      MC_dwarf_handle_variable_die(info, die, unit, frame);
+
+    // Variable:
+    case mc_tag_variable:
+      MC_dwarf_handle_variable_die(info, die, unit, frame, namespace);
+      break;
+
+    // Scope:
+    case mc_tag_scope:
+      // TODO
       break;
-  }
 
-  // Recursive processing of children DIE:
-  MC_dwarf_handle_children(info, die, unit, frame);
+    case mc_tag_namespace:
+      mc_dwarf_handle_namespace_die(info, die, unit, frame, namespace);
+      break;
+
+    default:
+      break;
+
+  }
 }
 
 void MC_dwarf_get_variables(mc_object_info_t info) {
@@ -989,18 +1103,14 @@ void MC_dwarf_get_variables(mc_object_info_t info) {
   Dwarf_Off next_offset = 0;
   size_t length;
   while (dwarf_nextcu (dwarf, offset, &next_offset, &length, NULL, NULL, NULL) == 0) {
-    Dwarf_Die die;
+    Dwarf_Die unit_die;
 
-    if(dwarf_offdie(dwarf, offset+length, &die)!=NULL) {
-
-      // Skip C++ for now (we will add support for it soon):
-      int lang = dwarf_srclang(&die);
-      if((lang==DW_LANG_C_plus_plus) || (lang==DW_LANG_ObjC_plus_plus)) {
-        offset = next_offset;
-        continue;
+    if(dwarf_offdie(dwarf, offset+length, &unit_die)!=NULL) {
+      Dwarf_Die child;
+      int res;
+      for (res=dwarf_child(&unit_die, &child); res==0; res=dwarf_siblingof(&child,&child)) {
+        MC_dwarf_handle_die(info, &child, &unit_die, NULL, NULL);
       }
-
-      MC_dwarf_handle_die(info, &die, &die, NULL);
     }
     offset = next_offset;
   }
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 0cda77fb7f..133343e8ee 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -35,6 +35,7 @@ int _sg_mc_max_depth=1000;
 int _sg_mc_visited=0;
 char *_sg_mc_dot_output_file = NULL;
 int _sg_mc_comms_determinism=0;
+int _sg_mc_send_determinism=0;
 
 int user_max_depth_reached = 0;
 
@@ -107,6 +108,13 @@ void _mc_cfg_cb_comms_determinism(const char *name, int pos) {
   _sg_mc_comms_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
+void _mc_cfg_cb_send_determinism(const char *name, int pos) {
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
+    xbt_die("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+  }
+  _sg_mc_send_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name);
+}
+
 /* MC global data structures */
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
@@ -191,17 +199,16 @@ void dw_variable_free_voidp(void *t){
 
 mc_object_info_t MC_new_object_info(void) {
   mc_object_info_t res = xbt_new0(s_mc_object_info_t, 1);
-  res->local_variables = xbt_dict_new_homogeneous(NULL);
+  res->subprograms = xbt_dynar_new(sizeof(dw_frame_t), NULL);
   res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
   res->types = xbt_dict_new_homogeneous(NULL);
   res->types_by_name = xbt_dict_new_homogeneous(NULL);
   return res;
 }
 
-
 void MC_free_object_info(mc_object_info_t* info) {
   xbt_free(&(*info)->file_name);
-  xbt_dict_free(&(*info)->local_variables);
+  xbt_dynar_free(&(*info)->subprograms);
   xbt_dynar_free(&(*info)->global_variables);
   xbt_dict_free(&(*info)->types);
   xbt_dict_free(&(*info)->types_by_name);
@@ -235,9 +242,8 @@ static void MC_make_functions_index(mc_object_info_t info) {
 
   // Populate the array:
   dw_frame_t frame = NULL;
-  xbt_dict_cursor_t cursor = NULL;
-  const char* name = NULL;
-  xbt_dict_foreach(info->local_variables, cursor, name, frame) {
+  unsigned cursor = 0;
+  xbt_dynar_foreach(info->subprograms, cursor, frame) {
     if(frame->low_pc==NULL)
       continue;
     s_mc_function_index_item_t entry;
@@ -307,10 +313,9 @@ static void MC_post_process_variables(mc_object_info_t info) {
 }
 
 static void MC_post_process_functions(mc_object_info_t info) {
-  xbt_dict_cursor_t cursor = NULL;
-  char* key = NULL;
+  unsigned cursor = 0;
   dw_frame_t function = NULL;
-  xbt_dict_foreach(info->local_variables, cursor, key, function) {
+  xbt_dynar_foreach(info->subprograms, cursor, function) {
     unsigned cursor2 = 0;
     dw_variable_t variable = NULL;
     xbt_dynar_foreach(function->variables, cursor2, variable) {
@@ -746,72 +751,50 @@ void MC_ignore_global_variable(const char *name){
     MC_UNSET_RAW_MEM;
 }
 
+static void MC_ignore_local_variable_in_object(const char *var_name, const char *frame_name, mc_object_info_t info) {
+  unsigned cursor2;
+  dw_frame_t frame;
+  int start, end;
+  int cursor = 0;
+  dw_variable_t current_var;
+
+  xbt_dynar_foreach(info->subprograms, cursor2, frame) {
+
+    if(frame_name && strcmp(frame_name, frame->name))
+      continue;
+
+    start = 0;
+    end = xbt_dynar_length(frame->variables) - 1;
+    while(start <= end){
+      cursor = (start + end) / 2;
+      current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
+
+      int compare = strcmp(current_var->name, var_name);
+      if(compare == 0){
+        xbt_dynar_remove_at(frame->variables, cursor, NULL);
+        start = 0;
+        end = xbt_dynar_length(frame->variables) - 1;
+      }else if(compare < 0){
+        start = cursor + 1;
+      }else{
+        end = cursor - 1;
+      }
+    }
+  }
+}
+
 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
   
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
+  if(strcmp(frame_name, "*") == 0)
+    frame_name = NULL;
+
   MC_SET_RAW_MEM;
 
-    unsigned int cursor = 0;
-    dw_variable_t current_var;
-    int start, end;
-    if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames */
-      xbt_dict_cursor_t dict_cursor;
-      char *current_frame_name;
-      dw_frame_t frame;
-      xbt_dict_foreach(mc_libsimgrid_info->local_variables, dict_cursor, current_frame_name, frame){
-        start = 0;
-        end = xbt_dynar_length(frame->variables) - 1;
-        while(start <= end){
-          cursor = (start + end) / 2;
-          current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t); 
-          if(strcmp(current_var->name, var_name) == 0){
-            xbt_dynar_remove_at(frame->variables, cursor, NULL);
-            start = 0;
-            end = xbt_dynar_length(frame->variables) - 1;
-          }else if(strcmp(current_var->name, var_name) < 0){
-            start = cursor + 1;
-          }else{
-            end = cursor - 1;
-          } 
-        }
-      }
-       xbt_dict_foreach(mc_binary_info->local_variables, dict_cursor, current_frame_name, frame){
-        start = 0;
-        end = xbt_dynar_length(frame->variables) - 1;
-        while(start <= end){
-          cursor = (start + end) / 2;
-          current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t); 
-          if(strcmp(current_var->name, var_name) == 0){
-            xbt_dynar_remove_at(frame->variables, cursor, NULL);
-            start = 0;
-            end = xbt_dynar_length(frame->variables) - 1;
-          }else if(strcmp(current_var->name, var_name) < 0){
-            start = cursor + 1;
-          }else{
-            end = cursor - 1;
-          } 
-        }
-      }
-    }else{
-      xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(
-                                      mc_libsimgrid_info->local_variables, frame_name))->variables;
-      start = 0;
-      end = xbt_dynar_length(variables_list) - 1;
-      while(start <= end){
-        cursor = (start + end) / 2;
-        current_var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor, dw_variable_t);
-        if(strcmp(current_var->name, var_name) == 0){
-          xbt_dynar_remove_at(variables_list, cursor, NULL);
-          start = 0;
-          end = xbt_dynar_length(variables_list) - 1;
-        }else if(strcmp(current_var->name, var_name) < 0){
-          start = cursor + 1;
-        }else{
-          end = cursor - 1;
-        } 
-      }
-    } 
+  MC_ignore_local_variable_in_object(var_name, frame_name, mc_libsimgrid_info);
+  if(frame_name!=NULL)
+    MC_ignore_local_variable_in_object(var_name, frame_name, mc_binary_info);
 
   if(!raw_mem_set)
     MC_UNSET_RAW_MEM;
@@ -961,12 +944,14 @@ void MC_init(){
   MC_ignore_local_variable("_throw_ctx", "*");
   MC_ignore_local_variable("ctx", "*");
 
+  MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
   MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
   MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
 
   /* Ignore local variable about time used for tracing */
   MC_ignore_local_variable("start_time", "*"); 
 
+  MC_ignore_global_variable("compared_pointers");
   MC_ignore_global_variable("mc_comp_times");
   MC_ignore_global_variable("mc_snapshot_comparison_time"); 
   MC_ignore_global_variable("mc_time");
@@ -1246,7 +1231,7 @@ void MC_replay(xbt_fifo_t stack, int start)
       xbt_free(key);
     }
   }
-  if(_sg_mc_comms_determinism)
+  if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
     xbt_dynar_reset(communications_pattern);
   MC_UNSET_RAW_MEM;
   
@@ -1278,7 +1263,7 @@ void MC_replay(xbt_fifo_t stack, int start)
       }
     }
 
-    if(_sg_mc_comms_determinism){
+    if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
       if(req->call == SIMCALL_COMM_ISEND)
         comm_pattern = 1;
       else if(req->call == SIMCALL_COMM_IRECV)
@@ -1287,7 +1272,7 @@ void MC_replay(xbt_fifo_t stack, int start)
 
     SIMIX_simcall_pre(req, value);
 
-    if(_sg_mc_comms_determinism){
+    if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
       MC_SET_RAW_MEM;
       if(comm_pattern != 0){
         get_comm_pattern(communications_pattern, req, comm_pattern);
@@ -1576,9 +1561,11 @@ void MC_print_statistics(mc_stats_t stats)
     fprintf(dot_output, "}\n");
     fclose(dot_output);
   }
-  if(initial_state_safety != NULL && _sg_mc_comms_determinism){
-    XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
-    XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
+  if(initial_state_safety != NULL){
+    if(_sg_mc_comms_determinism)
+      XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
+    if (_sg_mc_send_determinism)
+      XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
   }
   MC_UNSET_RAW_MEM;
 }
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 97aff1f9cc..e901815c8c 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -341,7 +341,7 @@ struct s_mc_object_info {
   char *start_exec, *end_exec; // Executable segment
   char *start_rw, *end_rw; // Read-write segment
   char *start_ro, *end_ro; // read-only segment
-  xbt_dict_t local_variables; // xbt_dict_t<frame_name, dw_frame_t>
+  xbt_dynar_t subprograms; // xbt_dynar_t<dw_frame_t>
   xbt_dynar_t global_variables; // xbt_dynar_t<dw_variable_t>
   xbt_dict_t types; // xbt_dict_t<origin as hexadecimal string, dw_type_t>
   xbt_dict_t types_by_name; // xbt_dict_t<name, dw_type_t> (full defined type only)
@@ -443,6 +443,8 @@ typedef struct s_dw_variable{
   dw_location_t location;
   void* address;
 
+  size_t start_scope;
+
 }s_dw_variable_t, *dw_variable_t;
 
 struct s_dw_frame{
@@ -495,6 +497,8 @@ typedef struct s_mc_comm_pattern{
   int completed;
   unsigned long src_proc;
   unsigned long dst_proc;
+  const char *src_host;
+  const char *dst_host;
   char *rdv;
   size_t data_size;
   void *data;
diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 6ffee19348..9fb5ad5cd0 100644
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -279,9 +279,9 @@ char *MC_request_to_string(smx_simcall_t req, int value)
   }
 
   if(args != NULL){
-    str = bprintf("[(%lu)%s (%s)] %s(%s) (%d)", req->issuer->pid , MSG_host_get_name(req->issuer->smx_host), req->issuer->name, type, args, req->call);
+    str = bprintf("[(%lu)%s (%s)] %s(%s)", req->issuer->pid , MSG_host_get_name(req->issuer->smx_host), req->issuer->name, type, args);
   }else{
-    str = bprintf("[(%lu)%s (%s)] %s (%d) ", req->issuer->pid , MSG_host_get_name(req->issuer->smx_host), req->issuer->name, type, req->call);
+    str = bprintf("[(%lu)%s (%s)] %s ", req->issuer->pid , MSG_host_get_name(req->issuer->smx_host), req->issuer->name, type);
   }
 
   xbt_free(args);
diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index 743b4527c0..4ebfb8ee45 100644
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -590,12 +590,18 @@ void sg_config_init(int *argc, char **argv)
                      xbt_cfgelm_string, 0, 1, _mc_cfg_cb_property, NULL);
     xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/property", "");
 
-    /* do determinism model-checking */
-        xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism",
+    /* do communications determinism model-checking */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism",
                      "Enable/disable the detection of determinism in the communications schemes",
                      xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_comms_determinism, NULL);
     xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/communications_determinism", "no");
 
+    /* do send determinism model-checking */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/send_determinism",
+                     "Enable/disable the detection of send-determinism in the communications schemes",
+                     xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_send_determinism, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/send_determinism", "no");
+
     /* Specify the kind of model-checking reduction */
     xbt_cfg_register(&_sg_cfg_set, "model-check/reduction",
                      "Specify the kind of exploration reduction (either none or DPOR)",
diff --git a/src/smpi/smpi_base.c b/src/smpi/smpi_base.c
index b72d6ce9b0..fa4e70dc99 100644
--- a/src/smpi/smpi_base.c
+++ b/src/smpi/smpi_base.c
@@ -765,7 +765,7 @@ void smpi_mpi_wait(MPI_Request * request, MPI_Status * status)
   if ((*request)->action != NULL) { // this is not a detached send
     simcall_comm_wait((*request)->action, -1.0);
 #ifdef HAVE_MC
-  if(MC_is_active())
+  if(MC_is_active() && (*request)->action)
     (*request)->action->comm.dst_data = NULL; // dangling pointer : dst_data is freed with a wait, need to set it to NULL for system state comparison
 #endif
   }
diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c
index bd2923c77c..241568874b 100644
--- a/src/xbt/mmalloc/mm_diff.c
+++ b/src/xbt/mmalloc/mm_diff.c
@@ -812,7 +812,10 @@ static int compare_heap_area_with_type(struct s_mm_diff *state, void *real_area1
     case DW_TAG_base_type:
     case DW_TAG_enumeration_type:
     case DW_TAG_pointer_type:
+    case DW_TAG_reference_type:
+    case DW_TAG_rvalue_reference_type:
     case DW_TAG_structure_type:
+    case DW_TAG_class_type:
     case DW_TAG_union_type:
       if(subtype->byte_size == 0){ /*declaration of the type, need the complete description */
           subtype = xbt_dict_get_or_null(other_info->types_by_name, subtype->name);
@@ -845,6 +848,8 @@ static int compare_heap_area_with_type(struct s_mm_diff *state, void *real_area1
         return res;
     }
     break;
+  case DW_TAG_reference_type:
+  case DW_TAG_rvalue_reference_type:
   case DW_TAG_pointer_type:
     if(type->dw_type_id && ((dw_type_t)xbt_dict_get_or_null(info->types, type->dw_type_id))->type == DW_TAG_subroutine_type){
       addr_pointed1 = *((void **)(area1)); 
@@ -874,6 +879,7 @@ static int compare_heap_area_with_type(struct s_mm_diff *state, void *real_area1
     }
     break;
   case DW_TAG_structure_type:
+  case DW_TAG_class_type:
     if(type->byte_size == 0){ /*declaration of the structure, need the complete description */
       dw_type_t full_type = xbt_dict_get_or_null(info->types_by_name, type->name);
       if(full_type){
@@ -928,6 +934,7 @@ static char* get_offset_type(char* type_id, int offset, mc_object_info_t info, m
   }
   switch(type->type){
   case DW_TAG_structure_type :
+  case DW_TAG_class_type:
     if(type->byte_size == 0){ /*declaration of the structure, need the complete description */
       if(*switch_type == 0){
         dw_type_t full_type = xbt_dict_get_or_null(info->types_by_name, type->name);
@@ -1033,7 +1040,7 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, mc_object_
         type = type->subtype;
       }
     }
-    if((type->byte_size == DW_TAG_pointer_type) || ((type->type == DW_TAG_base_type) && type->name!=NULL && (!strcmp(type->name, "char"))))
+    if((type->type == DW_TAG_pointer_type) || ((type->type == DW_TAG_base_type) && type->name!=NULL && (!strcmp(type->name, "char"))))
       type_size = -1;
     else
       type_size = type->byte_size;