|
|
@@ -0,0 +1,471 @@
|
|
|
+%%% File : gproc_eqc.erl
|
|
|
+%%% Author : <norton@alum.mit.edu>
|
|
|
+%%% : <Ulf.Wiger@erlang-consulting.com>
|
|
|
+%%% : <John.Hughes@quviq.com>
|
|
|
+%%% Description : QuickCheck test model for gproc
|
|
|
+%%% Created : 11 Dec 2008 by <John Hughes@JTABLET2007>
|
|
|
+
|
|
|
+-module(gproc_eqc).
|
|
|
+
|
|
|
+
|
|
|
+-include("eqc.hrl").
|
|
|
+-include("eqc_statem.hrl").
|
|
|
+
|
|
|
+-compile(export_all).
|
|
|
+
|
|
|
+%%
|
|
|
+%% QUESTIONS:
|
|
|
+%%
|
|
|
+%% - does set_value for Class==a make sense?
|
|
|
+%%
|
|
|
+
|
|
|
+%%
|
|
|
+%% TODO Now:
|
|
|
+%%
|
|
|
+%% - add non integer to value() generator
|
|
|
+%% - implement mreg
|
|
|
+%% - implement lookup_pid/lookup_pids
|
|
|
+%%
|
|
|
+
|
|
|
+%%
|
|
|
+%% TODO Later:
|
|
|
+%%
|
|
|
+%% - implement send
|
|
|
+%% - implement info
|
|
|
+%% - implement select
|
|
|
+%% - implement first/next/prev/last
|
|
|
+%% - implement table
|
|
|
+%%
|
|
|
+
|
|
|
+%% records
|
|
|
+-record(key,
|
|
|
+ {class %% class()
|
|
|
+ , scope %% scope()
|
|
|
+ , name %% name()
|
|
|
+ }).
|
|
|
+
|
|
|
+-record(reg,
|
|
|
+ {pid %% pid()
|
|
|
+ , key %% key()
|
|
|
+ , value %% int()
|
|
|
+ }).
|
|
|
+
|
|
|
+-record(state,
|
|
|
+ {pids=[] %% [pid()]
|
|
|
+ , killed=[] %% [pid()]
|
|
|
+ , regs=[] %% [reg()]
|
|
|
+ }).
|
|
|
+
|
|
|
+
|
|
|
+%% external API
|
|
|
+start_test() ->
|
|
|
+ eqc:module({numtests, 500}, ?MODULE).
|
|
|
+
|
|
|
+run() ->
|
|
|
+ run(500).
|
|
|
+
|
|
|
+run(Num) ->
|
|
|
+ eqc:quickcheck(eqc:numtests(Num, prop_gproc())).
|
|
|
+
|
|
|
+
|
|
|
+%% Command generator, S is the state
|
|
|
+command(S) ->
|
|
|
+ oneof(
|
|
|
+ %% spawn
|
|
|
+ [ {call,?MODULE,spawn, []} ]
|
|
|
+
|
|
|
+ %% where
|
|
|
+ ++ [ {call,?MODULE,where, [key()]} ]
|
|
|
+
|
|
|
+ %% kill
|
|
|
+ ++ [ oneof([
|
|
|
+ %% kill
|
|
|
+ {call,?MODULE,kill, [elements(S#state.pids)]}
|
|
|
+ %% register
|
|
|
+ , {call,?MODULE,reg, [elements(S#state.pids), key(), value()]}
|
|
|
+ %% unregister
|
|
|
+ , {call,?MODULE,unreg, [elements(S#state.pids), key()]}
|
|
|
+ %% many register
|
|
|
+ %%, {call,?MODULE,mreg, [elements(S#state.pids), class(), scope(), list({name(), value()})]}
|
|
|
+
|
|
|
+ %% set_value
|
|
|
+ , {call,?MODULE,set_value, [elements(S#state.pids), key(), value()]}
|
|
|
+ %% update_counter
|
|
|
+ , {call,?MODULE,update_counter, [elements(S#state.pids), key(), value()]}
|
|
|
+
|
|
|
+ %% get_value
|
|
|
+ , {call,?MODULE,get_value, [elements(S#state.pids), key()]}
|
|
|
+ %% lookup_pid
|
|
|
+ %%, {call,gproc,lookup_pid, [key()]}
|
|
|
+ %% lookup_pids
|
|
|
+ %%, {call,gproc,lookup_pids, [key()]}
|
|
|
+ ])
|
|
|
+ || S#state.pids/=[] ]
|
|
|
+ ).
|
|
|
+
|
|
|
+%% generator class
|
|
|
+class() -> elements([n,p,c,a]).
|
|
|
+
|
|
|
+%% generator scope
|
|
|
+scope() -> l.
|
|
|
+
|
|
|
+%% generator name
|
|
|
+name() -> elements([x,y,z,w]).
|
|
|
+
|
|
|
+%% generator key
|
|
|
+key() -> #key{class=class(), scope=scope(), name=name()}.
|
|
|
+
|
|
|
+%% generator value
|
|
|
+value() -> int().
|
|
|
+
|
|
|
+
|
|
|
+%% helpers
|
|
|
+is_register_ok(S,Pid,Key,_Value) ->
|
|
|
+ [] == [ Pid1 || #reg{pid=Pid1,key=Key1}
|
|
|
+ <- S#state.regs, is_register_eq(Pid,Key,Pid1,Key1) ].
|
|
|
+
|
|
|
+is_register_eq(_PidA,#key{class=Class}=KeyA,_PidB,KeyB)
|
|
|
+ when Class == n; Class ==a ->
|
|
|
+ KeyA==KeyB;
|
|
|
+is_register_eq(PidA,KeyA,PidB,KeyB) ->
|
|
|
+ PidA==PidB andalso KeyA==KeyB.
|
|
|
+
|
|
|
+is_unregister_ok(S,Pid,Key) ->
|
|
|
+ [] /= [ Pid1 || #reg{pid=Pid1,key=Key1}
|
|
|
+ <- S#state.regs, is_unregister_eq(Pid,Key,Pid1,Key1) ].
|
|
|
+
|
|
|
+is_unregister_eq(PidA,KeyA,PidB,KeyB) ->
|
|
|
+ KeyA==KeyB andalso PidA==PidB.
|
|
|
+
|
|
|
+is_registered_and_alive(S,Pid,Key) ->
|
|
|
+ is_unregister_ok(S,Pid,Key)
|
|
|
+ andalso lists:member(Pid,S#state.pids).
|
|
|
+
|
|
|
+
|
|
|
+%% Initialize the state
|
|
|
+initial_state() ->
|
|
|
+ #state{}.
|
|
|
+
|
|
|
+
|
|
|
+%% Next state transformation, S is the current state
|
|
|
+%% spawn
|
|
|
+next_state(S,V,{call,_,spawn,_}) ->
|
|
|
+ S#state{pids=[V|S#state.pids]};
|
|
|
+%% kill
|
|
|
+next_state(S,_V,{call,_,kill,[Pid]}) ->
|
|
|
+ S#state{pids=S#state.pids -- [Pid]
|
|
|
+ , killed=[Pid|S#state.killed]
|
|
|
+ , regs=[ X || #reg{pid=Pid1}=X <- S#state.regs, Pid/=Pid1 ]
|
|
|
+ };
|
|
|
+%% reg
|
|
|
+next_state(S,_V,{call,_,reg,[Pid,Key,Value]}) ->
|
|
|
+ case is_register_ok(S,Pid,Key,Value) of
|
|
|
+ false ->
|
|
|
+ S;
|
|
|
+ true ->
|
|
|
+ case Key of
|
|
|
+ #key{class=a,name=Name} ->
|
|
|
+ %% initialize aggr counter
|
|
|
+ FunC = fun(#reg{key=#key{class=Class1,name=Name1}}) -> (Class1 == c andalso Name==Name1) end,
|
|
|
+ {Regs, _Others} = lists:partition(FunC, S#state.regs),
|
|
|
+ InitialValue = lists:sum([ V || #reg{value=V} <- Regs ]),
|
|
|
+ S#state{regs=[#reg{pid=Pid,key=Key,value=InitialValue}|S#state.regs]};
|
|
|
+ #key{class=c,name=Name} ->
|
|
|
+ S1 = S#state{regs=[#reg{pid=Pid,key=Key,value=Value}|S#state.regs]},
|
|
|
+ %% update aggr counter
|
|
|
+ FunA = fun(#reg{key=#key{class=Class1,name=Name1}}) -> (Class1 == a andalso Name==Name1) end,
|
|
|
+ case lists:partition(FunA, S1#state.regs) of
|
|
|
+ {[Reg], Others} ->
|
|
|
+ S1#state{regs=[Reg#reg{value=Reg#reg.value+Value}|Others]};
|
|
|
+ {[], _Others} ->
|
|
|
+ S1
|
|
|
+ end;
|
|
|
+ _ ->
|
|
|
+ S#state{regs=[#reg{pid=Pid,key=Key,value=Value}|S#state.regs]}
|
|
|
+ end
|
|
|
+ end;
|
|
|
+%% unreg
|
|
|
+next_state(S,_V,{call,_,unreg,[Pid,Key]}) ->
|
|
|
+ case is_unregister_ok(S,Pid,Key) of
|
|
|
+ false ->
|
|
|
+ S;
|
|
|
+ true ->
|
|
|
+ FunC = fun(#reg{pid=Pid1,key=Key1}) -> (Pid==Pid1 andalso Key==Key1) end,
|
|
|
+ case lists:partition(FunC, S#state.regs) of
|
|
|
+ {[#reg{value=Value}], Others} ->
|
|
|
+ S1 = S#state{regs=Others},
|
|
|
+ case Key of
|
|
|
+ #key{class=c,name=Name} ->
|
|
|
+ %% update aggr counter
|
|
|
+ FunA = fun(#reg{key=#key{class=Class1,name=Name1}}) -> (Class1 == a andalso Name==Name1) end,
|
|
|
+ case lists:partition(FunA, S1#state.regs) of
|
|
|
+ {[], _Others1} ->
|
|
|
+ S1;
|
|
|
+ {[Reg], Others1} ->
|
|
|
+ S1#state{regs=[Reg#reg{value=Reg#reg.value-Value}|Others1]}
|
|
|
+ end;
|
|
|
+ _ ->
|
|
|
+ S1
|
|
|
+ end
|
|
|
+ end
|
|
|
+ end;
|
|
|
+%% set_value
|
|
|
+next_state(S,_V,{call,_,set_value,[Pid,Key,Value]}) ->
|
|
|
+ case is_registered_and_alive(S,Pid,Key) of
|
|
|
+ false ->
|
|
|
+ S;
|
|
|
+ true ->
|
|
|
+ FunC = fun(#reg{pid=Pid1,key=Key1}) -> (Pid==Pid1 andalso Key==Key1) end,
|
|
|
+ case lists:partition(FunC, S#state.regs) of
|
|
|
+ {[#reg{value=OldValue}=OldReg], Others} ->
|
|
|
+ S1 = S#state{regs=[OldReg#reg{value=Value}|Others]},
|
|
|
+ case Key of
|
|
|
+ #key{class=c,name=Name} ->
|
|
|
+ %% aggr counter update
|
|
|
+ FunA = fun(#reg{key=#key{class=Class1,name=Name1}}) -> (Class1 == a andalso Name==Name1) end,
|
|
|
+ case lists:partition(FunA, S1#state.regs) of
|
|
|
+ {[], _Others1} ->
|
|
|
+ S1;
|
|
|
+ {[Reg], Others1} ->
|
|
|
+ S1#state{regs=[Reg#reg{value=Reg#reg.value-OldValue+Value}|Others1]}
|
|
|
+ end;
|
|
|
+ _ ->
|
|
|
+ S1
|
|
|
+ end
|
|
|
+ end
|
|
|
+ end;
|
|
|
+%% update_counter
|
|
|
+next_state(S,_V,{call,_,update_counter,[Pid,#key{class=Class}=Key,Incr]})
|
|
|
+ when Class == c ->
|
|
|
+ case is_registered_and_alive(S,Pid,Key) of
|
|
|
+ false ->
|
|
|
+ S;
|
|
|
+ true ->
|
|
|
+ FunC = fun(#reg{pid=Pid1,key=Key1}) -> (Pid==Pid1 andalso Key==Key1) end,
|
|
|
+ case lists:partition(FunC, S#state.regs) of
|
|
|
+ {[#reg{value=OldValue}=OldReg], Others} ->
|
|
|
+ S1 = S#state{regs=[OldReg#reg{value=OldValue+Incr}|Others]},
|
|
|
+ case Key of
|
|
|
+ #key{class=c,name=Name} ->
|
|
|
+ %% aggr counter update
|
|
|
+ FunA = fun(#reg{key=#key{class=Class1,name=Name1}}) -> (Class1 == a andalso Name==Name1) end,
|
|
|
+ case lists:partition(FunA, S1#state.regs) of
|
|
|
+ {[], _Others1} ->
|
|
|
+ S1;
|
|
|
+ {[Reg], Others1} ->
|
|
|
+ S1#state{regs=[Reg#reg{value=Reg#reg.value+Incr}|Others1]}
|
|
|
+ end;
|
|
|
+ _ ->
|
|
|
+ S1
|
|
|
+ end
|
|
|
+ end
|
|
|
+ end;
|
|
|
+%% otherwise
|
|
|
+next_state(S,_V,{call,_,_,_}) ->
|
|
|
+ S.
|
|
|
+
|
|
|
+
|
|
|
+%% Precondition, checked before command is added to the command
|
|
|
+%% sequence
|
|
|
+precondition(_S,{call,_,_,_}) ->
|
|
|
+ true.
|
|
|
+
|
|
|
+
|
|
|
+%% Postcondition, checked after command has been evaluated. S is the
|
|
|
+%% state before next_state(S,_,<command>)
|
|
|
+
|
|
|
+%% spawn
|
|
|
+postcondition(_S,{call,_,spawn,_},_Res) ->
|
|
|
+ true;
|
|
|
+%% kill
|
|
|
+postcondition(_S,{call,_,kill,_},_Res) ->
|
|
|
+ true;
|
|
|
+%% where
|
|
|
+postcondition(S,{call,_,where,[#key{class=Class}=Key]},Res) ->
|
|
|
+ if Class == n orelse Class == a ->
|
|
|
+ case lists:keysearch(Key,#reg.key,S#state.regs) of
|
|
|
+ {value, #reg{pid=Pid}} ->
|
|
|
+ Res == Pid;
|
|
|
+ false ->
|
|
|
+ Res == undefined
|
|
|
+ end;
|
|
|
+ true ->
|
|
|
+ case Res of
|
|
|
+ {'EXIT', {badarg, _}} ->
|
|
|
+ true;
|
|
|
+ _ ->
|
|
|
+ false
|
|
|
+ end
|
|
|
+ end;
|
|
|
+%% reg
|
|
|
+postcondition(S,{call,_,reg,[Pid,Key,Value]},Res) ->
|
|
|
+ case Res of
|
|
|
+ true ->
|
|
|
+ is_register_ok(S,Pid,Key,Value);
|
|
|
+ {'EXIT', {badarg, _}} ->
|
|
|
+ is_unregister_ok(S,Pid,Key)
|
|
|
+ orelse not is_register_ok(S,Pid,Key,Value)
|
|
|
+ end;
|
|
|
+%% unreg
|
|
|
+postcondition(S,{call,_,unreg,[Pid,Key]},Res) ->
|
|
|
+ case Res of
|
|
|
+ true ->
|
|
|
+ is_unregister_ok(S,Pid,Key);
|
|
|
+ {'EXIT', {badarg, _}} ->
|
|
|
+ not is_unregister_ok(S,Pid,Key)
|
|
|
+ end;
|
|
|
+%% set_value
|
|
|
+postcondition(S,{call,_,set_value,[Pid,Key,_Value]},Res) ->
|
|
|
+ case Res of
|
|
|
+ true ->
|
|
|
+ is_registered_and_alive(S,Pid,Key);
|
|
|
+ {'EXIT', {badarg, _}} ->
|
|
|
+ not is_registered_and_alive(S,Pid,Key)
|
|
|
+ end;
|
|
|
+%% update_counter
|
|
|
+postcondition(S,{call,_,update_counter,[Pid,#key{class=Class}=Key,Incr]},Res)
|
|
|
+ when Class == c ->
|
|
|
+ case [ Value1 || #reg{pid=Pid1,key=Key1,value=Value1} <- S#state.regs
|
|
|
+ , (Pid==Pid1 andalso Key==Key1) ] of
|
|
|
+ [] ->
|
|
|
+ case Res of {'EXIT', {badarg, _}} -> true; _ -> false end;
|
|
|
+ [Value] ->
|
|
|
+ Res == Value+Incr
|
|
|
+ end;
|
|
|
+postcondition(_S,{call,_,update_counter,[_Pid,_Key,_Incr]},Res) ->
|
|
|
+ case Res of {'EXIT', {badarg, _}} -> true; _ -> false end;
|
|
|
+%% get_value
|
|
|
+postcondition(S,{call,_,get_value,[Pid,Key]},Res) ->
|
|
|
+ case [ Value1 || #reg{pid=Pid1,key=Key1,value=Value1} <- S#state.regs
|
|
|
+ , (Pid==Pid1 andalso Key==Key1) ] of
|
|
|
+ [] ->
|
|
|
+ case Res of {'EXIT', {badarg, _}} -> true; _ -> false end;
|
|
|
+ [Value] ->
|
|
|
+ Res == Value
|
|
|
+ end;
|
|
|
+%% otherwise
|
|
|
+postcondition(_S,{call,_,_,_},_Res) ->
|
|
|
+ false.
|
|
|
+
|
|
|
+%% property
|
|
|
+prop_gproc() ->
|
|
|
+ ?FORALL(Cmds,commands(?MODULE),
|
|
|
+ ?TRAPEXIT(
|
|
|
+ begin
|
|
|
+ ok = stop_app(),
|
|
|
+ ok = start_app(),
|
|
|
+ {H,S,Res} = run_commands(?MODULE,Cmds),
|
|
|
+ kill_all_pids({H,S}),
|
|
|
+
|
|
|
+ %% whenfail
|
|
|
+ ?WHENFAIL(
|
|
|
+ begin
|
|
|
+ io:format("~nHISTORY:"),
|
|
|
+ if
|
|
|
+ length(H) < 1 ->
|
|
|
+ io:format(" none~n");
|
|
|
+ true ->
|
|
|
+ CmdsH = eqc_statem:zip(Cmds,H),
|
|
|
+ [ begin
|
|
|
+ {Cmd,{State,Reply}} = lists:nth(N,CmdsH),
|
|
|
+ io:format("~n #~p:~n\tCmd: ~p~n\tReply: ~p~n\tState: ~p~n",
|
|
|
+ [N,Cmd,Reply,State])
|
|
|
+ end
|
|
|
+ || N <- lists:seq(1,length(CmdsH)) ]
|
|
|
+ end,
|
|
|
+ io:format("~nRESULT:~n\t~p~n",[Res]),
|
|
|
+ io:format("~nSTATE:~n\t~p~n",[S])
|
|
|
+ end,
|
|
|
+ Res == ok)
|
|
|
+ end)).
|
|
|
+
|
|
|
+%% helpers
|
|
|
+start_app() ->
|
|
|
+ case application:start(gproc) of
|
|
|
+ {error, {already_started,_}} ->
|
|
|
+ stop_app(),
|
|
|
+ ok = application:start(gproc);
|
|
|
+ ok ->
|
|
|
+ ok
|
|
|
+ end.
|
|
|
+
|
|
|
+stop_app() ->
|
|
|
+ case application:stop(gproc) of
|
|
|
+ {error, {not_started,_}} ->
|
|
|
+ ok;
|
|
|
+ ok ->
|
|
|
+ ok
|
|
|
+ end.
|
|
|
+
|
|
|
+%% If using the scheduler... This code needs to run in a separate
|
|
|
+%% module, so it can be compiled without instrumentation.
|
|
|
+kill_all_pids(Pid) when is_pid(Pid) ->
|
|
|
+ case is_process_alive(Pid) of
|
|
|
+ true ->
|
|
|
+ exit(Pid,kill);
|
|
|
+ false ->
|
|
|
+ ok
|
|
|
+ end;
|
|
|
+kill_all_pids(Tup) when is_tuple(Tup) ->
|
|
|
+ kill_all_pids(tuple_to_list(Tup));
|
|
|
+kill_all_pids([H|T]) ->
|
|
|
+ kill_all_pids(H),
|
|
|
+ kill_all_pids(T);
|
|
|
+kill_all_pids(_) ->
|
|
|
+ ok.
|
|
|
+
|
|
|
+
|
|
|
+%% spawn
|
|
|
+spawn() ->
|
|
|
+ spawn(fun() -> loop() end).
|
|
|
+
|
|
|
+loop() ->
|
|
|
+ receive
|
|
|
+ {From, Ref, F} ->
|
|
|
+ From ! {Ref, catch F()},
|
|
|
+ loop();
|
|
|
+ stop -> ok
|
|
|
+ end.
|
|
|
+
|
|
|
+%% kill
|
|
|
+kill(Pid) ->
|
|
|
+ exit(Pid,foo),
|
|
|
+ timer:sleep(10).
|
|
|
+
|
|
|
+%% where
|
|
|
+where(#key{class=Class,scope=Scope,name=Name}) ->
|
|
|
+ catch gproc:where({Class,Scope,Name}).
|
|
|
+
|
|
|
+%% reg
|
|
|
+reg(Pid,#key{class=Class,scope=Scope,name=Name},Value) ->
|
|
|
+ do(Pid, fun() -> catch gproc:reg({Class,Scope,Name},Value) end).
|
|
|
+
|
|
|
+%% unreg
|
|
|
+unreg(Pid,#key{class=Class,scope=Scope,name=Name}) ->
|
|
|
+ do(Pid, fun() -> catch gproc:unreg({Class,Scope,Name}) end).
|
|
|
+
|
|
|
+%% set_value
|
|
|
+set_value(Pid,#key{class=Class,scope=Scope,name=Name},Value) ->
|
|
|
+ do(Pid, fun() -> catch gproc:set_value({Class,Scope,Name},Value) end).
|
|
|
+
|
|
|
+%% update_counter
|
|
|
+update_counter(Pid, #key{class=Class,scope=Scope,name=Name},Incr) ->
|
|
|
+ do(Pid, fun() -> catch gproc:update_counter({Class,Scope,Name},Incr) end).
|
|
|
+
|
|
|
+%% get_value
|
|
|
+get_value(Pid,#key{class=Class,scope=Scope,name=Name}) ->
|
|
|
+ do(Pid, fun() -> catch gproc:get_value({Class,Scope,Name}) end).
|
|
|
+
|
|
|
+%% do
|
|
|
+do(Pid, F) ->
|
|
|
+ Ref = erlang:monitor(process, Pid),
|
|
|
+ Pid ! {self(), Ref, F},
|
|
|
+ receive
|
|
|
+ {'DOWN', Ref, process, Pid, Reason} ->
|
|
|
+ {'EXIT', {'DOWN', Reason}};
|
|
|
+ {Ref, Result} ->
|
|
|
+ erlang:demonitor(Ref),
|
|
|
+ Result
|
|
|
+ after 3000 ->
|
|
|
+ {'EXIT', timeout}
|
|
|
+ end.
|
jwnorton