Qc sync range #8
4 changed files with 134 additions and 49 deletions
3
Makefile
3
Makefile
|
@ -17,6 +17,9 @@ clean:
|
||||||
eunit: compile clean-test-btrees
|
eunit: compile clean-test-btrees
|
||||||
@$(REBAR) eunit skip_deps=true
|
@$(REBAR) eunit skip_deps=true
|
||||||
|
|
||||||
|
eunit_console:
|
||||||
|
erl -pa .eunit deps/*/ebin
|
||||||
|
|
||||||
clean-test-btrees:
|
clean-test-btrees:
|
||||||
rm -fr .eunit/Btree_* .eunit/simple
|
rm -fr .eunit/Btree_* .eunit/simple
|
||||||
|
|
||||||
|
|
|
@ -23,7 +23,9 @@ close(Ref) ->
|
||||||
gen_server:call(Ref, close)
|
gen_server:call(Ref, close)
|
||||||
catch
|
catch
|
||||||
exit:{noproc,_} -> ok;
|
exit:{noproc,_} -> ok;
|
||||||
exit:noproc -> ok
|
exit:noproc -> ok;
|
||||||
|
%% Handle the case where the monitor triggers
|
||||||
|
exit:{normal, _} -> ok
|
||||||
end.
|
end.
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -12,6 +12,7 @@
|
||||||
lookup_fail/2,
|
lookup_fail/2,
|
||||||
open/1, close/1,
|
open/1, close/1,
|
||||||
put/3,
|
put/3,
|
||||||
|
sync_range/3,
|
||||||
stop/0]).
|
stop/0]).
|
||||||
|
|
||||||
%% gen_server callbacks
|
%% gen_server callbacks
|
||||||
|
@ -49,6 +50,9 @@ close(N) ->
|
||||||
put(N, K, V) ->
|
put(N, K, V) ->
|
||||||
call({put, N, K, V}).
|
call({put, N, K, V}).
|
||||||
|
|
||||||
|
sync_range(T, LK, HK) ->
|
||||||
|
call({sync_range, T, LK, HK}).
|
||||||
|
|
||||||
stop() ->
|
stop() ->
|
||||||
call(stop).
|
call(stop).
|
||||||
|
|
||||||
|
@ -72,6 +76,12 @@ handle_call({close, N}, _, #state { btrees = D} = State) ->
|
||||||
Otherwise ->
|
Otherwise ->
|
||||||
{reply, {error, Otherwise}, State}
|
{reply, {error, Otherwise}, State}
|
||||||
end;
|
end;
|
||||||
|
handle_call({sync_range, Name, LoKey, HiKey}, _From,
|
||||||
|
#state { btrees = D} = State) ->
|
||||||
|
Tree = dict:fetch(Name, D),
|
||||||
|
{ok, Ref} = lsm_btree:sync_range(Tree, LoKey, HiKey),
|
||||||
|
Result = sync_range_gather(Ref),
|
||||||
|
{reply, Result, State};
|
||||||
handle_call({put, N, K, V}, _, #state { btrees = D} = State) ->
|
handle_call({put, N, K, V}, _, #state { btrees = D} = State) ->
|
||||||
Tree = dict:fetch(N, D),
|
Tree = dict:fetch(N, D),
|
||||||
case lsm_btree:put(Tree, K, V) of
|
case lsm_btree:put(Tree, K, V) of
|
||||||
|
@ -119,3 +129,15 @@ cleanup_trees(#state { btrees = BTs }) ->
|
||||||
BTs).
|
BTs).
|
||||||
|
|
||||||
|
|
||||||
|
sync_range_gather(Ref) ->
|
||||||
|
sync_range_gather(Ref, []).
|
||||||
|
|
||||||
|
sync_range_gather(Ref, Acc) ->
|
||||||
|
receive
|
||||||
|
{fold_result, Ref, K, V} ->
|
||||||
|
sync_range_gather(Ref, [{K, V} | Acc]);
|
||||||
|
{fold_done, Ref} ->
|
||||||
|
{ok, Acc}
|
||||||
|
after 3000 ->
|
||||||
|
{error, timeout}
|
||||||
|
end.
|
||||||
|
|
|
@ -20,6 +20,7 @@
|
||||||
next_state/3, postcondition/3,
|
next_state/3, postcondition/3,
|
||||||
precondition/2]).
|
precondition/2]).
|
||||||
|
|
||||||
|
-record(tree, { elements = dict:new() }).
|
||||||
-record(state, { open = dict:new(),
|
-record(state, { open = dict:new(),
|
||||||
closed = dict:new() }).
|
closed = dict:new() }).
|
||||||
-define(SERVER, lsm_btree_drv).
|
-define(SERVER, lsm_btree_drv).
|
||||||
|
@ -32,6 +33,8 @@ full_test_() ->
|
||||||
[
|
[
|
||||||
?_test(test_tree_simple_1()),
|
?_test(test_tree_simple_1()),
|
||||||
?_test(test_tree_simple_2()),
|
?_test(test_tree_simple_2()),
|
||||||
|
?_test(test_tree_simple_3()),
|
||||||
|
?_test(test_tree_simple_4()),
|
||||||
?_test(test_tree()),
|
?_test(test_tree()),
|
||||||
{timeout, 120, ?_test(test_qc())}
|
{timeout, 120, ?_test(test_qc())}
|
||||||
]}.
|
]}.
|
||||||
|
@ -72,16 +75,20 @@ g_open_tree(Open) ->
|
||||||
|
|
||||||
%% Pick a name of a non-empty Btree
|
%% Pick a name of a non-empty Btree
|
||||||
g_non_empty_btree(Open) ->
|
g_non_empty_btree(Open) ->
|
||||||
?LET(TreesWithKeys, dict:filter(fun(_K, D) -> dict:size(D) > 0 end, Open),
|
?LET(TreesWithKeys, dict:filter(fun(_K, #tree { elements = D}) ->
|
||||||
|
dict:size(D) > 0
|
||||||
|
end,
|
||||||
|
Open),
|
||||||
oneof(dict:fetch_keys(TreesWithKeys))).
|
oneof(dict:fetch_keys(TreesWithKeys))).
|
||||||
|
|
||||||
g_existing_key(Name, Open) ->
|
g_existing_key(Name, Open) ->
|
||||||
oneof(dict:fetch_keys(dict:fetch(Name, Open))).
|
#tree { elements = Elems } = dict:fetch(Name, Open),
|
||||||
|
oneof(dict:fetch_keys(Elems)).
|
||||||
|
|
||||||
g_non_existing_key(Name, Open) ->
|
g_non_existing_key(Name, Open) ->
|
||||||
?SUCHTHAT(Key, g_fail_key(),
|
?SUCHTHAT(Key, g_fail_key(),
|
||||||
begin
|
begin
|
||||||
D = dict:fetch(Name, Open),
|
#tree { elements = D } = dict:fetch(Name, Open),
|
||||||
not dict:is_key(Key, D)
|
not dict:is_key(Key, D)
|
||||||
end).
|
end).
|
||||||
|
|
||||||
|
@ -93,7 +100,7 @@ btree_name(I) ->
|
||||||
initial_state() ->
|
initial_state() ->
|
||||||
ClosedBTrees = lists:foldl(fun(N, Closed) ->
|
ClosedBTrees = lists:foldl(fun(N, Closed) ->
|
||||||
dict:store(btree_name(N),
|
dict:store(btree_name(N),
|
||||||
dict:new(),
|
#tree { },
|
||||||
Closed)
|
Closed)
|
||||||
end,
|
end,
|
||||||
dict:new(),
|
dict:new(),
|
||||||
|
@ -104,40 +111,42 @@ initial_state() ->
|
||||||
command(#state { open = Open, closed = Closed } = S) ->
|
command(#state { open = Open, closed = Closed } = S) ->
|
||||||
frequency(
|
frequency(
|
||||||
[ {20, {call, ?SERVER, open, [oneof(dict:fetch_keys(Closed))]}}
|
[ {20, {call, ?SERVER, open, [oneof(dict:fetch_keys(Closed))]}}
|
||||||
|| closed_dicts(S)] ++
|
|| closed_dicts(S)]
|
||||||
[ {20, {call, ?SERVER, close, [oneof(dict:fetch_keys(Open))]}}
|
++ [ {20, {call, ?SERVER, close, [oneof(dict:fetch_keys(Open))]}}
|
||||||
|| open_dicts(S)] ++
|
|| open_dicts(S)]
|
||||||
[ {2000, {call, ?SERVER, put, cmd_put_args(S)}}
|
++ [ {2000, {call, ?SERVER, put, cmd_put_args(S)}}
|
||||||
|| open_dicts(S)] ++
|
|| open_dicts(S)]
|
||||||
[ {1500, {call, ?SERVER, lookup_fail, cmd_lookup_fail_args(S)}}
|
++ [ {1500, {call, ?SERVER, lookup_fail, cmd_lookup_fail_args(S)}}
|
||||||
|| open_dicts(S)] ++
|
|| open_dicts(S)]
|
||||||
[ {1500, {call, ?SERVER, lookup_exist, cmd_lookup_args(S)}}
|
++ [ {1500, {call, ?SERVER, lookup_exist, cmd_lookup_args(S)}}
|
||||||
|| open_dicts(S), open_dicts_with_keys(S)] ++
|
|| open_dicts(S), open_dicts_with_keys(S)]
|
||||||
[ {500, {call, ?SERVER, delete_exist, cmd_delete_args(S)}}
|
++ [ {500, {call, ?SERVER, delete_exist, cmd_delete_args(S)}}
|
||||||
|| open_dicts(S), open_dicts_with_keys(S)]).
|
|| open_dicts(S), open_dicts_with_keys(S)]
|
||||||
|
++ [ {250, {call, ?SERVER, sync_range, cmd_sync_range_args(S)}}
|
||||||
|
|| open_dicts(S), open_dicts_with_keys(S)]
|
||||||
|
).
|
||||||
|
|
||||||
%% Precondition (abstract)
|
%% Precondition (abstract)
|
||||||
precondition(#state { open = _Open}, {call, ?SERVER, delete_exist,
|
precondition(S, {call, ?SERVER, sync_range, [_Tree, _K1, _K2]}) ->
|
||||||
[_Name, _K]}) ->
|
open_dicts(S) andalso open_dicts_with_keys(S);
|
||||||
%% No need to check since we limit this in the command/1 generator
|
precondition(S, {call, ?SERVER, delete_exist, [_Name, _K]}) ->
|
||||||
true;
|
open_dicts(S) andalso open_dicts_with_keys(S);
|
||||||
precondition(#state { open = _Open }, {call, ?SERVER, lookup_fail,
|
precondition(S, {call, ?SERVER, lookup_fail, [_Name, _K]}) ->
|
||||||
[_Name, _K]}) ->
|
open_dicts(S);
|
||||||
%% We can always try to look up some non-existing key
|
precondition(S, {call, ?SERVER, lookup_exist, [_Name, _K]}) ->
|
||||||
true;
|
open_dicts(S) andalso open_dicts_with_keys(S);
|
||||||
precondition(#state { open = _Open }, {call, ?SERVER, lookup_exist,
|
|
||||||
[_Name, _K]}) ->
|
|
||||||
%% No need to check since we limit this in the command/1 generator
|
|
||||||
true;
|
|
||||||
precondition(#state { open = Open }, {call, ?SERVER, put, [Name, _K, _V]}) ->
|
precondition(#state { open = Open }, {call, ?SERVER, put, [Name, _K, _V]}) ->
|
||||||
dict:is_key(Name, Open);
|
dict:is_key(Name, Open);
|
||||||
precondition(#state { open = Open, closed = Closed }, {call, ?SERVER, open, [Name]}) ->
|
precondition(#state { open = Open, closed = Closed },
|
||||||
|
{call, ?SERVER, open, [Name]}) ->
|
||||||
(not (dict:is_key(Name, Open))) and (dict:is_key(Name, Closed));
|
(not (dict:is_key(Name, Open))) and (dict:is_key(Name, Closed));
|
||||||
precondition(#state { open = Open, closed = Closed }, {call, ?SERVER, close, [Name]}) ->
|
precondition(#state { open = Open, closed = Closed },
|
||||||
|
{call, ?SERVER, close, [Name]}) ->
|
||||||
(dict:is_key(Name, Open)) and (not dict:is_key(Name, Closed)).
|
(dict:is_key(Name, Open)) and (not dict:is_key(Name, Closed)).
|
||||||
|
|
||||||
|
|
||||||
%% Next state manipulation (abstract / concrete)
|
%% Next state manipulation (abstract / concrete)
|
||||||
|
next_state(S, _Res, {call, ?SERVER, sync_range, [_Tree, _K1, _K2]}) ->
|
||||||
|
S;
|
||||||
next_state(S, _Res, {call, ?SERVER, lookup_fail, [_Name, _Key]}) ->
|
next_state(S, _Res, {call, ?SERVER, lookup_fail, [_Name, _Key]}) ->
|
||||||
S;
|
S;
|
||||||
next_state(S, _Res, {call, ?SERVER, lookup_exist, [_Name, _Key]}) ->
|
next_state(S, _Res, {call, ?SERVER, lookup_exist, [_Name, _Key]}) ->
|
||||||
|
@ -145,31 +154,42 @@ next_state(S, _Res, {call, ?SERVER, lookup_exist, [_Name, _Key]}) ->
|
||||||
next_state(#state { open = Open} = S, _Res,
|
next_state(#state { open = Open} = S, _Res,
|
||||||
{call, ?SERVER, delete_exist, [Name, Key]}) ->
|
{call, ?SERVER, delete_exist, [Name, Key]}) ->
|
||||||
S#state { open = dict:update(Name,
|
S#state { open = dict:update(Name,
|
||||||
fun(Dict) ->
|
fun(#tree { elements = Dict}) ->
|
||||||
dict:erase(Key, Dict)
|
#tree { elements =
|
||||||
|
dict:erase(Key, Dict)}
|
||||||
end,
|
end,
|
||||||
Open)};
|
Open)};
|
||||||
next_state(#state { open = Open} = S, _Res,
|
next_state(#state { open = Open} = S, _Res,
|
||||||
{call, ?SERVER, put, [Name, Key, Value]}) ->
|
{call, ?SERVER, put, [Name, Key, Value]}) ->
|
||||||
S#state { open = dict:update(Name,
|
S#state { open = dict:update(
|
||||||
fun(Dict) ->
|
Name,
|
||||||
dict:store(Key, Value, Dict)
|
fun(#tree { elements = Dict}) ->
|
||||||
|
#tree { elements =
|
||||||
|
dict:store(Key, Value, Dict) }
|
||||||
end,
|
end,
|
||||||
Open)};
|
Open)};
|
||||||
next_state(#state { open = Open, closed=Closed} = S, _Res, {call, ?SERVER, open, [Name]}) ->
|
next_state(#state { open = Open, closed=Closed} = S,
|
||||||
|
_Res, {call, ?SERVER, open, [Name]}) ->
|
||||||
S#state { open = dict:store(Name, dict:fetch(Name, Closed) , Open),
|
S#state { open = dict:store(Name, dict:fetch(Name, Closed) , Open),
|
||||||
closed = dict:erase(Name, Closed) };
|
closed = dict:erase(Name, Closed) };
|
||||||
next_state(#state { open = Open, closed=Closed} = S, _Res, {call, ?SERVER, close, [Name]}) ->
|
next_state(#state { open = Open, closed=Closed} = S, _Res,
|
||||||
|
{call, ?SERVER, close, [Name]}) ->
|
||||||
S#state { closed = dict:store(Name, dict:fetch(Name, Open) , Closed),
|
S#state { closed = dict:store(Name, dict:fetch(Name, Open) , Closed),
|
||||||
open = dict:erase(Name, Open) }.
|
open = dict:erase(Name, Open) }.
|
||||||
|
|
||||||
%% Postcondition check (concrete)
|
%% Postcondition check (concrete)
|
||||||
|
postcondition(#state { open = Open},
|
||||||
|
{call, ?SERVER, sync_range, [Tree, K1, K2]}, {ok, Result}) ->
|
||||||
|
#tree { elements = TDict } = dict:fetch(Tree, Open),
|
||||||
|
lists:sort(dict_range_query(TDict, K1, K2))
|
||||||
|
== lists:sort(Result);
|
||||||
postcondition(_S,
|
postcondition(_S,
|
||||||
{call, ?SERVER, lookup_fail, [_Name, _Key]}, notfound) ->
|
{call, ?SERVER, lookup_fail, [_Name, _Key]}, notfound) ->
|
||||||
true;
|
true;
|
||||||
postcondition(#state { open = Open },
|
postcondition(#state { open = Open },
|
||||||
{call, ?SERVER, lookup_exist, [Name, Key]}, {ok, Value}) ->
|
{call, ?SERVER, lookup_exist, [Name, Key]}, {ok, Value}) ->
|
||||||
dict:fetch(Key, dict:fetch(Name, Open)) == Value;
|
#tree { elements = Elems } = dict:fetch(Name, Open),
|
||||||
|
dict:fetch(Key, Elems) == Value;
|
||||||
postcondition(_S, {call, ?SERVER, delete_exist, [_Name, _Key]}, ok) ->
|
postcondition(_S, {call, ?SERVER, delete_exist, [_Name, _Key]}, ok) ->
|
||||||
true;
|
true;
|
||||||
postcondition(_S, {call, ?SERVER, put, [_Name, _Key, _Value]}, ok) ->
|
postcondition(_S, {call, ?SERVER, put, [_Name, _Key, _Value]}, ok) ->
|
||||||
|
@ -211,8 +231,28 @@ test_tree_simple_2() ->
|
||||||
ok = lsm_btree:delete(Tree, <<"ã">>),
|
ok = lsm_btree:delete(Tree, <<"ã">>),
|
||||||
ok = lsm_btree:close(Tree).
|
ok = lsm_btree:close(Tree).
|
||||||
|
|
||||||
test_tree() ->
|
test_tree_simple_3() ->
|
||||||
|
{ok, Tree} = lsm_btree:open("simple"),
|
||||||
|
ok = lsm_btree:put(Tree, <<"X">>, <<"Y">>),
|
||||||
|
{ok, Ref} = lsm_btree:sync_range(Tree, <<"X">>, <<"X">>),
|
||||||
|
?assertEqual(ok,
|
||||||
|
receive
|
||||||
|
{fold_done, Ref} -> ok
|
||||||
|
after 1000 -> {error, timeout}
|
||||||
|
end),
|
||||||
|
ok = lsm_btree:close(Tree).
|
||||||
|
|
||||||
|
test_tree_simple_4() ->
|
||||||
|
Key = <<56,11,62,42,35,163,16,100,9,224,8,228,130,94,198,2,126,117,243,
|
||||||
|
1,122,175,79,159,212,177,30,153,71,91,85,233,41,199,190,58,3,
|
||||||
|
173,220,9>>,
|
||||||
|
Value = <<212,167,12,6,105,152,17,80,243>>,
|
||||||
|
{ok, Tree} = lsm_btree:open("simple"),
|
||||||
|
ok = lsm_btree:put(Tree, Key, Value),
|
||||||
|
?assertEqual({ok, Value}, lsm_btree:lookup(Tree, Key)),
|
||||||
|
ok = lsm_btree:close(Tree).
|
||||||
|
|
||||||
|
test_tree() ->
|
||||||
application:start(sasl),
|
application:start(sasl),
|
||||||
|
|
||||||
{ok, Tree} = lsm_btree:open("simple2"),
|
{ok, Tree} = lsm_btree:open("simple2"),
|
||||||
|
@ -289,22 +329,35 @@ cmd_delete_args(#state { open = Open}) ->
|
||||||
?LET(Key, g_existing_key(Name, Open),
|
?LET(Key, g_existing_key(Name, Open),
|
||||||
[Name, Key])).
|
[Name, Key])).
|
||||||
|
|
||||||
|
cmd_sync_range_args(#state { open = Open }) ->
|
||||||
|
?LET(Tree, g_non_empty_btree(Open),
|
||||||
|
?LET({K1, K2}, {g_existing_key(Tree, Open),
|
||||||
|
g_existing_key(Tree, Open)},
|
||||||
|
[Tree, K1, K2])).
|
||||||
|
|
||||||
%% Context management
|
%% Context management
|
||||||
%% ----------------------------------------------------------------------
|
%% ----------------------------------------------------------------------
|
||||||
cleanup_test_trees(#state { open = Open}) ->
|
cleanup_test_trees(#state { open = Open, closed = Closed }) ->
|
||||||
[cleanup_tree(N) || N <- dict:fetch_keys(Open)].
|
[cleanup_tree(N) || N <- dict:fetch_keys(Open)],
|
||||||
|
[cleanup_tree(N) || N <- dict:fetch_keys(Closed)].
|
||||||
|
|
||||||
cleanup_tree(Tree) ->
|
cleanup_tree(Tree) ->
|
||||||
{ok, FileNames} = file:list_dir(Tree),
|
case file:list_dir(Tree) of
|
||||||
[ok = file:delete(filename:join([Tree, Fname])) || Fname <- FileNames],
|
{error, enoent} ->
|
||||||
file:del_dir(Tree).
|
ok;
|
||||||
|
{ok, FileNames} ->
|
||||||
|
[ok = file:delete(filename:join([Tree, Fname]))
|
||||||
|
|| Fname <- FileNames],
|
||||||
|
file:del_dir(Tree)
|
||||||
|
end.
|
||||||
|
|
||||||
%% Various Helper routines
|
%% Various Helper routines
|
||||||
%% ----------------------------------------------------------------------
|
%% ----------------------------------------------------------------------
|
||||||
|
|
||||||
open_dicts_with_keys(#state { open = Open}) ->
|
open_dicts_with_keys(#state { open = Open}) ->
|
||||||
lists:any(fun({_, D}) -> dict:size(D) > 0 end,
|
lists:any(fun({_, #tree { elements = D}}) ->
|
||||||
|
dict:size(D) > 0
|
||||||
|
end,
|
||||||
dict:to_list(Open)).
|
dict:to_list(Open)).
|
||||||
|
|
||||||
open_dicts(#state { open = Open}) ->
|
open_dicts(#state { open = Open}) ->
|
||||||
|
@ -313,4 +366,9 @@ open_dicts(#state { open = Open}) ->
|
||||||
closed_dicts(#state { closed = Closed}) ->
|
closed_dicts(#state { closed = Closed}) ->
|
||||||
dict:size(Closed) > 0.
|
dict:size(Closed) > 0.
|
||||||
|
|
||||||
|
dict_range_query(Dict, LowKey, HighKey) ->
|
||||||
|
[{K, V} || {K, V} <- dict:to_list(Dict),
|
||||||
|
K >= LowKey,
|
||||||
|
K < HighKey].
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue