Fix demonitor(..., [flush]) and unlink/1

[aronisstav]

As per the documentation of demonitor/1, the following program cannot fail:

-module(demonitor_flush).

-export([test/0]).

test() ->
  {Pid, Ref} = spawn_monitor(fun() -> ok end),
  demonitor(Ref, [flush]),
  receive
    {'DOWN', Ref, process, Pid, _} -> error(impossible)
  after
    0 -> ok
  end.

However Concuerror 0.15 reports:

Interleaving #4
--------------------------------------------------------------------------------
Errors found:
* At step 6 process P exited abnormally
    Reason:
      {impossible,[{demonitor_flush,test,0,
                                    [{file,"demonitor_flush.erl"},{line,9}]}]}
    Stacktrace:
      [{demonitor_flush,test,0,[{file,"demonitor_flush.erl"},{line,9}]}]
--------------------------------------------------------------------------------
Event trace:
   1: P: {P.1,#Ref<0.0.1.158>} = erlang:spawn_opt({erlang,apply,[#Fun<demonitor_flush.'-test/0-fun-0-'.0>,[]],[monitor]})
    in erlang.erl line 2647
   2: P.1: exits normally
   3: P: true = erlang:demonitor(#Ref<0.0.1.158>, [flush])
    in demonitor_flush.erl line 7
   4: P.1: {'DOWN',#Ref<0.0.1.158>,process,P.1,normal} = erlang:send(P, {'DOWN',#Ref<0.0.1.158>,process,P.1,normal})
    (while exiting)
   5: P: receives message ({'DOWN',#Ref<0.0.1.158>,process,P.1,normal})
    in demonitor_flush.erl line 8
   6: P: exits abnormally ({impossible,[{demonitor_flush,test,0,[{file,[100,101,109,111,110,105,116,111,114|...]},{line,9}]}]})

This is wrong; after the call to demonitor even a 'flying' future message should be suppressed.

[aronisstav]

Same for unlink/1.

[aronisstav]

Regarding unlink/1:

If a linked process can "start exiting" at the same time that an unlink/1 for that process is performed, then the signal could have been delivered anyway. It may be the case that an unlink happens and "later" the signal reaches, but then the signal could have reached before the unlink but after the process exited.

No special handling there then; if we were to 'cancel' such in-flight unlinks, then they'd race twice: process exiting and signal delivery.

[aronisstav]

This has been fixed a while ago.