diff --git a/prototype/corfurl/.gitignore b/prototype/corfurl/.gitignore index 661af0e..91f0c9c 100644 --- a/prototype/corfurl/.gitignore +++ b/prototype/corfurl/.gitignore @@ -4,3 +4,4 @@ current_counterexample.eqc deps ebin/*.beam ebin/*.app +erl_crash.dump diff --git a/prototype/corfurl/src/corfurl.erl b/prototype/corfurl/src/corfurl.erl index 7a1dd0d..0511518 100644 --- a/prototype/corfurl/src/corfurl.erl +++ b/prototype/corfurl/src/corfurl.erl @@ -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. diff --git a/prototype/corfurl/src/corfurl_flu.erl b/prototype/corfurl/src/corfurl_flu.erl index d847d5d..8951b5a 100644 --- a/prototype/corfurl/src/corfurl_flu.erl +++ b/prototype/corfurl/src/corfurl_flu.erl @@ -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