Skip to content

Instantly share code, notes, and snippets.

@jrwest

jrwest/riak_core_bg_manager_eqc.erl Secret

Last active December 20, 2015 03:39
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jrwest/c543a4e57e9edf5ce5fe to your computer and use it in GitHub Desktop.
Save jrwest/c543a4e57e9edf5ce5fe to your computer and use it in GitHub Desktop.
Download ZIP
in flux
Raw
gistfile1.md 
[{set,{var,1},{call,riak_core_bg_manager_eqc,create_lock,[c]}},
 {set,{var,14},{call,riak_core_bg_manager_eqc,start_process,[]}},
 {set,{var,15},{call,riak_core_bg_manager_eqc,get_lock,[c,{var,14},[]]}},
 {set,{var,18},{call,riak_core_bg_manager_eqc,create_lock,[b]}},
 {set,{var,25},{call,riak_core_bg_manager_eqc,start_process,[]}},
 {set,{var,27},{call,riak_core_bg_manager_eqc,get_lock,[c,{var,25},[]]}},
 {set,{var,28},{call,riak_core_bg_manager_eqc,get_lock,[b,{var,14},[]]}},
 {set,{var,57},{call,riak_core_bg_manager_eqc,start_process,[]}},
 {set,{var,59},{call,riak_core_bg_manager,disable,[b,true]}},
 {set,{var,60},{call,riak_core_bg_manager_eqc,get_lock,[c,{var,57},[]]}}]

S: #state{
     limits = [],
     enabled = [],
     disabled = [],
     global_enable = true,
     running_procs = [],
     created_locks = [],
     limit_killed = [],
     locks = [] }

riak_core_bg_manager_eqc:create_lock(c) -> {0, []}

S: #state{
     limits = [{c, 2}],
     enabled = [],
     disabled = [],
     global_enable = true,
     running_procs = [],
     created_locks = [c],
     limit_killed = [],
     locks = [] }

riak_core_bg_manager_eqc:start_process() -> <0.164.0>

S: #state{
     limits = [{c, 2}],
     enabled = [],
     disabled = [],
     global_enable = true,
     running_procs = [<0.164.0>],
     created_locks = [c],
     limit_killed = [],
     locks = [] }

riak_core_bg_manager_eqc:get_lock(c, <0.164.0>, []) ->
    #Ref<0.0.0.189>

S: #state{
     limits = [{c, 2}],
     enabled = [],
     disabled = [],
     global_enable = true,
     running_procs = [<0.164.0>],
     created_locks = [c],
     limit_killed = [],
     locks = [{c, [{#Ref<0.0.0.189>, <0.164.0>, [], active}]}] }

riak_core_bg_manager_eqc:create_lock(b) -> {0, []}

S: #state{
     limits = [{c, 2}, {b, 2}],
     enabled = [],
     disabled = [],
     global_enable = true,
     running_procs = [<0.164.0>],
     created_locks = [b, c],
     limit_killed = [],
     locks = [{c, [{#Ref<0.0.0.189>, <0.164.0>, [], active}]}] }

riak_core_bg_manager_eqc:start_process() -> <0.165.0>

S: #state{
     limits = [{c, 2}, {b, 2}],
     enabled = [],
     disabled = [],
     global_enable = true,
     running_procs = [<0.165.0>, <0.164.0>],
     created_locks = [b, c],
     limit_killed = [],
     locks = [{c, [{#Ref<0.0.0.189>, <0.164.0>, [], active}]}] }

riak_core_bg_manager_eqc:get_lock(c, <0.165.0>, []) ->
    #Ref<0.0.0.193>

S: #state{
     limits = [{c, 2}, {b, 2}],
     enabled = [],
     disabled = [],
     global_enable = true,
     running_procs = [<0.165.0>, <0.164.0>],
     created_locks = [b, c],
     limit_killed = [],
     locks =
       [{c, [{#Ref<0.0.0.193>, <0.165.0>, [], active},
             {#Ref<0.0.0.189>, <0.164.0>, [], active}]}] }

riak_core_bg_manager_eqc:get_lock(b, <0.164.0>, []) ->
    #Ref<0.0.0.196>

S: #state{
     limits = [{c, 2}, {b, 2}],
     enabled = [],
     disabled = [],
     global_enable = true,
     running_procs = [<0.165.0>, <0.164.0>],
     created_locks = [b, c],
     limit_killed = [],
     locks =
       [{c, [{#Ref<0.0.0.193>, <0.165.0>, [], active},
             {#Ref<0.0.0.189>, <0.164.0>, [], active}]},
        {b, [{#Ref<0.0.0.196>, <0.164.0>, [], active}]}] }

riak_core_bg_manager_eqc:start_process() -> <0.166.0>

S: #state{
     limits = [{c, 2}, {b, 2}],
     enabled = [],
     disabled = [],
     global_enable = true,
     running_procs = [<0.166.0>, <0.165.0>, <0.164.0>],
     created_locks = [b, c],
     limit_killed = [],
     locks =
       [{c, [{#Ref<0.0.0.193>, <0.165.0>, [], active},
             {#Ref<0.0.0.189>, <0.164.0>, [], active}]},
        {b, [{#Ref<0.0.0.196>, <0.164.0>, [], active}]}] }

riak_core_bg_manager:disable(b, true) -> ok

S: #state{
     limits = [{c, 2}, {b, 2}],
     enabled = [],
     disabled = [b],
     global_enable = true,
     running_procs = [<0.166.0>, <0.165.0>],
     created_locks = [b, c],
     limit_killed = [],
     locks =
       [{c, [{#Ref<0.0.0.193>, <0.165.0>, [], active},
             {#Ref<0.0.0.189>, <0.164.0>, [], inactive}]},
        {b, [{#Ref<0.0.0.196>, <0.164.0>, [], inactive}]}] }

riak_core_bg_manager_eqc:get_lock(c, <0.166.0>, []) ->
    max_concurrency

S: #state{
     limits = [{c, 2}, {b, 2}],
     enabled = [],
     disabled = [b],
     global_enable = true,
     running_procs = [<0.166.0>, <0.165.0>],
     created_locks = [b, c],
     limit_killed = [],
     locks =
       [{c, [{#Ref<0.0.0.193>, <0.165.0>, [], active},
             {#Ref<0.0.0.189>, <0.164.0>, [], inactive}]},
        {b, [{#Ref<0.0.0.196>, <0.164.0>, [], inactive}]}] }

Reason: {postcondition, false}
false
Raw
riak_core_bg_manager_eqc.erl
%% -------------------------------------------------------------------
%%
%%
%% Copyright (c) 2013 Basho Technologies, Inc. All Rights Reserved.
%%
%% This file is provided to you under the Apache License,
%% Version 2.0 (the "License"); you may not use this file
%% except in compliance with the License. You may obtain
%% a copy of the License at
%%
%% http://www.apache.org/licenses/LICENSE-2.0
%%
%% Unless required by applicable law or agreed to in writing,
%% software distributed under the License is distributed on an
%% "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
%% KIND, either express or implied. See the License for the
%% specific language governing permissions and limitations
%% under the License.
%%
%% -------------------------------------------------------------------
-module(riak_core_bg_manager_eqc).
-ifdef(EQC).
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_statem.hrl").
-include_lib("eunit/include/eunit.hrl").
-compile(export_all).
-define(QC_OUT(P),
eqc:on_output(fun(Str, Args) -> io:format(user, Str, Args) end, P)).
-define(STARTING_LIMIT, 2).
-define(LOCK_TYPES, [a,b,c,d,e]).
-record(state,{
limits :: [{atom(), non_neg_integer() | infinity}],
enabled :: ordset:ordset(),
disabled :: ordset:ordset(),
global_enable :: boolean(),
running_procs :: [pid()],
created_locks :: [atom()],
limit_killed :: [[pid()]],
locks :: [{atom(), [{reference(), pid(), [{atom(), term()}], active | inactive}]}]
}).
run_eqc() ->
run_eqc(1000).
run_eqc(N) ->
run_eqc(N, prop_bg_manager_locks).
run_eqc_para() ->
run_eqc_para(1000).
run_eqc_para(N) ->
run_eqc(N, prop_bg_manager_locks_para).
run_eqc(N, Prop) ->
eqc:quickcheck(eqc:numtests(N, ?QC_OUT(?MODULE:Prop()))).
check() ->
eqc:check(eqc_gen:with_parameter(show_states, true, ?MODULE:prop_bg_manager_locks())).
%% @doc Returns the state in which each test case starts. (Unless a different
%% initial state is supplied explicitly to, e.g. commands/2.)
-spec initial_state() -> eqc_statem:symbolic_state().
initial_state() ->
#state{limits=[],
enabled=ordsets:new(), %% TODO: remove me, i'm not needed, disabled is sufficient
disabled=ordsets:new(),
global_enable=true,
running_procs=[],
limit_killed=[],
created_locks=[],
locks=[]}.
%% @doc Command generator, S is the current state
-spec command(S :: eqc_statem:symbolic_state()) -> eqc_gen:gen(eqc_statem:call()).
command(#state{running_procs=Running,created_locks=CreatedLocks}) ->
LimitFreq = case length(Running) > 0 of
true -> 15;
false -> 35
end,
EnableDisableFreq=10,
%% In the case there are no running processes no calls to get_lock/3 will be generated
%% so the processes commands get its slice of the pie for command generation (making it
%% more likely we create a process soon so we can start getting locks!)
ResourcesFreq = case length(Running) > 0 of
true -> 25;
false -> 35
end,
GetLockFreq = 30,
QueryLocksFreq = 20,
%% Commands that deal with concurrency limits for a given lock type
LimitCommands = [{call,
?MODULE, set_concurrency_limit,
%% TODO: change back to boolean
[lock_type(), concurrency_limit(), true]},
{call,
riak_core_bg_manager, concurrency_limit,
[lock_type()]}],
%% Commands that enable and disable per-lock type and globally
EnableDisableCommands =
[{call, riak_core_bg_manager, enable, [lock_type()]},
{call, riak_core_bg_manager, disable, [lock_type(), bool()]},
{call, riak_core_bg_manager, enable, []},
{call, riak_core_bg_manager, disable, []}],
%% Commands that start and stop processes that will have locks aqcuired on their behalf
ResourceCommands =
[{call, ?MODULE, start_process, []}] ++
[{call, ?MODULE, create_lock, [new_lock_type(CreatedLocks)]} ||
length(CreatedLocks) < length(?LOCK_TYPES)],
%% ++ [{call, ?MODULE, stop_process, [oneof(Running)]} ||
% length(Running) > 0],
%% The get_lock command
GetLockCommand =
{call, ?MODULE, get_lock, [existing_lock_type(CreatedLocks), oneof(Running), metadata()]},
%% TODO: change to just query_locks and make arg. generator include empty list
%% Query command
QueryLocksCommand = {call, riak_core_bg_manager, all_locks, []},
Limit = [{LimitFreq, oneof(LimitCommands)}],
EnableDisable = [{EnableDisableFreq, oneof(EnableDisableCommands)}],
Resources = [{ResourcesFreq, oneof(ResourceCommands)}],
GetLock = [{GetLockFreq, GetLockCommand} || (length(Running) > 0) andalso (length(CreatedLocks) > 0)],
QueryLocks = [{QueryLocksFreq, QueryLocksCommand}],
_A = frequency(Limit ++ EnableDisable ++ Resources ++ GetLock ++ QueryLocks),
oneof(LimitCommands ++ EnableDisableCommands ++ ResourceCommands ++
[GetLockCommand || length(Running) > 0 andalso length(CreatedLocks) > 0] ++
[QueryLocksCommand]).
%% @doc lock type generator. lock type can be any term, so we arbitrarily choose
%% a space of 100 integers as the lock types we may potentially test
lock_type() ->
oneof(?LOCK_TYPES).
existing_lock_type(ExistingTypes) ->
oneof(ExistingTypes).
%% @doc return a lock type we haven't "created" already
new_lock_type(ExistingTypes) ->
?SUCHTHAT(Type, lock_type(), not lists:member(Type, ExistingTypes)).
%% @doc concurrency limit generator. concurrency limit can be any positive integer
%% or infinity
concurrency_limit() ->
frequency([{5, infinity}, {95, choose(1, 10)}]).
%% TODO: implement me
metadata() ->
[].
%% @doc Next state transformation, S is the current state. Returns next state.
-spec next_state(S :: eqc_statem:symbolic_state(), V :: eqc_statem:var(),
C :: eqc_statem:call()) -> eqc_statem:symbolic_state().
next_state(S=#state{running_procs=Running}, Pid,
{call, ?MODULE, start_process, []}) ->
S#state{running_procs=[Pid | Running]};
next_state(S=#state{running_procs=Running}, _, {call, ?MODULE, stop_process, [Pid]}) ->
S#state{running_procs=lists:delete(Pid, Running)};
next_state(S=#state{created_locks=Created,limits=Limits}, _, {call, ?MODULE, create_lock, [LockType]}) ->
S#state{created_locks=[LockType | Created],
limits=lists:keystore(LockType, 1, Limits, {LockType, ?STARTING_LIMIT})};
next_state(S=#state{limits=Limits}, KilledPids,
{call, ?MODULE, set_concurrency_limit, [LockType, NewLimit, _Kill]}) ->
%% can't mark locks owned by KilledPids as inactive because KilledPids may be symbolic return value
%% (e.g. not a list) so instead we build up a list of list of killed pids to keep track of this
S#state{limits=lists:keystore(LockType, 1, Limits, {LockType, NewLimit}),
limit_killed=[KilledPids | S#state.limit_killed]};
next_state(S=#state{enabled=Enabled,disabled=Disabled}, _V,
{call, riak_core_bg_manager, enable, [LockType]}) ->
S#state{enabled=ordsets:add_element(LockType, Enabled),
disabled=ordsets:del_element(LockType, Disabled)};
next_state(S=#state{enabled=Enabled,disabled=Disabled,locks=Locks, running_procs=Running}, _V,
{call, riak_core_bg_manager, disable, [LockType, Kill]}) ->
Updates = case Kill of
true ->
%% If we are killing processes that hold the locks, they will release
%% any other locks they hold. account for this.
Held = get_lock_info(LockType, S),
{KilledPids, Inactive} = mark_inactive(Held),
Locks2 = lists:keystore(LockType, 1, Locks, {LockType, Inactive}),
Locks3 = [{LT, mark_inactive(H, KilledPids)} || {LT, H} <- Locks2],
{Locks3, Running -- KilledPids};
false -> {Locks, Running}
end,
{NewLocks, NewRunning} = Updates,
S#state{enabled=ordsets:del_element(LockType, Enabled),
disabled=ordsets:add_element(LockType, Disabled),
running_procs=NewRunning,
locks=NewLocks};
next_state(S, _V, {call, riak_core_bg_manager, enable, []}) ->
S#state{global_enable=true};
next_state(S, _V, {call, riak_core_bg_manager, disable, []}) ->
S#state{global_enable=false};
next_state(S=#state{locks=Locks}, RefOrMaxC,
{call, ?MODULE, get_lock, [LockType, Pid, Metadata]}) ->
TypeLimit = get_limit(LockType, S),
Existing = get_lock_info(LockType, S),
ExistingCount = get_lock_count(LockType, S),
Enabled = is_enabled(LockType, S),
TooMany = ExistingCount >= TypeLimit,
%% lock manager and lock type must be enabled and must not be above concurrency limit
case not Enabled or TooMany of
%% max_concurrency
true -> S;
%% lock acquired
false ->
S#state{locks=lists:keystore(LockType, 1, Locks,
{LockType, [{RefOrMaxC, Pid, Metadata, active} | Existing]})}
end;
next_state(S, _V, {call, _, _, _}) ->
S.
%% @doc Precondition, checked before command is added to the command sequence.
-spec precondition(S :: eqc_statem:symbolic_state(), C :: eqc_statem:call()) -> boolean().
precondition(S, {call, ?MODULE, get_lock, [LockType, _, _]}) ->
get_limit(LockType, S) =/= 0;
precondition(_S, {call, _, _, _}) ->
true.
%% @doc Postcondition, checked after command has been evaluated
%% Note: S is the state before next_state(S,_,C)
-spec postcondition(S :: eqc_statem:dynamic_state(), C :: eqc_statem:call(),
Res :: term()) -> boolean().
postcondition(_S, {call, ?MODULE, start_process, []}, _Pid) ->
true;
postcondition(_S, {call, ?MODULE, stop_process, [_Pid]}, _) ->
true;
postcondition(_S, {call, ?MODULE, create_lock, [_LockType]}, _) ->
true;
postcondition(_S, {call, ?MODULE, set_concurrency_limit, [_LockType, _NewLimit, _Kill]}, _) ->
true;
postcondition(S, {call, riak_core_bg_manager, concurrency_limit, [LockType]}, Limit) ->
Limit =:= get_limit(LockType, S);
postcondition(_S, {call, riak_core_bg_manager, enable, [_LockType]}, ok) ->
true;
postcondition(_S, {call, riak_core_bg_manager, disable, [_LockType, _Kill]}, ok) ->
true;
postcondition(_S, {call, riak_core_bg_manager, enable, []}, ok) ->
true;
postcondition(_S, {call, riak_core_bg_manager, disable, []}, ok) ->
true;
postcondition(S, {call, ?MODULE, get_lock, [LockType, _Pid, _Metadata]}, max_concurrency) ->
Limit = get_limit(LockType, S),
ExistingCount = get_lock_count(LockType, S),
TooMany = ExistingCount >= Limit,
io:format("EXISTING COUNT: ~p LIMIT: ~p~n", [ExistingCount, Limit]),
not is_enabled(LockType, S) orelse TooMany;
postcondition(S, {call, ?MODULE, get_lock, [LockType, _Pid, _Metadata]}, _LockRef) ->
io:format("GOT LOCK~n"),
Limit = get_limit(LockType, S),
ExistingCount = get_lock_count(LockType, S),
WithinLimit = ExistingCount < Limit,
Enabled = is_enabled(LockType, S),
Enabled andalso WithinLimit;
postcondition(_S=#state{locks=Locks, running_procs=_Running, limit_killed=LimitKilled},
{call, riak_core_bg_manager, all_locks, []},
Results) ->
AllLocks = lists:flatmap(fun({LockType, Ls}) -> [{LockType, L} || L <- Ls] end,
Locks),
%% For every lock in the model (what we think we have), ensure its in the returned list
%% with the appropriate information. If its not, then we should have killed the process
%% (its no longer in the running list). We don't check that processes that holds the lock
%% is still running because it may be dead but the monitor message may be in the bg_managers
%% message queue
LocksOk = lists:all(fun({LockType, {Ref, Pid, Meta, Status}}) ->
case lists:keyfind(Ref, 3, Results) of
{LockType, Pid, Ref, Meta} -> true;
_ -> Status =:= inactive orelse
lists:member(Pid, lists:flatten(LimitKilled))
end
end, AllLocks),
io:format("ALL LOCKS: ~p RESULTS: ~p~n", [AllLocks, Results]),
%% we may have more locks (because we account for dead processes lazily but the lock
%% manager should never return more
LengthOk = length(AllLocks) >= length(Results),
LengthOk andalso LocksOk.
-spec prop_bg_manager_locks() -> eqc:property().
prop_bg_manager_locks() ->
?FORALL(Cmds, commands(?MODULE),
?TRAPEXIT(
aggregate(command_names(Cmds),
begin
setup(),
{H, S, Res} = run_commands(?MODULE,Cmds),
teardown(S#state.running_procs),
pretty_commands(?MODULE, Cmds, {H, S, Res},
Res == ok)
end))).
prop_bg_manager_locks_para() ->
?FORALL(Repetitions, ?SHRINK(1,[10]),
?FORALL(Cmds, parallel_commands(?MODULE),
?ALWAYS(Repetitions,
?TRAPEXIT(
begin
setup(),
{_H, _S, Res} = run_parallel_commands(?MODULE,Cmds),
teardown([]),
Res == ok
end)))).
locks_para_test_() ->
{inparallel,
[{spawn,
[{setup,
fun() -> ok end,
fun(_) -> ok end,
[
%% Run the quickcheck tests
{timeout, 60000, % timeout is in msec
%% Indicate the number of test iterations for each property here
?_assertEqual(true, run_eqc_para())
}]}]}]}.
%%%===================================================================
%%% Module commands
%%%===================================================================
get_lock(LockType, Pid, Metadata) ->
case riak_core_bg_manager:get_lock(LockType, Pid, Metadata) of
{ok, Ref} -> Ref;
max_concurrency -> max_concurrency
end.
%% starts a process we use as a placeholder for grabbing a lock.
%% (locks are grabbed on the processes behalf)
start_process() ->
Pid = spawn(fun() ->
receive die -> done
%% protection against leaking too many processes since its
%% its a PITA to teardown properly w/ run_parallel_commands
after 360000 -> timeout
end
end),
Pid.
stop_process(Pid) ->
Pid ! die,
wait_for_pid(Pid).
set_concurrency_limit(LockType, Limit, Kill) ->
{_, KilledPids} = riak_core_bg_manager:set_concurrency_limit(LockType, Limit, Kill),
KilledPids.
create_lock(LockType) ->
riak_core_bg_manager:set_concurrency_limit(LockType, ?STARTING_LIMIT, false).
%%%===================================================================
%%% Internal functions
%%%===================================================================
get_limit(LockType, #state{limits=Limits}) ->
case lists:keyfind(LockType, 1, Limits) of
false -> 0; %% default from lock manager
{LockType, Limit} -> Limit
end.
get_lock_info(LockType, #state{locks=Locks}) ->
case lists:keyfind(LockType, 1, Locks) of
false -> [];
{LockType, Ls} -> Ls
end.
get_lock_count(LockType, S=#state{running_procs=Running,limit_killed=LimitKilled}) ->
ValidLocks = [{Ref, Pid, Meta} || {Ref, Pid, Meta, active} <- get_lock_info(LockType, S),
lists:member(Pid, Running) andalso
not lists:member(Pid, lists:flatten(LimitKilled))],
length(ValidLocks).
is_enabled(LockType, #state{disabled=Disabled, global_enable=GlobalEnable}) ->
GlobalEnable andalso not ordsets:is_element(LockType, Disabled).
mark_inactive(Held) ->
lists:unzip([{Pid, {Ref, Pid, Meta, inactive}} || {Ref, Pid, Meta, _} <- Held]).
mark_inactive(Held, KilledPids) ->
[{Ref, Pid, Meta, new_status(Status, Pid, KilledPids)} || {Ref, Pid, Meta, Status} <- Held].
new_status(inactive, _, _) ->
inactive;
new_status(active, Pid, KilledPids) ->
case lists:member(Pid, KilledPids) of
true -> inactive;
false -> active
end.
setup() ->
teardown([]),
riak_core_bg_manager:start_link().
teardown(Created) ->
stop_pid(whereis(riak_core_bg_manager)),
[stop_pid(Pid) || Pid <- Created].
stop_pid(Other) when not is_pid(Other) ->
ok;
stop_pid(Pid) ->
unlink(Pid),
exit(Pid, shutdown),
ok = wait_for_pid(Pid).
wait_for_pid(Pid) ->
Mref = erlang:monitor(process, Pid),
receive
{'DOWN', Mref, process, _, _} ->
ok
after
5000 ->
{error, didnotexit}
end.
-endif.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment