Merge pull request devinus#15 from devinus/adt-eqc-blocking

Update quickcheck to use blocking/1 and fix uncovered bug
seven1240 · Aug 31, 2012 · c8f3f83 · c8f3f83
2 parents 6294c7d + 3acb457
commit c8f3f83
Show file tree

Hide file tree

Showing 2 changed files with 38 additions and 25 deletions.
diff --git a/src/poolboy.erl b/src/poolboy.erl
@@ -264,7 +264,12 @@ handle_info({'DOWN', Ref, _, _, _}, StateName, State) ->
         [[Pid]] ->
             Sup = State#state.supervisor,
             ok = supervisor:terminate_child(Sup, Pid),
-            {next_state, StateName, State};
+            %% Don't wait for the EXIT message to come in.
+            %% Deal with the worker exit right now to avoid
+            %% a race condition with messages waiting in the
+            %% mailbox.
+            true = ets:delete(State#state.monitors, Pid),
+            handle_worker_exit(Pid, StateName, State);
         [] ->
             {next_state, StateName, State}
     end;

diff --git a/test/poolboy_eqc.erl b/test/poolboy_eqc.erl
@@ -83,7 +83,8 @@ checkin(Pool, {Worker, _}) ->
 
 kill_worker({Worker, _}) ->
     exit(Worker, kill),
-    timer:sleep(1).
+    timer:sleep(1),
+    Worker.
 
 kill_idle_worker(Pool) ->
     Pid = poolboy:checkout(Pool, false),
@@ -115,29 +116,36 @@ precondition(S,{call,_,checkin,[_Pool, Pid]}) ->
 precondition(_S,{call,_,_,_}) ->
     true.
 
-%% XXX comment out for parallel mode XXX
-%dynamic_precondition(S = #state{pid=Pid},_) when Pid /= undefined ->
-    %State = if length(S#state.checked_out) == S#state.size + S#state.max_overflow ->
-            %full;
-        %length(S#state.checked_out) >= S#state.size ->
-            %overflow;
-        %true ->
-            %ready
-    %end,
-
-    %Workers = max(0, S#state.size - length(S#state.checked_out)),
-    %OverFlow = max(0, length(S#state.checked_out) - S#state.size),
-    %Monitors = length(S#state.checked_out),
-
-    %RealStatus = gen_fsm:sync_send_all_state_event(Pid, status),
-    %case RealStatus == {State, Workers, OverFlow, Monitors} of
-        %true ->
-            %true;
-        %_ ->
-            %exit({wrong_state, RealStatus, {State, Workers, OverFlow, Monitors}})
-    %end;
-%dynamic_precondition(_,_) ->
-    %true.
+%% check model state against internal state, only used in sequential tests
+invariant(S = #state{pid=Pid},_) when Pid /= undefined ->
+    State = if length(S#state.checked_out) == S#state.size + S#state.max_overflow ->
+            full;
+        length(S#state.checked_out) >= S#state.size ->
+            overflow;
+        true ->
+            ready
+    end,
+
+    Workers = max(0, S#state.size - length(S#state.checked_out)),
+    OverFlow = max(0, length(S#state.checked_out) - S#state.size),
+    Monitors = length(S#state.checked_out),
+
+    RealStatus = gen_fsm:sync_send_all_state_event(Pid, status),
+    case RealStatus == {State, Workers, OverFlow, Monitors} of
+        true ->
+            true;
+        _ ->
+            {wrong_state, RealStatus, {State, Workers, OverFlow, Monitors}}
+    end;
+invariant(_,_) ->
+    true.
+
+%% what states block
+blocking(S, {call, _, checkout_block, _}) ->
+    %% blocking checkout can block if we expect a checkout to fail
+    not checkout_ok(S);
+blocking(_, _) ->
+    false.
 
 postcondition(S,{call,_,checkout_block,[_Pool]},R) ->
     case R of