From b3ed9ef51ccfff6e0bef42f5f7fe22e37d3bd1d2 Mon Sep 17 00:00:00 2001 From: Scott Lystig Fritchie Date: Thu, 20 Feb 2014 00:12:20 +0900 Subject: [PATCH] Add fill checking to PULSE model, minimal API coverage is complete --- prototype/corfurl/src/corfurl.erl | 17 ++++++---- prototype/corfurl/test/corfurl_pulse.erl | 40 +++++++++++++++++++----- 2 files changed, 43 insertions(+), 14 deletions(-) diff --git a/prototype/corfurl/src/corfurl.erl b/prototype/corfurl/src/corfurl.erl index 1eb047b..c92a1ac 100644 --- a/prototype/corfurl/src/corfurl.erl +++ b/prototype/corfurl/src/corfurl.erl @@ -25,7 +25,7 @@ read_projection/2, save_projection/2]). -export([append_page/3, read_page/2, scan_forward/3, - fill_page/2]). + fill_page/2, trim_page/2]). -include("corfurl.hrl"). @@ -203,16 +203,21 @@ scan_forward(P, LPN, MaxPages, _Status, _MoreP, Acc) -> fill_page(#proj{epoch=Epoch} = P, LPN) -> Chain = project_to_chain(LPN, P), - fill_page2(Chain, Epoch, LPN). + fill_or_trim_page(Chain, Epoch, LPN, fill). -fill_page2([], _Epoch, _LPN) -> +trim_page(#proj{epoch=Epoch} = P, LPN) -> + Chain = project_to_chain(LPN, P), + fill_or_trim_page(Chain, Epoch, LPN, trim). + +fill_or_trim_page([], _Epoch, _LPN, _Func) -> ok; -fill_page2([H|T], Epoch, LPN) -> - case corfurl_flu:fill(flu_pid(H), Epoch, LPN) of +fill_or_trim_page([H|T], Epoch, LPN, Func) -> + case corfurl_flu:Func(flu_pid(H), Epoch, LPN) of ok -> - fill_page2(T, Epoch, LPN); + fill_or_trim_page(T, Epoch, LPN, Func); Else -> %% TODO: worth doing anything here, if we're in the middle of chain? + %% TODO: is that ^^ anything different for fill vs. trim? Else end. diff --git a/prototype/corfurl/test/corfurl_pulse.erl b/prototype/corfurl/test/corfurl_pulse.erl index 0426beb..0b4bb27 100644 --- a/prototype/corfurl/test/corfurl_pulse.erl +++ b/prototype/corfurl/test/corfurl_pulse.erl @@ -65,7 +65,7 @@ %% Define true to fake bad behavior that model **must** notice & fail! -ifndef(TRIP_no_append_duplicates). --define(TRIP_no_append_duplicates, false). +-define(TRIP_no_append_duplicates, true). -endif. -ifndef(TRIP_bad_read). -define(TRIP_bad_read, false). @@ -76,6 +76,9 @@ -ifndef(TRIP_bad_fill). -define(TRIP_bad_fill, false). -endif. +-ifndef(TRIP_bad_trim). +-define(TRIP_bad_trim, false). +-endif. initial_state() -> #state{}. @@ -115,6 +118,8 @@ command(#state{run=Run} = S) -> || S#state.is_setup] ++ [{4, {call, ?MODULE, fill, [Run, gen_approx_page()]}} || S#state.is_setup] ++ + [{4, {call, ?MODULE, trim, [Run, gen_approx_page()]}} + || S#state.is_setup] ++ [])). %% Precondition, checked before a command is added to the command sequence. @@ -138,6 +143,8 @@ next_state(S, _, {call, _, read_approx, _}) -> next_state(S, _, {call, _, scan_forward, _}) -> S; next_state(S, _, {call, _, fill, _}) -> + S; +next_state(S, _, {call, _, trim, _}) -> S. eqeq(X, X) -> true; @@ -163,12 +170,14 @@ postcondition(_S, {call, _, scan_forward, _}, V) -> _ -> eqeq(V, {todoTODO_fixit,?LINE}) end; -postcondition(_S, {call, _, fill, _}, V) -> +postcondition(_S, {call, _, FillTrim, _}, V) + when FillTrim == fill; FillTrim == trim -> case V of ok -> true; error_trimmed -> true; + error_unwritten -> true; error_overwritten -> true; - _ -> eqeq(V, {fill_error, V}) + _ -> eqeq(V, {error, FillTrim, V}) end. valid_read_result(Pg) when is_binary(Pg) -> true; @@ -305,7 +314,8 @@ check_trace(Trace0, _Cmds, _Seed) -> AllLPNsR = eqc_temporal:stateful( fun({call, _Pid, {append, _Pg, will_be, LPN}}) -> LPN; ({call, _Pid, {read, LPN}}) -> LPN; - ({call, _Pid, {fill, LPN, will_be, ok}}) -> LPN + ({call, _Pid, {fill, LPN, will_be, ok}}) -> LPN; + ({call, _Pid, {trim, LPN, will_be, ok}}) -> LPN end, fun(x) -> [] end, Calls), @@ -333,8 +343,6 @@ check_trace(Trace0, _Cmds, _Seed) -> [] end, Events), - %%ModsX = filter_relation_facts(fun(T) when element(4,T) == fill; element(4,T) == trim -> true; (_) -> false end, Mods), - %%io:format("Modsx ~p\n", [ModsX]), %% StartMod contains {mod_start, Ttn, LPN, V} when a modification finished. %% DoneMod contains {mod_end, Ttn, LPN, V} when a modification finished. @@ -675,6 +683,14 @@ fill(#run{seq=Seq, proj=Proj}, SeedInt) -> perhaps_trip_fill_page(?TRIP_bad_fill, Res, LPN) end). +trim(#run{seq=Seq, proj=Proj}, SeedInt) -> + LPN = pick_an_LPN(Seq, SeedInt) + 2, + ?LOG({trim, LPN}, + begin + Res = corfurl:trim_page(Proj, LPN), + perhaps_trip_trim_page(?TRIP_bad_trim, Res, LPN) + end). + perhaps_trip_append_page(false, Res, _Page) -> Res; perhaps_trip_append_page(true, {ok, LPN}, _Page) when LPN > 3 -> @@ -693,7 +709,7 @@ perhaps_trip_read_approx(true, Res, _LPN) -> perhaps_trip_scan_forward(false, Res, _EndLPN) -> Res; -perhaps_trip_scan_forward(true, _Res, 20) -> +perhaps_trip_scan_forward(true, _Res, 10) -> io:format(user, "TRIP: scan_forward\n", []), <<"magic number bingo, you are a winner">>; perhaps_trip_scan_forward(true, Res, _EndLPN) -> @@ -701,12 +717,20 @@ perhaps_trip_scan_forward(true, Res, _EndLPN) -> perhaps_trip_fill_page(false, Res, _EndLPN) -> Res; -perhaps_trip_fill_page(true, _Res, LPN) when 10 =< LPN, LPN =< 20 -> +perhaps_trip_fill_page(true, _Res, LPN) when 3 =< LPN, LPN =< 5 -> io:format(user, "TRIP: fill_page\n", []), ok; % can trigger both invalid ttn and bad read perhaps_trip_fill_page(true, Res, _EndLPN) -> Res. +perhaps_trip_trim_page(false, Res, _EndLPN) -> + Res; +perhaps_trip_trim_page(true, _Res, LPN) when 3 =< LPN, LPN =< 5 -> + io:format(user, "TRIP: trim_page\n", []), + ok; +perhaps_trip_trim_page(true, Res, _EndLPN) -> + Res. + -endif. % PULSE -endif. % TEST