> [ 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
> [ 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
> [ 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
> [ 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
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)
${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
${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
--- /dev/null
+c-1.me
+c-2.me
+c-3.me
--- /dev/null
+c-1.me
+c-2.me
+c-3.me
--- /dev/null
+/* ../../../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;
+}
--- /dev/null
+/* ../../../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;
+}
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;
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;
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);
/************************************* 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;
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;
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;
}
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));
}
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);
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);
}
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);
}
}
int MC_compare_snapshots(void *s1, void *s2){
-
- MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
+
return simcall_mc_compare_snapshots(s1, s2);
}
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){
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;
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);
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);
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");
}
}
* 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);
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)
/* 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)
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 */
* \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
*
* \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)
*
* \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
*
switch (attr) {
#include "mc_dwarf_attrnames.h"
default:
- return "DW_AT_unkown";
+ return "DW_AT_unknown";
}
}
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;
+
}
}
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:
// 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:
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:
// 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);
}
}
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;
* \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;
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);
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 ?
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));
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) {
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.
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) {
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;
}
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;
_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;
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);
// 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;
}
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) {
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;
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");
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;
}
}
- 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)
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);
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;
}
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)
dw_location_t location;
void* address;
+ size_t start_scope;
+
}s_dw_variable_t, *dw_variable_t;
struct s_dw_frame{
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;
}
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);
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)",
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
}
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);
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));
}
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){
}
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);
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;
