forked from devinus/poolboy
-
Notifications
You must be signed in to change notification settings - Fork 26
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
b6218ae
commit fb8705f
Showing
12 changed files
with
288 additions
and
15 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -3,3 +3,6 @@ | |
.test | ||
.eunit | ||
.dialyzer_plt | ||
_build/* | ||
rebar.lock | ||
.DS_Store |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,262 @@ | ||
-module(poolboy_eqc). | ||
-compile([poolboy_test_]). %%FIXME: Probably needs fix by adding missing functions. | ||
|
||
-ifdef(TEST). | ||
-ifdef(EQC). | ||
-include_lib("eqc/include/eqc.hrl"). | ||
-include_lib("eqc/include/eqc_statem.hrl"). | ||
|
||
-include_lib("eunit/include/eunit.hrl"). | ||
|
||
poolboy_test_() -> | ||
{timeout, 20, | ||
fun() -> | ||
?assert(eqc:quickcheck(eqc:testing_time(4, | ||
poolboy_eqc:prop_sequential()))), | ||
?assert(eqc:quickcheck(eqc:testing_time(4, | ||
poolboy_eqc:prop_parallel()))) | ||
end | ||
}. | ||
|
||
-record(state, | ||
{ | ||
pid, | ||
size, | ||
max_overflow, | ||
checked_out = [] | ||
}). | ||
|
||
initial_state() -> | ||
#state{}. | ||
|
||
command(S) -> | ||
oneof( | ||
[{call, ?MODULE, start_poolboy, make_args(S, nat(), nat())} || S#state.pid == undefined] ++ | ||
[{call, ?MODULE, stop_poolboy, [S#state.pid]} || S#state.pid /= undefined] ++ | ||
[{call, ?MODULE, checkout_nonblock, [S#state.pid]} || S#state.pid /= undefined] ++ | ||
%% checkout shrinks to checkout_nonblock so we can simplify counterexamples | ||
[{call, ?MODULE, ?SHRINK(checkout_block, [checkout_nonblock]), [S#state.pid]} || S#state.pid /= undefined] ++ | ||
[{call, ?MODULE, checkin, [S#state.pid, fault({call, ?MODULE, spawn_process, []}, elements(S#state.checked_out))]} || S#state.pid /= undefined, S#state.checked_out /= []] ++ | ||
[{call, ?MODULE, kill_worker, [elements(S#state.checked_out)]} || S#state.pid /= undefined, S#state.checked_out /= []] ++ | ||
[{call, ?MODULE, kill_idle_worker, [S#state.pid]} || S#state.pid /= undefined] ++ | ||
[{call, ?MODULE, spurious_exit, [S#state.pid]} || S#state.pid /= undefined] | ||
). | ||
|
||
make_args(_S, Size, Overflow) -> | ||
[[{size, Size}, {max_overflow, Overflow}, {worker_module, poolboy_test_worker}, {name, {local, poolboy_eqc}}]]. | ||
|
||
spawn_process() -> | ||
{spawn(fun() -> | ||
timer:sleep(5000) | ||
end), self()}. | ||
|
||
spawn_linked_process(Pool) -> | ||
Parent = self(), | ||
Pid = spawn(fun() -> | ||
link(Pool), | ||
Parent ! {linked, self()}, | ||
timer:sleep(5000) | ||
end), | ||
receive | ||
{linked, Pid} -> | ||
Pid | ||
end. | ||
|
||
start_poolboy(Args) -> | ||
{ok, Pid} = poolboy:start_link(Args), | ||
Pid. | ||
|
||
stop_poolboy(Pid) -> | ||
gen_fsm:sync_send_all_state_event(Pid, stop), | ||
timer:sleep(1). | ||
|
||
checkout_nonblock(Pool) -> | ||
{poolboy:checkout(Pool, false), self()}. | ||
|
||
checkout_block(Pool) -> | ||
{catch(poolboy:checkout(Pool, true, 100)), self()}. | ||
|
||
checkin(Pool, {Worker, _}) -> | ||
Res = poolboy:checkin(Pool, Worker), | ||
gen_fsm:sync_send_all_state_event(Pool, get_avail_workers), | ||
Res. | ||
|
||
kill_worker({Worker, _}) -> | ||
exit(Worker, kill), | ||
timer:sleep(1), | ||
Worker. | ||
|
||
kill_idle_worker(Pool) -> | ||
Pid = poolboy:checkout(Pool, false), | ||
case Pid of | ||
_ when is_pid(Pid) -> | ||
poolboy:checkin(Pool, Pid), | ||
kill_worker({Pid, self()}); | ||
_ -> | ||
timer:sleep(1), | ||
kill_idle_worker(Pool) | ||
end. | ||
|
||
spurious_exit(Pool) -> | ||
Pid = spawn_linked_process(Pool), | ||
exit(Pid, kill). | ||
|
||
precondition(S,{call,_,start_poolboy,_}) -> | ||
%% only start new pool when old one is stopped | ||
S#state.pid == undefined; | ||
precondition(S,_) when S#state.pid == undefined -> | ||
%% all other states need a running pool | ||
false; | ||
precondition(S, {call, _, kill_worker, [Pid]}) -> | ||
lists:member(Pid, S#state.checked_out); | ||
precondition(S,{call,_,kill_idle_worker,[_Pool]}) -> | ||
length(S#state.checked_out) < S#state.size; | ||
precondition(S,{call,_,checkin,[_Pool, Pid]}) -> | ||
lists:member(Pid, S#state.checked_out); | ||
precondition(_S,{call,_,_,_}) -> | ||
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 | ||
{{'EXIT', {timeout, _}}, _} -> | ||
case length(S#state.checked_out) >= S#state.size + S#state.max_overflow of | ||
true -> | ||
true; | ||
_ -> | ||
{checkout_block, R} | ||
end; | ||
_ -> | ||
case length(S#state.checked_out) < S#state.size + S#state.max_overflow of | ||
true -> | ||
true; | ||
_ -> | ||
{checkout_block, R} | ||
end | ||
end; | ||
postcondition(S,{call,_,checkout_nonblock,[_Pool]},R) -> | ||
case R of | ||
{full, _} -> | ||
case length(S#state.checked_out) >= S#state.size + S#state.max_overflow of | ||
true -> | ||
true; | ||
_ -> | ||
{checkout_nonblock, R} | ||
end; | ||
_ -> | ||
case length(S#state.checked_out) < S#state.size + S#state.max_overflow of | ||
true -> | ||
true; | ||
_ -> | ||
{checkout_block, R} | ||
end | ||
end; | ||
postcondition(_S, {call,_,checkin,_}, R) -> | ||
case R of | ||
ok -> | ||
true; | ||
_ -> | ||
{checkin, R} | ||
end; | ||
postcondition(_S,{call,_,_,_},_R) -> | ||
true. | ||
|
||
next_state(S,V,{call,_,start_poolboy, [Args]}) -> | ||
S#state{pid=V, | ||
size=proplists:get_value(size, Args), | ||
max_overflow=proplists:get_value(max_overflow, Args) | ||
}; | ||
next_state(S,_V,{call,_,stop_poolboy, [_Args]}) -> | ||
S#state{pid=undefined, checked_out=[]}; | ||
next_state(S,V,{call,_,checkout_block,_}) -> | ||
%% if the model says the checkout worked, store the result | ||
case checkout_ok(S) of | ||
false -> | ||
S; | ||
_ -> | ||
S#state{checked_out=S#state.checked_out++[V]} | ||
end; | ||
next_state(S,V,{call,_,checkout_nonblock,_}) -> | ||
%% if the model says the checkout worked, store the result | ||
case checkout_ok(S) of | ||
false -> | ||
S; | ||
_ -> | ||
S#state{checked_out=S#state.checked_out++[V]} | ||
end; | ||
next_state(S,_V,{call, _, checkin, [_Pool, Worker]}) -> | ||
S#state{checked_out=S#state.checked_out -- [Worker]}; | ||
next_state(S,_V,{call, _, kill_worker, [Worker]}) -> | ||
S#state{checked_out=S#state.checked_out -- [Worker]}; | ||
next_state(S,_V,{call, _, kill_idle_worker, [_Pool]}) -> | ||
S; | ||
next_state(S,_V,{call, _, spurious_exit, [_Pool]}) -> | ||
S; | ||
next_state(S,V,{call, erlang, self, []}) -> | ||
%% added after test generation, values are never symbolic | ||
S#state{checked_out=[{Worker, Pid} || {Worker, Pid} <- S#state.checked_out, Pid /= V]}. | ||
|
||
|
||
prop_sequential() -> | ||
fault_rate(1, 10, | ||
?FORALL(Cmds,commands(?MODULE), | ||
?TRAPEXIT( | ||
aggregate(command_names(Cmds), | ||
begin | ||
{H,S,Res} = run_commands(?MODULE,Cmds), | ||
catch(stop_poolboy(whereis(poolboy_eqc))), | ||
?WHENFAIL(io:format("History: ~p\nState: ~p\nRes: ~p\n~p\n", | ||
[H,S,Res, zip(Cmds, [Y || {_, Y} <- H])]), | ||
Res == ok) | ||
end)))). | ||
|
||
prop_parallel() -> | ||
fault_rate(1, 10, | ||
?FORALL(Cmds={Seq,Par},parallel_commands(?MODULE), | ||
?TRAPEXIT( | ||
aggregate(command_names(Cmds), | ||
begin | ||
NewPar = [P ++ [{set, {var, 0}, {call, erlang, self, []}}] || P <- Par], | ||
{H,S,Res} = run_parallel_commands(?MODULE,{Seq,NewPar}), | ||
catch(stop_poolboy(whereis(poolboy_eqc))), | ||
?WHENFAIL(io:format("History: ~p\nState: ~p\nRes: ~p\n", | ||
[H,S,Res]), | ||
Res == ok) | ||
end)))). | ||
|
||
|
||
checkout_ok(S) -> | ||
length(S#state.checked_out) < S#state.size + S#state.max_overflow. | ||
|
||
-endif. | ||
-endif. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Binary file not shown.
Binary file not shown.
Binary file not shown.