|
| 1 | +-module(poolboy_eqc). |
| 2 | +-compile([poolboy_test_]). %%FIXME: Probably needs fix by adding missing functions. |
| 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_fsm:sync_send_all_state_event(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_fsm:sync_send_all_state_event(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_fsm:sync_send_all_state_event(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. |
0 commit comments