greg/machi
1
0
Fork 0
Code Issues 11 Pull requests 1 Projects Releases Packages Wiki Activity Actions

Make PULSE model aware of read-repair for 'error_trimmed' races

Browse source 
The read operation isn't a read-only operation: it can trigger
read-repair in the case where a hole is discovered.  The PULSE
model needs to be aware of this kind of thing.

Imagine that we have a 3-way race, between an append to LPN 1,
a read of LPN 1, and a trim of LPN 1.  There is a single chain
of length 3.  The FLUs in the chain are annotated below with
"F1", "F2", and "F3".  Note also the indentation levels, with
F1's indented is smaller than F2's << F3's.

 2,{call,<0.8748.3>,{append,<<0>>,will_be,1}}},
 4,{call,<0.8746.3>,{read,1}}},
 6,{call,<0.8747.3>,{trim,1,will_fail,error_unwritten}}},

 6, Read has contacted tail of chain, it is unwritten.  Time for repair.
 6,{read_repair,1,[<0.8741.3>,<0.8742.3>,<0.8743.3>]}},

 6,  F1:{flu,write,<0.8741.3>,1,ok}},
 7,  F1:{flu,trim,<0.8741.3>,1,ok}},  % by repair

 9,{read_repair,1,fill,<0.8742.3>}},

 9,          F2:{flu,trim,<0.8742.3>,1,error_unwritten}},

 9,{read_repair,1,<0.8741.3>,trimmed}},

10,{result,<0.8747.3>,error_unwritten}},
   Trim operation from time=6 stops here

10,          F2:{flu,write,<0.8742.3>,1,ok}},
11,          F2:{flu,fill,<0.8742.3>,1,error_overwritten}},

12,                  F3:{flu,write,<0.8743.3>,1,ok}},

12,{read_repair,1,fill,<0.8742.3>,overwritten,try_trim}},

13,{result,<0.8748.3>,{ok,1}}}, % append/write to LPN 1

13,          F2:{flu,trim,<0.8742.3>,1,ok}},

14,{read_repair,1,fill,<0.8743.3>}},
15,                  F3:{flu,fill,<0.8743.3>,1,error_overwritten}},

16,{read_repair,1,fill,<0.8743.3>,overwritten,try_to_trim}},
17,                  F3:{flu,trim,<0.8743.3>,1,ok}},

18,{result,<0.8746.3>,error_trimmed}}]
This commit is contained in:
Scott Lystig Fritchie 2014-02-24 11:52:31 +09:00
parent a7dd78d8f1
commit 479efce0b1
1 changed files with 15 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
prototype/corfurl/test/corfurl_pulse.erl
View file

@ -320,7 +320,7 @@ 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, {read, LPN, _, _}}) -> LPN;
({call, _Pid, {fill, LPN, will_be, ok}}) -> LPN;
({call, _Pid, {trim, LPN, will_be, ok}}) -> LPN
end,
@ -344,7 +344,9 @@ check_trace(Trace0, _Cmds, _Seed) ->
({call, Pid, {fill, LPN, will_be, ok}}) ->
{mod_working, w_ft, LPN, fill, Pid};
({call, Pid, {trim, LPN, will_be, ok}}) ->
{mod_working, w_tt, LPN, trim, Pid}
{mod_working, w_tt, LPN, trim, Pid};
({call, Pid, {read, LPN, will_fail, error_trimmed}}) ->
{mod_working, w_tt, LPN, read_repair_maybe, Pid}
end,
fun({mod_working, _Ttn, _LPN, _Pg, _Pid}, {result, _Pid, _Res})->
[]
@ -434,7 +436,7 @@ check_trace(Trace0, _Cmds, _Seed) ->
%% that appear at any time during the read op's lifetime.
Reads = eqc_temporal:stateful(
fun({call, Pid, {read, LPN}}) ->
fun({call, Pid, {read, LPN, _, _}}) ->
{read, Pid, LPN, []}
end,
fun({read, Pid, LPN, V1s}, {values, Values}) ->
@ -519,6 +521,15 @@ add_LPN_to_append_calls([{TS, {call, Pid, {OpName, LPN}}}|Rest])
{TS, {call, Pid, {OpName, LPN, will_fail, Else}}}
end,
[New|add_LPN_to_append_calls(Rest)];
add_LPN_to_append_calls([{TS, {call, Pid, {read, LPN}}}|Rest]) ->
Res = trace_lookahead_pid(Pid, Rest),
New = case Res of
Page when is_binary(Page) ->
{TS, {call, Pid, {read, LPN, will_be, Page}}};
Else ->
{TS, {call, Pid, {read, LPN, 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([]) ->
@ -747,7 +758,7 @@ perhaps_trip_append_page(true, Else, _Page) ->
perhaps_trip_read_approx(false, Res, _LPN) ->
Res;
perhaps_trip_read_approx(true, _Res, 3 = LPN) ->
io:format(user, "TRIP: read_approx LPN ~p", [LPN]),
io:format(user, "TRIP: read_approx LPN ~p\n", [LPN]),
<<"FAKE!">>;
perhaps_trip_read_approx(true, Res, _LPN) ->
Res.