Attempt to fix unimplemented corner case, thanks PULSE!

This commit is contained in:
Scott Lystig Fritchie 2014-02-24 18:22:40 +09:00
parent b7e3f91931
commit d077148b47
3 changed files with 35 additions and 7 deletions

View file

@ -4,3 +4,4 @@ current_counterexample.eqc
deps
ebin/*.beam
ebin/*.app
erl_crash.dump

View file

@ -62,14 +62,14 @@ append_page(Sequencer, P, Page, Retries) when Retries < 50 ->
write_single_page(#proj{epoch=Epoch} = P, LPN, Page) ->
Chain = project_to_chain(LPN, P),
write_single_page_to_chain(Chain, Epoch, LPN, Page, 1).
write_single_page_to_chain(Chain, Chain, Epoch, LPN, Page, 1).
write_single_page_to_chain([], _Epoch, _LPN, _Page, _Nth) ->
write_single_page_to_chain([], _Chain, _Epoch, _LPN, _Page, _Nth) ->
ok;
write_single_page_to_chain([FLU|Rest], Epoch, LPN, Page, Nth) ->
write_single_page_to_chain([FLU|Rest], Chain, Epoch, LPN, Page, Nth) ->
case corfurl_flu:write(flu_pid(FLU), Epoch, LPN, Page) of
ok ->
write_single_page_to_chain(Rest, Epoch, LPN, Page, Nth+1);
write_single_page_to_chain(Rest, Chain, Epoch, LPN, Page, Nth+1);
error_badepoch ->
%% TODO: Interesting case: there may be cases where retrying with
%% a new epoch & that epoch's projection is just fine (and
@ -96,13 +96,22 @@ write_single_page_to_chain([FLU|Rest], Epoch, LPN, Page, Nth) ->
{ok, AlreadyThere} when AlreadyThere =:= Page ->
%% Alright, well, let's go continue the repair/writing,
%% since we agree on the page's value.
write_single_page_to_chain(Rest, Epoch, LPN, Page, Nth+1);
write_single_page_to_chain(Rest, Chain, Epoch, LPN, Page, Nth+1);
error_badepoch ->
%% TODO: same TODO as the above error_badepoch case.
error_badepoch;
error_trimmed ->
%% PULSE can drive us to this case, excellent!
%% We had a race with read-repair and lost (the write).
%% Now this read failed with error_trimmed because we
%% lost a race with someone trimming this block.
%% Let's be paranoid and repair, just in case.
OurResult = error_trimmed,
error_trimmed = read_repair_chain(Epoch, LPN, Chain),
OurResult;
Else ->
%% Guess what?? PULSE can drive us to this case, excellent!
giant_error({left_off_here, ?MODULE, ?LINE, Else})
giant_error({left_off_here, ?MODULE, ?LINE, Else, nth, Nth})
end
end.

View file

@ -40,6 +40,7 @@
-compile(export_all).
-ifdef(PULSE).
-compile({parse_transform, pulse_instrument}).
-compile({pulse_skip,[{msc, 3}]}).
-endif.
-endif.
@ -47,6 +48,7 @@
%%% Debugging: for extra events in the PULSE event log, use the 2nd statement.
-define(EVENT_LOG(X), ok).
%% -define(EVENT_LOG(X), erlang:display(X)).
%%% -define(EVENT_LOG(X), event_logger(X)).
-record(state, {
@ -96,7 +98,9 @@ fill(Pid, Epoch, LogicalPN)
g_call(Pid, Arg, Timeout) ->
LC1 = lamport_clock:get(),
msc(self(), Pid, Arg),
{Res, LC2} = gen_server:call(Pid, {Arg, LC1}, Timeout),
msc(Pid, self(), Res),
lamport_clock:update(LC2),
Res.
@ -176,7 +180,9 @@ handle_call({{read, ClientEpoch, _LogicalPN}, LC1}, _From,
{reply, {error_badepoch, LC2}, State};
handle_call({{read, _ClientEpoch, LogicalPN}, LC1}, _From, State) ->
LC2 = lamport_clock:update(LC1),
{reply, {read_page(LogicalPN, State), LC2}, State};
Reply = read_page(LogicalPN, State),
?EVENT_LOG({flu, read, self(), LogicalPN, Reply}),
{reply, {Reply, LC2}, State};
handle_call({{seal, ClientEpoch}, LC1}, _From, #state{min_epoch=MinEpoch} = State)
when ClientEpoch =< MinEpoch ->
@ -409,3 +415,15 @@ trim_page(Op, LogicalPN, #state{max_mem=MaxMem, mem_fh=FH} = S) ->
true ->
badarg
end.
-ifdef(PULSE_HACKING).
%% Create a trace file that can be formatted by "mscgen" utility.
%% Lots of hand-editing is required after creating the file, sorry!
msc(_From, _To, _Tag) ->
{ok, FH} = file:open("/tmp/goo", [write, append]),
io:format(FH, " \"~w\" -> \"~w\" [ label = \"~w\" ] ;\n", [_From, _To, _Tag]),
file:close(FH).
-else. % PULSE_HACKING
msc(_From, _To, _Tag) ->
ok.
-endif. % PULSE_HACkING