|
| 1 | +-module(hashtree_eqc). |
| 2 | +-compile([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 | +-define(QC_OUT(P), |
| 9 | + eqc:on_output(fun(Str, Args) -> io:format(user, Str, Args) end, P)). |
| 10 | + |
| 11 | +-include_lib("eunit/include/eunit.hrl"). |
| 12 | + |
| 13 | +hashtree_test_() -> |
| 14 | + {timeout, 30, |
| 15 | + fun() -> |
| 16 | + ?assert(eqc:quickcheck(?QC_OUT(eqc:testing_time(29, |
| 17 | + hashtree_eqc:prop_correct())))) |
| 18 | + end |
| 19 | + }. |
| 20 | + |
| 21 | +-record(state, |
| 22 | + { |
| 23 | + tree1, |
| 24 | + tree2, |
| 25 | + only1 = [], |
| 26 | + only2 = [], |
| 27 | + both = [], |
| 28 | + segments, |
| 29 | + width, |
| 30 | + mem_levels |
| 31 | + }). |
| 32 | + |
| 33 | + |
| 34 | +initial_state() -> |
| 35 | + #state{ |
| 36 | + only1 = [], |
| 37 | + only2 = [], |
| 38 | + both = [] |
| 39 | + }. |
| 40 | + |
| 41 | +integer_to_binary(Int) -> |
| 42 | + list_to_binary(integer_to_list(Int)). |
| 43 | + |
| 44 | +-ifndef(old_hash). |
| 45 | +sha(Bin) -> |
| 46 | + crypto:hash(sha, Bin). |
| 47 | +-else. |
| 48 | +sha(Bin) -> |
| 49 | + crypto:sha(Bin). |
| 50 | +-endif. |
| 51 | + |
| 52 | +object(_S) -> |
| 53 | + {?LET(Key, int(), ?MODULE:integer_to_binary(Key)), sha(term_to_binary(make_ref()))}. |
| 54 | + |
| 55 | +command(S) -> |
| 56 | + oneof( |
| 57 | + [{call, ?MODULE, start_1, [S]} || S#state.tree1 == undefined] ++ |
| 58 | + [{call, ?MODULE, start_2, [S]} || S#state.tree2 == undefined] ++ |
| 59 | + [{call, ?MODULE, write_1, [S#state.tree1, object(S)]} || |
| 60 | + S#state.tree1 /= undefined] ++ |
| 61 | + [{call, ?MODULE, write_2, [S#state.tree2, object(S)]} || |
| 62 | + S#state.tree2 /= undefined] ++ |
| 63 | + [{call, ?MODULE, write_both, [S#state.tree1, S#state.tree2, object(S)]} || |
| 64 | + S#state.tree1 /= undefined, S#state.tree2 /= undefined] ++ |
| 65 | + [{call, ?MODULE, update_tree_1, [S#state.tree1]} || S#state.tree1 /= undefined] ++ |
| 66 | + [{call, ?MODULE, update_tree_2, [S#state.tree2]} || S#state.tree2 /= undefined] ++ |
| 67 | + [{call, ?MODULE, reconcile, [S]} || |
| 68 | + S#state.tree1 /= undefined, S#state.tree2 /= undefined] ++ |
| 69 | + [] |
| 70 | + ). |
| 71 | + |
| 72 | +make_treevars() -> |
| 73 | + Powers = [8, 16, 32, 64, 128, 256, 512, 1024], |
| 74 | + Segments=oneof(Powers), |
| 75 | + Width=oneof(Powers), |
| 76 | + %NumLevels = erlang:trunc(math:log(Segments) / math:log(Width)) + 1, |
| 77 | + %MemLevels = random:uniform(NumLevels+1)-1, |
| 78 | + %MemLevels = oneof(lists:seq(0, NumLevels), |
| 79 | + MemLevels=4, |
| 80 | + {{call, erlang, '*', [Segments, Segments]}, Width, MemLevels}. |
| 81 | + %{1024*1024, 1024, 4}. |
| 82 | + |
| 83 | +start_1(S) -> |
| 84 | + hashtree:new({0,0}, [{segments, S#state.segments}, {width, |
| 85 | + S#state.width}, {mem_levels, S#state.mem_levels}]). |
| 86 | +start_2(S) -> |
| 87 | + hashtree:new({0,0}, [{segments, S#state.segments}, {width, |
| 88 | + S#state.width}, {mem_levels, S#state.mem_levels}]). |
| 89 | + |
| 90 | +write_1(Tree, {Key, Hash}) -> |
| 91 | + hashtree:insert(Key, Hash, Tree). |
| 92 | + |
| 93 | +write_2(Tree, {Key, Hash}) -> |
| 94 | + hashtree:insert(Key, Hash, Tree). |
| 95 | + |
| 96 | +write_both(Tree1, Tree2, {Key, Hash}) -> |
| 97 | + {hashtree:insert(Key, Hash, Tree1), hashtree:insert(Key, Hash, Tree2)}. |
| 98 | + |
| 99 | +update_tree_1(T1) -> |
| 100 | + hashtree:update_tree(T1). |
| 101 | + |
| 102 | +update_tree_2(T2) -> |
| 103 | + hashtree:update_tree(T2). |
| 104 | + |
| 105 | +reconcile(S) -> |
| 106 | + A2 = hashtree:update_tree(S#state.tree1), |
| 107 | + B2 = hashtree:update_tree(S#state.tree2), |
| 108 | + KeyDiff = hashtree:local_compare(A2, B2), |
| 109 | + Missing = [M || {missing, M} <- KeyDiff], |
| 110 | + RemoteMissing = [M || {remote_missing, M} <- KeyDiff], |
| 111 | + Different = [D || {different, D} <- KeyDiff], |
| 112 | + |
| 113 | + Insert = fun(Tree, Vals) -> |
| 114 | + lists:foldl(fun({Key, Hash}, Acc) -> |
| 115 | + hashtree:insert(Key, Hash, Acc) |
| 116 | + end, Tree, Vals) |
| 117 | + end, |
| 118 | + |
| 119 | + A3 = Insert(A2, [lists:keyfind(K, 1, S#state.only2) || K <- Missing, lists:keyfind(K, 1, |
| 120 | + S#state.only2) /= false]), |
| 121 | + B3 = Insert(B2, [lists:keyfind(K, 1, S#state.only1) || K <- RemoteMissing, lists:keyfind(K, 1, |
| 122 | + S#state.only1) /= false]), |
| 123 | + B4 = Insert(B3, [lists:keyfind(K, 1, S#state.only1) || K <- Different, lists:keyfind(K, 1, |
| 124 | + S#state.only1) /= false]), |
| 125 | + Res = {hashtree:update_tree(A3), hashtree:update_tree(B4)}, |
| 126 | + Res. |
| 127 | + |
| 128 | + |
| 129 | +write_differing(Tree1, Tree2, {Key, Hash1}, Hash2) -> |
| 130 | + {{Key, Hash1}, {Key, Hash2}, hashtree:insert(Key, Hash1, Tree1), |
| 131 | + hashtree:insert(Key, Hash2, Tree2)}. |
| 132 | + |
| 133 | +precondition(S,{call,_,start_1,_}) -> |
| 134 | + S#state.tree1 == undefined; |
| 135 | +precondition(S,{call,_,start_2,_}) -> |
| 136 | + S#state.tree2 == undefined; |
| 137 | +precondition(S,{call,_,write_1,_}) -> |
| 138 | + S#state.tree1 /= undefined; |
| 139 | +precondition(S,{call,_,write_2,_}) -> |
| 140 | + S#state.tree2 /= undefined; |
| 141 | +precondition(S,{call,_,write_both,_}) -> |
| 142 | + S#state.tree1 /= undefined andalso S#state.tree2 /= undefined; |
| 143 | +precondition(S,{call,_,reconcile,_}) -> |
| 144 | + S#state.tree1 /= undefined andalso S#state.tree2 /= undefined; |
| 145 | +precondition(S,{call,_,update_tree_1,_}) -> |
| 146 | + S#state.tree1 /= undefined; |
| 147 | +precondition(S,{call,_,update_tree_2,_}) -> |
| 148 | + S#state.tree2 /= undefined. |
| 149 | + |
| 150 | +postcondition(_S,{call,_,_,_},_R) -> |
| 151 | + true. |
| 152 | + |
| 153 | +next_state(S,V,{call, _, start_1, [_]}) -> |
| 154 | + S#state{tree1=V, only1=[], both=[]}; |
| 155 | +next_state(S,V,{call, _, start_2, [_]}) -> |
| 156 | + S#state{tree2=V, only2=[], both=[]}; |
| 157 | +next_state(S,V,{call, _, write_1, [_, {Key, Val}]}) -> |
| 158 | + S#state{tree1=V, only1=[{Key, Val}|lists:keydelete(Key, 1, |
| 159 | + S#state.only1)]}; |
| 160 | +next_state(S,V,{call, _, write_2, [_, {Key, Val}]}) -> |
| 161 | + S#state{tree2=V, only2=[{Key, Val}|lists:keydelete(Key, 1, |
| 162 | + S#state.only2)]}; |
| 163 | +next_state(S,V,{call, _, update_tree_1, [_]}) -> |
| 164 | + S#state{tree1=V}; |
| 165 | +next_state(S,V,{call, _, update_tree_2, [_]}) -> |
| 166 | + S#state{tree2=V}; |
| 167 | +next_state(S,R,{call, _, write_both, [_, _, {Key, Val}]}) -> |
| 168 | + S#state{tree1={call, erlang, element, [1, R]}, |
| 169 | + tree2={call, erlang, element, [2, R]}, |
| 170 | + only1=[{Key, Val}|lists:keydelete(Key, 1, S#state.only1)], |
| 171 | + only2=[{Key, Val}|lists:keydelete(Key, 1, S#state.only2)] |
| 172 | + }; |
| 173 | +next_state(S,R,{call, _, reconcile, [_]}) -> |
| 174 | + Keys = lists:ukeymerge(1, lists:ukeysort(1, S#state.only1), |
| 175 | + lists:ukeysort(1, S#state.only2)), |
| 176 | + S#state{tree1={call, erlang, element, [1, R]}, |
| 177 | + tree2={call, erlang, element, [2, R]}, |
| 178 | + only1 = Keys, |
| 179 | + only2 = Keys |
| 180 | + }. |
| 181 | + |
| 182 | + |
| 183 | +prop_correct() -> |
| 184 | + ?FORALL({Segments, Width, MemLevels}, make_treevars(), |
| 185 | + ?FORALL(Cmds,commands(?MODULE, #state{segments=Segments, width=Width, |
| 186 | + mem_levels=MemLevels}), |
| 187 | + ?TRAPEXIT( |
| 188 | + aggregate(command_names(Cmds), |
| 189 | + begin |
| 190 | + {H,S,Res} = run_commands(?MODULE,Cmds), |
| 191 | + ?WHENFAIL( |
| 192 | + begin |
| 193 | + io:format("History: ~p\nState: ~p\nRes: ~p\n~p\n", |
| 194 | + [H,S,Res, zip(tl(Cmds), [Y || {_, Y} <- H])]), |
| 195 | + catch hashtree:destroy(hashtree:close(S#state.tree1)), |
| 196 | + catch hashtree:destroy(hashtree:close(S#state.tree2)) |
| 197 | + end, |
| 198 | + begin |
| 199 | + ?assertEqual(ok, Res), |
| 200 | + Unique1 = S#state.only1 -- S#state.only2, |
| 201 | + Unique2 = S#state.only2 -- S#state.only1, |
| 202 | + Expected = [{missing, Key} || {Key, _} <- |
| 203 | + Unique2, not |
| 204 | + lists:keymember(Key, 1, S#state.only1)] ++ |
| 205 | + [{remote_missing, Key} || {Key, _} <- |
| 206 | + Unique1, not |
| 207 | + lists:keymember(Key, 1, S#state.only2)] ++ |
| 208 | + [{different, Key} || Key <- |
| 209 | + sets:to_list(sets:intersection(sets:from_list([Key |
| 210 | + || {Key,_} <- Unique1]), |
| 211 | + sets:from_list([Key || {Key,_} |
| 212 | + <- Unique2])))], |
| 213 | + |
| 214 | + case S#state.tree1 == undefined orelse |
| 215 | + S#state.tree2 == undefined of |
| 216 | + true -> |
| 217 | + true; |
| 218 | + _ -> |
| 219 | + |
| 220 | + T1 = hashtree:update_tree(S#state.tree1), |
| 221 | + T2 = hashtree:update_tree(S#state.tree2), |
| 222 | + |
| 223 | + KeyDiff = hashtree:local_compare(T1, T2), |
| 224 | + |
| 225 | + ?assertEqual(lists:usort(Expected), |
| 226 | + lists:usort(KeyDiff)), |
| 227 | + |
| 228 | + catch hashtree:destroy(hashtree:close(T1)), |
| 229 | + catch hashtree:destroy(hashtree:close(T2)), |
| 230 | + true |
| 231 | + end |
| 232 | + end |
| 233 | + ) |
| 234 | + end)))). |
| 235 | + |
| 236 | +-endif. |
| 237 | +-endif. |
0 commit comments