Communications should not be canceled when a process stops
Inria Forge bug #15008: https://gforge.inria.fr/tracker/index.php?func=detail&aid=15008&group_id=12&atid=165
From: Lucas Nussbaum
Date: 24/10/2012 19:07
Hi,
The attached archive contains a simple simgrid program (one isend, one irecv). (I provided versions for both m_task_t and msg_task_t). dcomm-tests.tgz
When run, I get this (expected) output:
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] CASE 2
[Ruby:receiver:(1) 1.001560] [msg_test/INFO] THIS POINT IS NEVER REACHED IN MC
[Ruby:receiver:(1) 1.001560] [msg_test/INFO] I'm done. See you!
[Tremblay:sender:(2) 100.000000] [msg_test/INFO] Goodbye now!
[100.000000] [msg_test/INFO] Simulation time 100
My receiver code is:
int receiver(int argc, char *argv[])
{
m_task_t task = NULL;
msg_comm_t res_irecv;
MSG_error_t res;
MSG_process_sleep(1);
res_irecv = MSG_task_irecv(&task, "receiver-0");
if (MSG_comm_test(res_irecv)) {
XBT_INFO("CASE 1");
} else {
XBT_INFO("CASE 2");
res = MSG_comm_wait(res_irecv, 2);
if (res == MSG_OK) {
XBT_INFO("THIS POINT IS NEVER REACHED IN MC");
MC_assert(0);
} else {
XBT_INFO("ERR");
}
}
XBT_INFO("I'm done. See you!");
return 0;
}
And, when running that program with MC enabled, the MC_assert(0) is never reached. Example output with the current git:
$ ./dpeer small_platform.xml deployment_dpeer01.xml --log=mc.thres=DEBUG --cfg=model-check:1
[0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check' to '1'
[0.000000] [mc_global/INFO] Check a safety property
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:27: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:28: [mc_dpor/DEBUG] Initial state
[0.000000] /tmp/simgrid-master/src/mc/mc_checkpoint.c:45: [mc_checkpoint/DEBUG] New region : type : 0, data : 0xa1d7000, size : 3010560
[0.000000] /tmp/simgrid-master/src/mc/mc_checkpoint.c:45: [mc_checkpoint/DEBUG] New region : type : 1, data : 0xa061000, size : 36864
[0.000000] /tmp/simgrid-master/src/mc/mc_checkpoint.c:45: [mc_checkpoint/DEBUG] New region : type : 1, data : 0xa06a000, size : 28672
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:81: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:84: [mc_dpor/DEBUG] Exploration depth=1 (state=0xa1d1000)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:97: [mc_dpor/DEBUG] Execute: [(1)receiver] iRecv (dst=receiver, buff=0x8f94fb8, size=0)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:81: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:84: [mc_dpor/DEBUG] Exploration depth=2 (state=0xa1d1200)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:97: [mc_dpor/DEBUG] Execute: [(1)receiver] Test FALSE (comm=0x8e6c500)
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] CASE 2
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:81: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:84: [mc_dpor/DEBUG] Exploration depth=3 (state=0xa1d1400)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:97: [mc_dpor/DEBUG] Execute: [(1)receiver] WaitTimeout (comm=0x8e6cb00)
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] ERR
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] I'm done. See you!
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:81: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:84: [mc_dpor/DEBUG] Exploration depth=4 (state=0xa1d1600)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:97: [mc_dpor/DEBUG] Execute: [(2)sender] iSend (src=sender, buff=0x8e6ac00, size=8)
[Tremblay:sender:(2) 100.000000] [msg_test/INFO] Goodbye now!
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:81: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:84: [mc_dpor/DEBUG] Exploration depth=5 (state=0xa1d1800)(0 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:139: [mc_dpor/DEBUG] There are no more processes to interleave.
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:165: [mc_dpor/DEBUG] Dependent Transitions:
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:168: [mc_dpor/DEBUG] [(1)receiver] WaitTimeout (comm=0xa060a00) (state=0xa1d1400)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:172: [mc_dpor/DEBUG] [(2)sender] iSend (src=sender, buff=0x8e6ac00, size=8) (state=0xa1d1600)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:212: [mc_dpor/DEBUG] Back-tracking to depth 3
[0.000000] /tmp/simgrid-master/src/mc/mc_global.c:288: [mc_global/DEBUG] **** Begin Replay ****
[0.000000] /tmp/simgrid-master/src/mc/mc_global.c:322: [mc_global/DEBUG] Replay: [(1)receiver] iRecv (dst=receiver, buff=0x8f94fb8, size=0) (0xa1d1000)
[0.000000] /tmp/simgrid-master/src/mc/mc_global.c:322: [mc_global/DEBUG] Replay: [(1)receiver] Test FALSE (comm=0x8e6c500) (0xa1d1200)
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] CASE 2
[0.000000] /tmp/simgrid-master/src/mc/mc_global.c:334: [mc_global/DEBUG] **** End Replay ****
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:81: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:84: [mc_dpor/DEBUG] Exploration depth=3 (state=0xa1d1400)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:97: [mc_dpor/DEBUG] Execute: [(2)sender] iSend (src=sender, buff=0x8e6ac00, size=8)
[Tremblay:sender:(2) 100.000000] [msg_test/INFO] Goodbye now!
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:81: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:84: [mc_dpor/DEBUG] Exploration depth=4 (state=0xa1d1600)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:97: [mc_dpor/DEBUG] Execute: [(1)receiver] WaitTimeout (comm=0x8e6ca00)
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] ERR
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] I'm done. See you!
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:81: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:84: [mc_dpor/DEBUG] Exploration depth=5 (state=0xa1d1800)(0 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:139: [mc_dpor/DEBUG] There are no more processes to interleave.
[0.000000] [mc_global/INFO] Expanded states = 7
[0.000000] [mc_global/INFO] Visited states = 10
[0.000000] [mc_global/INFO] Executed transitions = 8
[0.000000] [mc_global/INFO] Expanded / Visited = 1.428571
[0.000000] [mc_global/INFO] Expanded states = 7
[0.000000] [mc_global/INFO] Visited states = 10
[0.000000] [mc_global/INFO] Executed transitions = 8
[0.000000] [mc_global/INFO] Expanded / Visited = 1.428571
[0.000000] [msg_test/INFO] Simulation time 0
The good thing is, it used to work (in SG 3.6.2, for example):
[0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check' to '1'
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:26: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:27: [mc_dpor/DEBUG] Initial state
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:67: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:70: [mc_dpor/DEBUG] Exploration detph=1 (state=0xa726000)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:83: [mc_dpor/DEBUG] Execute: [(1)receiver] iRecv (dst=receiver, buff=0x93cafb8, size=0)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:67: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:70: [mc_dpor/DEBUG] Exploration detph=2 (state=0xa726c00)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:83: [mc_dpor/DEBUG] Execute: [(1)receiver] Test FALSE (comm=0x94af200)
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] CASE 2
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:67: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:70: [mc_dpor/DEBUG] Exploration detph=3 (state=0xa726e00)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:83: [mc_dpor/DEBUG] Execute: [(1)receiver] WaitTimeout (comm=0x9420ac0)
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] ERR
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] I'm done. See you!
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:67: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:70: [mc_dpor/DEBUG] Exploration detph=4 (state=0xa726a00)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:83: [mc_dpor/DEBUG] Execute: [(2)sender] iSend (src=sender, buff=0x9424480, size=8)
[Tremblay:sender:(2) 100.000000] [msg_test/INFO] Goodbye now!
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:67: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:70: [mc_dpor/DEBUG] Exploration detph=5 (state=0xa726800)(0 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:118: [mc_dpor/DEBUG] There are no more processes to interleave.
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:144: [mc_dpor/DEBUG] Dependent Transitions:
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:147: [mc_dpor/DEBUG] [(1)receiver] WaitTimeout (comm=0xa727f90) (state=0xa726e00)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:151: [mc_dpor/DEBUG] [(2)sender] iSend (src=sender, buff=0x9424480, size=8) (state=0xa726a00)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:166: [mc_dpor/DEBUG] Back-tracking to depth 3
[0.000000] /tmp/simgrid-master/src/mc/mc_global.c:123: [mc_global/DEBUG] **** Begin Replay ****
[0.000000] /tmp/simgrid-master/src/mc/mc_global.c:147: [mc_global/DEBUG] Replay: [(1)receiver] iRecv (dst=receiver, buff=0x93cafb8, size=0) (0xa726000)
[0.000000] /tmp/simgrid-master/src/mc/mc_global.c:147: [mc_global/DEBUG] Replay: [(1)receiver] Test FALSE (comm=0x94af200) (0xa726c00)
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] CASE 2
[0.000000] /tmp/simgrid-master/src/mc/mc_global.c:159: [mc_global/DEBUG] **** End Replay ****
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:67: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:70: [mc_dpor/DEBUG] Exploration detph=3 (state=0xa726e00)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:83: [mc_dpor/DEBUG] Execute: [(2)sender] iSend (src=sender, buff=0x9424480, size=8)
[Tremblay:sender:(2) 100.000000] [msg_test/INFO] Goodbye now!
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:67: [mc_dpor/DEBUG] **************************************************
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:70: [mc_dpor/DEBUG] Exploration detph=4 (state=0xa726600)(1 interleave)
[0.000000] /tmp/simgrid-master/src/mc/mc_dpor.c:83: [mc_dpor/DEBUG] Execute: [(1)receiver] Wait (comm=0x94af200 [(2)sender -> (1)receiver])
[Ruby:receiver:(1) 1.000000] [msg_test/INFO] THIS POINT IS NEVER REACHED IN MC
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] **************************
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] *** PROPERTY NOT VALID ***
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] **************************
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] Counter-example execution trace:
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] [(1)receiver] iRecv (dst=receiver, buff=0x93cafb8, size=0)
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] [(1)receiver] Test FALSE (comm=0xa726c10)
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] [(2)sender] iSend (src=sender, buff=0x9424480, size=8)
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] [(1)receiver] Wait (comm=0xa726610 [(2)sender -> (1)receiver])
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] State space size ~= 1
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] Expanded states = 6
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] Visited states = 9
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] Executed transitions = 8
[Ruby:receiver:(1) 1.000000] [mc_global/INFO] Expanded / Visited = 1.500000
Aborted
According to git bisect, the bug was introduced between ab9642a5 and 0f10bf7b. It's hard to understand which exact commit in that set introduced the problem, though e5922b4d looks like a good candidate.
From: Martin Quinson
Date: 09/11/2012 10:51
Thanks for the report.
Actually, the problem is that the communication of the sender process is canceled when the process stops, and this process stops right after sending the message (since there is no sleep in model checking since there is no time either). As a result, the communication has absolutely no chance of being delivered since it's canceled right after being created.
The right solution seems to not cancel the comms on process stop, as it also causes issues elsewhere.
We see two solutions to implement this:
- refcount the processes and destroy them only when there is no communication involving them. That is to say, ref the process when the comm starts, and unref the process once the comm is done. This solution seems rather cumbersome, difficult to get right, and potentially slow to execute.
- not destroy the comm when the process leaves, but replace it by a sentinel in the communication fields. Imagine that the leaving process is the sender of the comm; then, when it leaves, the src field of the comm is changed to a specific value (such as 0xDEADBEAF ;) that is recognized as such by the process-related functions. That way, we are certain that the other side will never get a segfault while consulting MSG_task_get_source(). You also need to change all functions such as MSG_process_get_name() to deal properly with that sentinel.
Thanks again for the report, Mt.