prop_emqx_ft_assembly.erl 7.9 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233
  1. %%--------------------------------------------------------------------
  2. %% Copyright (c) 2020-2024 EMQ Technologies Co., Ltd. All Rights Reserved.
  3. %%
  4. %% Licensed under the Apache License, Version 2.0 (the "License");
  5. %% you may not use this file except in compliance with the License.
  6. %% You may obtain a copy of the License at
  7. %%
  8. %% http://www.apache.org/licenses/LICENSE-2.0
  9. %%
  10. %% Unless required by applicable law or agreed to in writing, software
  11. %% distributed under the License is distributed on an "AS IS" BASIS,
  12. %% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  13. %% See the License for the specific language governing permissions and
  14. %% limitations under the License.
  15. %%--------------------------------------------------------------------
  16. -module(prop_emqx_ft_assembly).
  17. -include_lib("proper/include/proper.hrl").
  18. -import(emqx_proper_types, [scaled/2, fixedmap/1, typegen/0, generate/2]).
  19. -define(COVERAGE_TIMEOUT, 10000).
  20. prop_coverage() ->
  21. ?FORALL(
  22. #{filesize := Filesize, segsizes := Segsizes, typegen := TypeGen},
  23. noshrink(
  24. fixedmap(#{
  25. filesize => filesize_t(),
  26. segsizes => segsizes_t(),
  27. typegen => typegen()
  28. })
  29. ),
  30. ?TIMEOUT(
  31. ?COVERAGE_TIMEOUT,
  32. begin
  33. Segments = generate(segments_t(Filesize, Segsizes), TypeGen),
  34. ASM1 = append_segments(mk_assembly(Filesize), Segments),
  35. {Time, ASM2} = timer:tc(emqx_ft_assembly, update, [ASM1]),
  36. measure(
  37. #{"Segments" => length(Segments), "Time" => Time},
  38. case emqx_ft_assembly:status(ASM2) of
  39. complete ->
  40. Coverage = emqx_ft_assembly:coverage(ASM2),
  41. measure(
  42. #{"CoverageLength" => length(Coverage)},
  43. is_coverage_complete(Coverage)
  44. );
  45. {incomplete, {missing, {segment, _, _}}} ->
  46. measure("CoverageLength", 0, true)
  47. end
  48. )
  49. end
  50. )
  51. ).
  52. prop_coverage_likely_incomplete() ->
  53. ?FORALL(
  54. #{filesize := Filesize, segsizes := Segsizes, hole := HoleIn, typegen := TypeGen},
  55. noshrink(
  56. fixedmap(#{
  57. filesize => filesize_t(),
  58. segsizes => segsizes_t(),
  59. hole => filesize_t(),
  60. typegen => typegen()
  61. })
  62. ),
  63. ?TIMEOUT(?COVERAGE_TIMEOUT, begin
  64. Hole = HoleIn rem max(Filesize, 1),
  65. Segments = generate(segments_t(Filesize, Segsizes, Hole), TypeGen),
  66. ASM1 = append_segments(mk_assembly(Filesize), Segments),
  67. {Time, ASM2} = timer:tc(emqx_ft_assembly, update, [ASM1]),
  68. measure(
  69. #{"Segments" => length(Segments), "Time" => Time},
  70. case emqx_ft_assembly:status(ASM2) of
  71. complete ->
  72. % NOTE: this is still possible due to the nature of `SUCHTHATMAYBE`
  73. IsComplete = emqx_ft_assembly:coverage(ASM2),
  74. collect(complete, is_coverage_complete(IsComplete));
  75. {incomplete, {missing, {segment, _, _}}} ->
  76. collect(incomplete, true)
  77. end
  78. )
  79. end)
  80. ).
  81. prop_coverage_complete() ->
  82. ?FORALL(
  83. #{filesize := Filesize, segsizes := Segsizes, node := RemoteNode, typegen := TypeGen},
  84. noshrink(
  85. fixedmap(#{
  86. filesize => filesize_t(),
  87. segsizes => ?SUCHTHAT([BaseSegsize | _], segsizes_t(), BaseSegsize > 0),
  88. node => remote_node_t(),
  89. typegen => typegen()
  90. })
  91. ),
  92. ?TIMEOUT(
  93. ?COVERAGE_TIMEOUT,
  94. begin
  95. % Ensure that we have complete coverage
  96. Segments = generate(segments_t(Filesize, Segsizes), TypeGen),
  97. ASM1 = mk_assembly(Filesize),
  98. ASM2 = append_coverage(ASM1, RemoteNode, Filesize, Segsizes),
  99. ASM3 = append_segments(ASM2, Segments),
  100. {Time, ASM4} = timer:tc(emqx_ft_assembly, update, [ASM3]),
  101. measure(
  102. #{"CoverageMax" => nsegs(Filesize, Segsizes), "Time" => Time},
  103. case emqx_ft_assembly:status(ASM4) of
  104. complete ->
  105. Coverage = emqx_ft_assembly:coverage(ASM4),
  106. measure(
  107. #{"Coverage" => length(Coverage)},
  108. is_coverage_complete(Coverage)
  109. );
  110. {incomplete, _} ->
  111. false
  112. end
  113. )
  114. end
  115. )
  116. ).
  117. measure(NamedSamples, Test) ->
  118. maps:fold(fun(Name, Sample, Acc) -> measure(Name, Sample, Acc) end, Test, NamedSamples).
  119. is_coverage_complete([]) ->
  120. true;
  121. is_coverage_complete(Coverage = [_ | Tail]) ->
  122. is_coverage_complete(Coverage, Tail).
  123. is_coverage_complete([_], []) ->
  124. true;
  125. is_coverage_complete(
  126. [{_Node1, #{fragment := {segment, #{offset := O1, size := S1}}}} | Rest],
  127. [{_Node2, #{fragment := {segment, #{offset := O2}}}} | Tail]
  128. ) ->
  129. (O1 + S1 == O2) andalso is_coverage_complete(Rest, Tail).
  130. mk_assembly(Filesize) ->
  131. emqx_ft_assembly:append(emqx_ft_assembly:new(Filesize), node(), mk_filemeta(Filesize)).
  132. append_segments(ASMIn, Fragments) ->
  133. lists:foldl(
  134. fun({Node, {Offset, Size}}, ASM) ->
  135. emqx_ft_assembly:append(ASM, Node, mk_segment(Offset, Size))
  136. end,
  137. ASMIn,
  138. Fragments
  139. ).
  140. append_coverage(ASM, Node, Filesize, Segsizes = [BaseSegsize | _]) ->
  141. append_coverage(ASM, Node, Filesize, BaseSegsize, 0, nsegs(Filesize, Segsizes)).
  142. append_coverage(ASM, Node, Filesize, Segsize, I, NSegs) when I < NSegs ->
  143. Offset = I * Segsize,
  144. Size = min(Segsize, Filesize - Offset),
  145. ASMNext = emqx_ft_assembly:append(ASM, Node, mk_segment(Offset, Size)),
  146. append_coverage(ASMNext, Node, Filesize, Segsize, I + 1, NSegs);
  147. append_coverage(ASM, _Node, _Filesize, _Segsize, _, _NSegs) ->
  148. ASM.
  149. mk_filemeta(Filesize) ->
  150. #{
  151. path => "MANIFEST.json",
  152. fragment => {filemeta, #{name => ?MODULE_STRING, size => Filesize}}
  153. }.
  154. mk_segment(Offset, Size) ->
  155. #{
  156. path => "SEG" ++ integer_to_list(Offset) ++ integer_to_list(Size),
  157. fragment => {segment, #{offset => Offset, size => Size}}
  158. }.
  159. nsegs(Filesize, [BaseSegsize | _]) ->
  160. Filesize div max(1, BaseSegsize) + 1.
  161. segments_t(Filesize, Segsizes) ->
  162. scaled(nsegs(Filesize, Segsizes), list({node_t(), segment_t(Filesize, Segsizes)})).
  163. segments_t(Filesize, Segsizes, Hole) ->
  164. scaled(nsegs(Filesize, Segsizes), list({node_t(), segment_t(Filesize, Segsizes, Hole)})).
  165. segment_t(Filesize, Segsizes, Hole) ->
  166. ?SUCHTHATMAYBE(
  167. {Offset, Size},
  168. segment_t(Filesize, Segsizes),
  169. Hole =< Offset orelse Hole > (Offset + Size)
  170. ).
  171. segment_t(Filesize, Segsizes) ->
  172. ?LET(
  173. Segsize,
  174. oneof(Segsizes),
  175. ?LET(
  176. Index,
  177. range(0, Filesize div max(1, Segsize)),
  178. {Index * Segsize, min(Segsize, Filesize - (Index * Segsize))}
  179. )
  180. ).
  181. filesize_t() ->
  182. scaled(2000, non_neg_integer()).
  183. segsizes_t() ->
  184. ?LET(
  185. BaseSize,
  186. segsize_t(),
  187. oneof([
  188. [BaseSize, BaseSize * 2],
  189. [BaseSize, BaseSize * 2, BaseSize * 3],
  190. [BaseSize, BaseSize * 2, BaseSize * 5]
  191. ])
  192. ).
  193. segsize_t() ->
  194. scaled(50, non_neg_integer()).
  195. remote_node_t() ->
  196. oneof([
  197. 'emqx42@emqx.local',
  198. 'emqx43@emqx.local',
  199. 'emqx44@emqx.local'
  200. ]).
  201. node_t() ->
  202. oneof([
  203. node(),
  204. 'emqx42@emqx.local',
  205. 'emqx43@emqx.local',
  206. 'emqx44@emqx.local'
  207. ]).