| 6 |
7u83 |
1 |
-module(poolboy_eqc).
|
|
|
2 |
-compile([export_all, nowarn_export_all]).
|
|
|
3 |
|
|
|
4 |
-ifdef(TEST).
|
|
|
5 |
-ifdef(EQC).
|
|
|
6 |
-include_lib("eqc/include/eqc.hrl").
|
|
|
7 |
-include_lib("eqc/include/eqc_statem.hrl").
|
|
|
8 |
|
|
|
9 |
-include_lib("eunit/include/eunit.hrl").
|
|
|
10 |
|
|
|
11 |
poolboy_test_() ->
|
|
|
12 |
{timeout, 20,
|
|
|
13 |
fun() ->
|
|
|
14 |
?assert(eqc:quickcheck(eqc:testing_time(4,
|
|
|
15 |
poolboy_eqc:prop_sequential()))),
|
|
|
16 |
?assert(eqc:quickcheck(eqc:testing_time(4,
|
|
|
17 |
poolboy_eqc:prop_parallel())))
|
|
|
18 |
end
|
|
|
19 |
}.
|
|
|
20 |
|
|
|
21 |
-record(state,
|
|
|
22 |
{
|
|
|
23 |
pid,
|
|
|
24 |
size,
|
|
|
25 |
max_overflow,
|
|
|
26 |
checked_out = []
|
|
|
27 |
}).
|
|
|
28 |
|
|
|
29 |
initial_state() ->
|
|
|
30 |
#state{}.
|
|
|
31 |
|
|
|
32 |
command(S) ->
|
|
|
33 |
oneof(
|
|
|
34 |
[{call, ?MODULE, start_poolboy, make_args(S, nat(), nat())} || S#state.pid == undefined] ++
|
|
|
35 |
[{call, ?MODULE, stop_poolboy, [S#state.pid]} || S#state.pid /= undefined] ++
|
|
|
36 |
[{call, ?MODULE, checkout_nonblock, [S#state.pid]} || S#state.pid /= undefined] ++
|
|
|
37 |
%% checkout shrinks to checkout_nonblock so we can simplify counterexamples
|
|
|
38 |
[{call, ?MODULE, ?SHRINK(checkout_block, [checkout_nonblock]), [S#state.pid]} || S#state.pid /= undefined] ++
|
|
|
39 |
[{call, ?MODULE, checkin, [S#state.pid, fault({call, ?MODULE, spawn_process, []}, elements(S#state.checked_out))]} || S#state.pid /= undefined, S#state.checked_out /= []] ++
|
|
|
40 |
[{call, ?MODULE, kill_worker, [elements(S#state.checked_out)]} || S#state.pid /= undefined, S#state.checked_out /= []] ++
|
|
|
41 |
[{call, ?MODULE, kill_idle_worker, [S#state.pid]} || S#state.pid /= undefined] ++
|
|
|
42 |
[{call, ?MODULE, spurious_exit, [S#state.pid]} || S#state.pid /= undefined]
|
|
|
43 |
).
|
|
|
44 |
|
|
|
45 |
make_args(_S, Size, Overflow) ->
|
|
|
46 |
[[{size, Size}, {max_overflow, Overflow}, {worker_module, poolboy_test_worker}, {name, {local, poolboy_eqc}}]].
|
|
|
47 |
|
|
|
48 |
spawn_process() ->
|
|
|
49 |
{spawn(fun() ->
|
|
|
50 |
timer:sleep(5000)
|
|
|
51 |
end), self()}.
|
|
|
52 |
|
|
|
53 |
spawn_linked_process(Pool) ->
|
|
|
54 |
Parent = self(),
|
|
|
55 |
Pid = spawn(fun() ->
|
|
|
56 |
link(Pool),
|
|
|
57 |
Parent ! {linked, self()},
|
|
|
58 |
timer:sleep(5000)
|
|
|
59 |
end),
|
|
|
60 |
receive
|
|
|
61 |
{linked, Pid} ->
|
|
|
62 |
Pid
|
|
|
63 |
end.
|
|
|
64 |
|
|
|
65 |
start_poolboy(Args) ->
|
|
|
66 |
{ok, Pid} = poolboy:start_link(Args),
|
|
|
67 |
Pid.
|
|
|
68 |
|
|
|
69 |
stop_poolboy(Pid) ->
|
|
|
70 |
gen_server:call(Pid, stop),
|
|
|
71 |
timer:sleep(1).
|
|
|
72 |
|
|
|
73 |
checkout_nonblock(Pool) ->
|
|
|
74 |
{poolboy:checkout(Pool, false), self()}.
|
|
|
75 |
|
|
|
76 |
checkout_block(Pool) ->
|
|
|
77 |
{catch(poolboy:checkout(Pool, true, 100)), self()}.
|
|
|
78 |
|
|
|
79 |
checkin(Pool, {Worker, _}) ->
|
|
|
80 |
Res = poolboy:checkin(Pool, Worker),
|
|
|
81 |
gen_server:call(Pool, get_avail_workers),
|
|
|
82 |
Res.
|
|
|
83 |
|
|
|
84 |
kill_worker({Worker, _}) ->
|
|
|
85 |
exit(Worker, kill),
|
|
|
86 |
timer:sleep(1),
|
|
|
87 |
Worker.
|
|
|
88 |
|
|
|
89 |
kill_idle_worker(Pool) ->
|
|
|
90 |
Pid = poolboy:checkout(Pool, false),
|
|
|
91 |
case Pid of
|
|
|
92 |
_ when is_pid(Pid) ->
|
|
|
93 |
poolboy:checkin(Pool, Pid),
|
|
|
94 |
kill_worker({Pid, self()});
|
|
|
95 |
_ ->
|
|
|
96 |
timer:sleep(1),
|
|
|
97 |
kill_idle_worker(Pool)
|
|
|
98 |
end.
|
|
|
99 |
|
|
|
100 |
spurious_exit(Pool) ->
|
|
|
101 |
Pid = spawn_linked_process(Pool),
|
|
|
102 |
exit(Pid, kill).
|
|
|
103 |
|
|
|
104 |
precondition(S,{call,_,start_poolboy,_}) ->
|
|
|
105 |
%% only start new pool when old one is stopped
|
|
|
106 |
S#state.pid == undefined;
|
|
|
107 |
precondition(S,_) when S#state.pid == undefined ->
|
|
|
108 |
%% all other states need a running pool
|
|
|
109 |
false;
|
|
|
110 |
precondition(S, {call, _, kill_worker, [Pid]}) ->
|
|
|
111 |
lists:member(Pid, S#state.checked_out);
|
|
|
112 |
precondition(S,{call,_,kill_idle_worker,[_Pool]}) ->
|
|
|
113 |
length(S#state.checked_out) < S#state.size;
|
|
|
114 |
precondition(S,{call,_,checkin,[_Pool, Pid]}) ->
|
|
|
115 |
lists:member(Pid, S#state.checked_out);
|
|
|
116 |
precondition(_S,{call,_,_,_}) ->
|
|
|
117 |
true.
|
|
|
118 |
|
|
|
119 |
%% check model state against internal state, only used in sequential tests
|
|
|
120 |
invariant(S = #state{pid=Pid},_) when Pid /= undefined ->
|
|
|
121 |
State = if length(S#state.checked_out) == S#state.size + S#state.max_overflow ->
|
|
|
122 |
full;
|
|
|
123 |
length(S#state.checked_out) >= S#state.size ->
|
|
|
124 |
overflow;
|
|
|
125 |
true ->
|
|
|
126 |
ready
|
|
|
127 |
end,
|
|
|
128 |
|
|
|
129 |
Workers = max(0, S#state.size - length(S#state.checked_out)),
|
|
|
130 |
OverFlow = max(0, length(S#state.checked_out) - S#state.size),
|
|
|
131 |
Monitors = length(S#state.checked_out),
|
|
|
132 |
|
|
|
133 |
RealStatus = gen_server:call(Pid, status),
|
|
|
134 |
case RealStatus == {State, Workers, OverFlow, Monitors} of
|
|
|
135 |
true ->
|
|
|
136 |
true;
|
|
|
137 |
_ ->
|
|
|
138 |
{wrong_state, RealStatus, {State, Workers, OverFlow, Monitors}}
|
|
|
139 |
end;
|
|
|
140 |
invariant(_,_) ->
|
|
|
141 |
true.
|
|
|
142 |
|
|
|
143 |
%% what states block
|
|
|
144 |
blocking(S, {call, _, checkout_block, _}) ->
|
|
|
145 |
%% blocking checkout can block if we expect a checkout to fail
|
|
|
146 |
not checkout_ok(S);
|
|
|
147 |
blocking(_, _) ->
|
|
|
148 |
false.
|
|
|
149 |
|
|
|
150 |
postcondition(S,{call,_,checkout_block,[_Pool]},R) ->
|
|
|
151 |
case R of
|
|
|
152 |
{{'EXIT', {timeout, _}}, _} ->
|
|
|
153 |
case length(S#state.checked_out) >= S#state.size + S#state.max_overflow of
|
|
|
154 |
true ->
|
|
|
155 |
true;
|
|
|
156 |
_ ->
|
|
|
157 |
{checkout_block, R}
|
|
|
158 |
end;
|
|
|
159 |
_ ->
|
|
|
160 |
case length(S#state.checked_out) < S#state.size + S#state.max_overflow of
|
|
|
161 |
true ->
|
|
|
162 |
true;
|
|
|
163 |
_ ->
|
|
|
164 |
{checkout_block, R}
|
|
|
165 |
end
|
|
|
166 |
end;
|
|
|
167 |
postcondition(S,{call,_,checkout_nonblock,[_Pool]},R) ->
|
|
|
168 |
case R of
|
|
|
169 |
{full, _} ->
|
|
|
170 |
case length(S#state.checked_out) >= S#state.size + S#state.max_overflow of
|
|
|
171 |
true ->
|
|
|
172 |
true;
|
|
|
173 |
_ ->
|
|
|
174 |
{checkout_nonblock, R}
|
|
|
175 |
end;
|
|
|
176 |
_ ->
|
|
|
177 |
case length(S#state.checked_out) < S#state.size + S#state.max_overflow of
|
|
|
178 |
true ->
|
|
|
179 |
true;
|
|
|
180 |
_ ->
|
|
|
181 |
{checkout_block, R}
|
|
|
182 |
end
|
|
|
183 |
end;
|
|
|
184 |
postcondition(_S, {call,_,checkin,_}, R) ->
|
|
|
185 |
case R of
|
|
|
186 |
ok ->
|
|
|
187 |
true;
|
|
|
188 |
_ ->
|
|
|
189 |
{checkin, R}
|
|
|
190 |
end;
|
|
|
191 |
postcondition(_S,{call,_,_,_},_R) ->
|
|
|
192 |
true.
|
|
|
193 |
|
|
|
194 |
next_state(S,V,{call,_,start_poolboy, [Args]}) ->
|
|
|
195 |
S#state{pid=V,
|
|
|
196 |
size=proplists:get_value(size, Args),
|
|
|
197 |
max_overflow=proplists:get_value(max_overflow, Args)
|
|
|
198 |
};
|
|
|
199 |
next_state(S,_V,{call,_,stop_poolboy, [_Args]}) ->
|
|
|
200 |
S#state{pid=undefined, checked_out=[]};
|
|
|
201 |
next_state(S,V,{call,_,checkout_block,_}) ->
|
|
|
202 |
%% if the model says the checkout worked, store the result
|
|
|
203 |
case checkout_ok(S) of
|
|
|
204 |
false ->
|
|
|
205 |
S;
|
|
|
206 |
_ ->
|
|
|
207 |
S#state{checked_out=S#state.checked_out++[V]}
|
|
|
208 |
end;
|
|
|
209 |
next_state(S,V,{call,_,checkout_nonblock,_}) ->
|
|
|
210 |
%% if the model says the checkout worked, store the result
|
|
|
211 |
case checkout_ok(S) of
|
|
|
212 |
false ->
|
|
|
213 |
S;
|
|
|
214 |
_ ->
|
|
|
215 |
S#state{checked_out=S#state.checked_out++[V]}
|
|
|
216 |
end;
|
|
|
217 |
next_state(S,_V,{call, _, checkin, [_Pool, Worker]}) ->
|
|
|
218 |
S#state{checked_out=S#state.checked_out -- [Worker]};
|
|
|
219 |
next_state(S,_V,{call, _, kill_worker, [Worker]}) ->
|
|
|
220 |
S#state{checked_out=S#state.checked_out -- [Worker]};
|
|
|
221 |
next_state(S,_V,{call, _, kill_idle_worker, [_Pool]}) ->
|
|
|
222 |
S;
|
|
|
223 |
next_state(S,_V,{call, _, spurious_exit, [_Pool]}) ->
|
|
|
224 |
S;
|
|
|
225 |
next_state(S,V,{call, erlang, self, []}) ->
|
|
|
226 |
%% added after test generation, values are never symbolic
|
|
|
227 |
S#state{checked_out=[{Worker, Pid} || {Worker, Pid} <- S#state.checked_out, Pid /= V]}.
|
|
|
228 |
|
|
|
229 |
|
|
|
230 |
prop_sequential() ->
|
|
|
231 |
fault_rate(1, 10,
|
|
|
232 |
?FORALL(Cmds,commands(?MODULE),
|
|
|
233 |
?TRAPEXIT(
|
|
|
234 |
aggregate(command_names(Cmds),
|
|
|
235 |
begin
|
|
|
236 |
{H,S,Res} = run_commands(?MODULE,Cmds),
|
|
|
237 |
catch(stop_poolboy(whereis(poolboy_eqc))),
|
|
|
238 |
?WHENFAIL(io:format("History: ~p\nState: ~p\nRes: ~p\n~p\n",
|
|
|
239 |
[H,S,Res, zip(Cmds, [Y || {_, Y} <- H])]),
|
|
|
240 |
Res == ok)
|
|
|
241 |
end)))).
|
|
|
242 |
|
|
|
243 |
prop_parallel() ->
|
|
|
244 |
fault_rate(1, 10,
|
|
|
245 |
?FORALL(Cmds={Seq,Par},parallel_commands(?MODULE),
|
|
|
246 |
?TRAPEXIT(
|
|
|
247 |
aggregate(command_names(Cmds),
|
|
|
248 |
begin
|
|
|
249 |
NewPar = [P ++ [{set, {var, 0}, {call, erlang, self, []}}] || P <- Par],
|
|
|
250 |
{H,S,Res} = run_parallel_commands(?MODULE,{Seq,NewPar}),
|
|
|
251 |
catch(stop_poolboy(whereis(poolboy_eqc))),
|
|
|
252 |
?WHENFAIL(io:format("History: ~p\nState: ~p\nRes: ~p\n",
|
|
|
253 |
[H,S,Res]),
|
|
|
254 |
Res == ok)
|
|
|
255 |
end)))).
|
|
|
256 |
|
|
|
257 |
|
|
|
258 |
checkout_ok(S) ->
|
|
|
259 |
length(S#state.checked_out) < S#state.size + S#state.max_overflow.
|
|
|
260 |
|
|
|
261 |
-endif.
|
|
|
262 |
-endif.
|