Checking whether exit-kill-wait-drain is valid

pdm.erl

%% @doc Figure out whether the kill-then-drain-message pattern is
%% valid and free of races.
-module(pdm).

-compile(export_all).
-compile({parse_transform, pulse_instrument}).
-compile({pulse_skip,[{prop_kill_then_drain,0}]}).

-include_lib("eqc/include/eqc.hrl").
-include_lib("pulse/include/pulse.hrl").

send_msg_start(Ref, Target) ->
    send_msg_loop(Ref, Target, 0).

send_msg_loop(Ref, Target, Count) ->
    Target ! {Ref, Count},
    %% the test hangs without this sleep; fans spin up, machine gets hot
    timer:sleep(1),
    send_msg_loop(Ref, Target, Count+1).

prop_kill_then_drain() ->
    ?PULSE(Late,
           attempt_kill_then_drain(),
           Late == 0).

attempt_kill_then_drain() ->
    %% start a process sending us messages
    Ref = make_ref(),
    Sender = spawn(?MODULE, send_msg_start, [Ref, self()]),

    %% if this line is included, the test passes, but without this
    %% line, the test fails after very few attempts
%    receive {Ref, _} -> ok end,

    %% kill the process
    exit(Sender, kill),

    %% drain what it sent us
    _ = drain(Ref),

    %% try draining again - this one should *always* return 0 because the
    %% previous drain should have caught everything possible
    drain(Ref).

prop_kill_wait_then_drain() ->
    ?PULSE(Late,
           attempt_kill_wait_then_drain(),
           Late == 0).

attempt_kill_wait_then_drain() ->
    %% start a process sending us messages
    Ref = make_ref(),
    Sender = spawn(?MODULE, send_msg_start, [Ref, self()]),

    %% in this version, the following line does not matter - the test
    %% passes both with and without it
%    receive {Ref, _} -> ok end,

    %% kill the process
    exit(Sender, kill),

    %% wait until we're sure it's dead
    wait(Sender),

    %% drain what it sent us
    _ = drain(Ref),

    %% try draining again - this one should *always* return 0 because the
    %% previous drain should have caught everything possible
    drain(Ref).

wait(Sender) ->
    case is_process_alive(Sender) of
        true ->
            timer:sleep(1),
            wait(Sender);
        false ->
            ok
    end.

prop_kill_monitor_then_drain() ->
    ?PULSE(Late,
           attempt_kill_monitor_then_drain(),
           Late == 0).

attempt_kill_monitor_then_drain() ->
    %% start a process sending us messages
    Ref = make_ref(),
    Sender = spawn(?MODULE, send_msg_start, [Ref, self()]),

    %% in this version, the following line does not matter - the test
    %% passes both with and without it
%    receive {Ref, _} -> ok end,

    %% monitor before killing
    Mon = erlang:monitor(process, Sender),

    %% kill the process
    exit(Sender, kill),

    %% wait until we're sure it's dead
    receive {'DOWN', Mon, process, Sender, _Reason} -> ok end,

    %% drain what it sent us
    _ = drain(Ref),

    %% try draining again - this one should *always* return 0 because the
    %% previous drain should have caught everything possible
    drain(Ref).


drain(Ref) ->
    drain(Ref, 0).

drain(Ref, Count) ->
    receive
        {Ref, _} ->
            drain(Ref, Count+1)
    after 0 ->
            Count
    end.