Just in case commit: WIP
This commit is contained in:
Scott Lystig Fritchie
parent
58ced8d14c
commit
25bf64a03c
1 changed files with 67 additions and 20 deletions
|
|
@ -202,14 +202,24 @@ prop_pulse_test_() ->
|
|||
%% {44522,{result,<0.467.0>,{ok,1}}},
|
||||
%% {47651,{result,<0.466.0>,{ok,2}}}]
|
||||
|
||||
check_trace(Trace, _Cmds, _Seed) ->
|
||||
check_trace(Trace0, _Cmds, _Seed) ->
|
||||
%% Let's treat this thing like a KV store. It is, mostly.
|
||||
%% Key = LPN, Value = error_unwritten | {ok, Blob} | error_trimmed
|
||||
%%
|
||||
%% Problem: At {call, Pid, ...} time, we don't know what Key is!
|
||||
%% We find out at {return, Pid, {ok, LSN}} time.
|
||||
%% Also, the append might fail, so the model can ignore those
|
||||
%% failures because they're not mutating any state that and
|
||||
%% external viewer can see.
|
||||
Trace = add_LPN_to_append_calls(Trace0),
|
||||
|
||||
Events = eqc_temporal:from_timed_list(Trace),
|
||||
%% Example Events, temporal style, 1 usec resolution, same as original trace
|
||||
%%
|
||||
%% [{0,32014,[]},
|
||||
%% {32014,32015,[{call,<0.467.0>,{append,<<"O">>}}]},
|
||||
%% {32014,32015,[{call,<0.467.0>,{append,<<"O">>,will_be,1}}]},
|
||||
%% {32015,32421,[]},
|
||||
%% {32421,32422,[{call,<0.466.0>,{append,<<134>>}}]},
|
||||
%% {32421,32422,[{call,<0.466.0>,{append,<<134>>,will_be,2}}]},
|
||||
%% {32422,44522,[]},
|
||||
%% {44522,44523,[{result,<0.467.0>,{ok,...}}]},
|
||||
%% {44523,47651,[]},
|
||||
|
|
@ -223,27 +233,44 @@ check_trace(Trace, _Cmds, _Seed) ->
|
|||
%% Example Calls (temporal map of when a call is in progress)
|
||||
%%
|
||||
%% [{0,32014,[]},
|
||||
%% {32014,32421,[{call,<0.467.0>,{append,<<"O">>}}]},
|
||||
%% {32014,32421,[{call,<0.467.0>,{append,<<"O">>,will_be,1}}]},
|
||||
%% {32421,44522,
|
||||
%% [{call,<0.466.0>,{append,<<134>>}},{call,<0.467.0>,{append,<<"O">>}}]},
|
||||
%% {44522,47651,[{call,<0.466.0>,{append,<<134>>}}]},
|
||||
%% [{call,<0.466.0>,{append,<<134>>,will_be,2}},{call,<0.467.0>,{append,<<"O">>,will_be,1}}]},
|
||||
%% {44522,47651,[{call,<0.466.0>,{append,<<134>>,will_be,2}}]},
|
||||
%% {47651,infinity,[]}]
|
||||
|
||||
AppendResultFilter = fun({ok, LPN}) -> LPN;
|
||||
(Else) -> Else end,
|
||||
AppendResults = eqc_temporal:stateful(
|
||||
fun({call, Pid, Call}) -> [{call, Pid, Call}] end,
|
||||
fun({call, Pid, {append, _Pg}}, {result, Pid, Res}) ->
|
||||
[AppendResultFilter(Res)] end,
|
||||
%% Remember: Appends contains only successful append ops!
|
||||
Appends = eqc_temporal:stateful(
|
||||
fun({call, Pid, {append, Pg, will_be, LPN}}) ->
|
||||
{status, LPN, Pid, Pg}
|
||||
end,
|
||||
fun({status, LPN, Pid, Pg}, {result, Pid, {ok, LPN}})->
|
||||
[{status, LPN, x, Pg}]
|
||||
end,
|
||||
Events),
|
||||
{_, infinity, AppendLPNs} = lists:last(eqc_temporal:all_future(AppendResults)),
|
||||
if length(Appends) < 10 -> io:format("Trace ~p\n", [Trace]), io:format("Events ~p\n", [Events]), io:format("Appends ~p\n", [Appends]); true -> ok end,
|
||||
%% The last item in the relation tells us what the last/infinite future
|
||||
%% state of each LPN is. We'll use it to identify all successfully
|
||||
%% written LPNs and other stuff.
|
||||
{_, infinity, FinalStatus} = lists:last(eqc_temporal:all_future(Appends)),
|
||||
|
||||
|
||||
InitialVals = eqc_temporal:elems(eqc_temporal:ret([{status, LPN, x, error_unwritten} || {status, LPN, _, _} <- FinalStatus])),
|
||||
Vals = eqc_temporal:union(InitialVals, Appends),
|
||||
|
||||
Values = eqc_temporal:stateful(
|
||||
fun({status, _LPN, Pid, _Pg} = I) when is_pid(Pid) -> I end,
|
||||
fun({status, LPN, Pid, Pg}, {status, LPN, x, Pg})
|
||||
when is_pid(Pid) -> [] end,
|
||||
Vals),
|
||||
if length(Appends) < 10 -> io:format(user, "Values ~P\n", [Values, 100]); true -> ok end,
|
||||
|
||||
%% Desired properties
|
||||
AllCallsFinish = eqc_temporal:is_false(eqc_temporal:all_future(Calls)),
|
||||
NoAppendLPNDups = lists:sort(AppendLPNs) == lists:usort(AppendLPNs),
|
||||
NoAppendLPNDups = true, %%% QQQ TODO!!!!!!!! lists:sort(AppendLPNs) == lists:usort(AppendLPNs),
|
||||
|
||||
?WHENFAIL(begin
|
||||
?QC_FMT("*AppendLPNs: ~p\n", [range_ify(AppendLPNs)])
|
||||
?QC_FMT("*AppendLPNs: ~p\n", [todoTODO]) %%%%% [range_ify(AppendLPNs)])
|
||||
end,
|
||||
conjunction(
|
||||
[
|
||||
|
|
@ -251,13 +278,33 @@ check_trace(Trace, _Cmds, _Seed) ->
|
|||
{no_append_duplicates, NoAppendLPNDups},
|
||||
%% If you want to see PULSE causing crazy scheduling, then
|
||||
%% change one of the "true orelse" -> "false orelse" below.
|
||||
{bogus_no_gaps,
|
||||
true orelse
|
||||
(AppendLPNs == [] orelse length(range_ify(AppendLPNs)) == 1)},
|
||||
{bogus_exactly_1_to_N,
|
||||
true orelse (AppendLPNs == lists:seq(1, length(AppendLPNs)))}
|
||||
%% {bogus_no_gaps,
|
||||
%% true orelse
|
||||
%% (AppendLPNs == [] orelse length(range_ify(AppendLPNs)) == 1)},
|
||||
%% {bogus_exactly_1_to_N,
|
||||
%% true orelse (AppendLPNs == lists:seq(1, length(AppendLPNs)))},
|
||||
{true, true}
|
||||
])).
|
||||
|
||||
add_LPN_to_append_calls([{TS, {call, Pid, {append, Page}}}|Rest]) ->
|
||||
Res = trace_lookahead_pid(Pid, Rest),
|
||||
New = case Res of
|
||||
{ok, LPN} ->
|
||||
{TS, {call, Pid, {append, Page, will_be, LPN}}};
|
||||
Else ->
|
||||
{TS, {call, Pid, {append, Page, will_fail, Else}}}
|
||||
end,
|
||||
[New|add_LPN_to_append_calls(Rest)];
|
||||
add_LPN_to_append_calls([X|Rest]) ->
|
||||
[X|add_LPN_to_append_calls(Rest)];
|
||||
add_LPN_to_append_calls([]) ->
|
||||
[].
|
||||
|
||||
trace_lookahead_pid(Pid, [{_TS, {result, Pid, Res}}|_]) ->
|
||||
Res;
|
||||
trace_lookahead_pid(Pid, [_H|T]) ->
|
||||
trace_lookahead_pid(Pid, T).
|
||||
|
||||
%% Presenting command data statistics in a nicer way
|
||||
command_data({set, _, {call, _, Fun, _}}, {_S, _V}) ->
|
||||
Fun.
|
||||
|
|
|
|||
Loading…
Reference in a new issue