This trim race is (as far as I can tell) fine -- I see no correctness
problem with CORFU, on the client side or the server side. However,
this race with a trim causes a model problem that I believe can be
solved this way:
1. We must keep track of the fact that the page write is happening:
someone can notice the write via read-repair or even a regular read by
the tail. We do this in basically the way that all other writes
are handled in the ValuesR relation.
2. Add new code to client-side writer: if there's a trim race, *and*
if we're using PULSE, then return a special error code that says that
the write was ok *and* that we raced with trim.
2b. If we aren't using pulse, just return {ok, LPN}.
3. For the transition check property, treat the new return code as if
it is a w_tt. Actually, we use a special marker atom, w_special_trimmed
for that purpose, but it is later treated the same way that w_tt is by the
filter_transition_trimfill_suffixes() filter.
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}}]
Also, for peace of mind (I hope), I've added this -ifndef to introduce
a bug that should cause the new exactly-once append_page() check to fail.
This should make it easier to change the model and *TEST* the changes,
to avoid breaking the model without ever knowing it.
