aronisstav
commented
6 years ago Investigating more:
When a process exits while having a monitor the following events happen:
1) process starts exiting 2) a monitor message is sent 3) the monitor message is delivered
Calls to demonitor/1 depend only with event 3 (whether the monitor will be placed in the mailbox upon delivery or not). Other variants of demonitor either have no dependencies at all (demonitor flush), have dependencies with 2 (demonitor info) or also have dependencies only with 3 (demonitor flush info).
However, event 2 can also be completely 'cancelled' by the demonitor. Concuerror, however, cannot handle cases where racing events completely disappear. Even worse, it will completely lose it if events that are not racing, e.g. demonitor/1 and sending (NOT delivering) a monitor message cannot be reordered (e.g. because demonitor eliminated the sending).
A solution could be to always emit monitor messages, even when the monitors have been cancelled (and will be ignored upon delivery) and configure the dependencies accordingly.
It will lead to strange traces though:
41. <P> <Ref> = monitor(process, <P1>)
42. <P> true = demonitor(<Ref>)
43. <P1> exits (normal)
44. <P1> sends {'DOWN', <Ref>, process, <P1>, normal} (while exiting)
45. {'DOWN', <Ref>, process, <P1>, normal} reaches <P> (but will never end up in the mailbox)This will be even worse for flushing variants, because there should be no difference to the event corresponding to the message being delivered before demonitoring and the event of the message being delivered after demonitoring. So the ignored field should be removed and this will lead to more schedulings when use_receive_patterns is false.
Is your feature request related to a problem? Please describe. When one uses
demonitor(Ref, [flush])there are absolutely no races with the exit of the monitored process. When one usesdemonitor(Ref, [])the only race is with the delivered message, not with the exit. The only case where there are races with the exit is withdemonitor(Ref, [info]). Yet another rule exists fordemonitor(Ref, [flush, exit])(races with the delivery of the message).There are plenty of schedulings to be saved if this is redesigned.
Describe the solution you'd like Make races more accurate.
Preliminary work exists in the 1098a133c3a769 branch