Semantics of EXIT message delivery is broken.

[aartamonau]

Describe the bug

The documentation for erlang:unlink/1 function states the following:

Once unlink(Id) has returned, it is guaranteed that the link between the caller and the entity referred to by Id has no effect on the caller in the future (unless the link is setup again). If the caller is trapping exits, an {'EXIT', Id, _} message from the link can have been placed in the caller's message queue before the call.

So if a process A with trap_exit set to true unlinks from a process B and then makes sure to clean up an EXIT message from B that might have been put into the mailbox before the call to unlink, it should be protected from seeing this EXIT message in the future. Concuerror doesn't seem to adhere to this semantics.

To Reproduce

Run Concuerror on the following module:

-module(test).

-compile(export_all).

test() ->
    process_flag(trap_exit, true),
    Pid = spawn_link(fun () ->
                             ok
                     end),
    unlink(Pid),
    receive
        {'EXIT', Pid, _} ->
            ok
    after 0 ->
            ok
    end,

    receive
        {'EXIT', Pid, _} ->
            exit(bad)
    after 0 ->
            ok
    end.

Concuerror reports an error:

Errors found:
* At step 8 process <P> exited abnormally
    Reason:
      bad
    Stacktrace:
      [{test,test,0,[{file,"/tmp/test.erl"},{line,21}]}]
--------------------------------------------------------------------------------
Event trace:
   1: <P>: false = erlang:process_flag(trap_exit, true)
    in test.erl line 6
   2: <P>: <P.1> = erlang:spawn_link(erlang, apply, [#Fun<test.'-test/0-fun-0-'.0>,[]])
    in erlang.erl line 2708
   3: <P.1>: exits normally
   4: <P>: true = erlang:unlink(<P.1>)
    in test.erl line 10
   5: <P>: receive timeout expires after 0 ms
    in test.erl line 11
   6: <P.1>: true = erlang:exit(<P>, normal)
    (while exiting)
   7: <P>: receives message ({'EXIT',<P.1>,normal})
    in test.erl line 19
   8: <P>: exits abnormally (bad)

Expected behavior

According to my reading of erlang:unlink/1 documentation this code is fine and no error should be reported.

[aronisstav]

This seems indeed to be a bug. I mistakenly thought that this was not a valid issue when I closed #102, but the justification given there is wrong.

Thank you very much for the report and the test!