Improve demonitor precision

[aronisstav]

Summary

This change optimizes the races of demonitor variants, but introduces some weirdness in the reported traces.

Fixes #43.

Motivation

Before this PR, Concuerror's handling of races between demonitor variants and a monitored process exiting was 'coarse', in the sense that the call to demonitor would be considered as racing with both the exit event itself (which would determine if a monitor message will be sent) and the 'DOWN'message being delivered (which determined if the message is placed in the mailbox). This would lead to 3 schedulings being explored: monitor is delivered, monitor is emitted but blocked from delivery while in-flight, or monitor is removed before emission. Currently the decision about whether the monitor will be emitted is taken when the process starts exiting.

However, out of four variants of demonitor, only one races with both events (demonitor(..., [info])). In contrast, a call to demonitor(..., [flush]) does not race with either the exit or the deliver events: it is irrelevant whether the process exited before or after, as is irrelevant whether the 'DOWN' message has been delivered or not: the message will never exist in the recipient's mailbox.

All gen_ behavior calls use the following pattern from gen.erl:

Mref = monitor(process, P),
erlang:send(P, Request),
receive
  Reply ->
    demonitor(Mref, [flush]),
    Reply;
  {'DOWN', Mref, _, _, Reason} ->
    exit(Reason)
after
  Timeout ->
    demonitor(Mref, [flush]),
    exit(timeout)
end

For the Reply and after cases Concuerror would explore three schedulings instead of just one.

Change

In order to treat demonitor(..., [flush]) as independent from exit and message delivery, we must ensure that all events appear identical in any of the orderings. This leads to the following changes:

• 'DOWN' messages should be emitted, even if a monitor has been removed before the process exits: Concuerror must be allowed to reschedule independent events in any order it likes, so if demonitor and exit are independent, it must not matter whether they happen in one way or the other. This means that demonitor, exit (maybe emit) should be the same as exit (maybe emit), demonitor so the monitor must always be emitted. Concuerror will also show a warning when emitting DOWN messages for inactive monitors.
• 'DOWN' messages for cancelled monitors can no longer be marked as ignored during scheduling: for the same reason, if demonitor and message delivery are independent, they must be identical in the trace. However, the use_receive_patterns pass can mark such messages as 'received' and not try to reschedule them.

Checklist

• [x] Has tests
• [ ] Updates CHANGELOG (or too minor)
• [x] References related Issues

[codecov[bot]]

Codecov Report

Merging #46 into master will increase coverage by 0.06%. The diff coverage is 99.29%.

@@            Coverage Diff             @@
##           master      #46      +/-   ##
==========================================
+ Coverage   94.39%   94.45%   +0.06%     
==========================================
  Files          12       12              
  Lines        3589     3646      +57     
==========================================
+ Hits         3388     3444      +56     
- Misses        201      202       +1

Flag	Coverage Δ
#tests	94.1% <99.29%> (+0.03%)	:arrow_up:
#tests_real	84.5% <92.25%> (+0.1%)	:arrow_up:
#unit_tests	2.69% <0%> (-0.05%)	:arrow_down:

Impacted Files	Coverage Δ
src/concuerror_scheduler.erl	96.89% <100%> (+0.2%)	:arrow_up:
src/concuerror_dependencies.erl	87.79% <100%> (+0.47%)	:arrow_up:
src/concuerror_io_lib.erl	98.63% <100%> (ø)	:arrow_up:
src/concuerror_callback.erl	92.71% <98.33%> (-0.02%)	:arrow_down:

---

Continue to review full report at Codecov.

Legend - Click here to learn more Δ = absolute <relative> (impact), ø = not affected, ? = missing data Powered by Codecov. Last update c040b0d...5fce895. Read the comment docs.

[aronisstav]

Moving this to parapluu/master.