Commit graph

860 commits

Author SHA1 Message Date
Scott Lystig Fritchie
8df5326b0c Try to restart the sequencer only if it looks like nobody else has 2015-03-02 18:08:29 +09:00
Scott Lystig Fritchie
0b031bcf0a Change polling constants for to deal with PULSE's evil 2015-03-02 18:08:28 +09:00
Scott Lystig Fritchie
fb1216649c Finish very basic PULSE testing of stopping & restarting the sequencer 2015-03-02 18:08:28 +09:00
Scott Lystig Fritchie
63d1c93fc9 Fix silly-dumb errors in seal epoch comparisons 2015-03-02 18:08:28 +09:00
Scott Lystig Fritchie
96b561cde9 Fix broken EUnit tests 2015-03-02 18:08:28 +09:00
Scott Lystig Fritchie
d93572c391 Refactoring to implement stop_sequencer command 2015-03-02 18:08:24 +09:00
Scott Lystig Fritchie
d5091358ff Put the sequencer pid inside the projection 2015-03-02 18:06:52 +09:00
Scott Lystig Fritchie
a64a09338d Fix broken EUnit tests (been in PULSE land too long) 2015-03-02 18:06:48 +09:00
Scott Lystig Fritchie
20a2a51649 Partial fix (#2 of 2) for model problem in honest write-vs-trim race 2015-03-02 18:05:03 +09:00
Scott Lystig Fritchie
638a45e8cb Partial fix for model problem in honest write-vs-trim race 2015-03-02 18:05:03 +09:00
Scott Lystig Fritchie
eabebac6f2 Fix PULSE model difficulty of how to handle races between write & trim.
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.
2015-03-02 18:05:02 +09:00
Scott Lystig Fritchie
13e15e0ecf Add MSC charts to help explain BAD-looking trim race 2015-03-02 18:05:02 +09:00
Scott Lystig Fritchie
d077148b47 Attempt to fix unimplemented corner case, thanks PULSE! 2015-03-02 18:05:02 +09:00
Scott Lystig Fritchie
b7e3f91931 Add ?EVENT_LOG() to add extra trace info to corfurl and corfurl_flu 2015-03-02 18:05:02 +09:00
Scott Lystig Fritchie
479efce0b1 Make PULSE model aware of read-repair for 'error_trimmed' races
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}}]
2015-03-02 18:05:02 +09:00
Scott Lystig Fritchie
a7dd78d8f1 Switch to Lamport clocks for PULSE verifying 2015-03-02 18:04:59 +09:00
Scott Lystig Fritchie
5420e9ca1f Bugfix for read repair: if trimmed, try fill first then trim 2015-03-02 18:03:10 +09:00
Scott Lystig Fritchie
88d44722be Fix PULSE model bug of adding multiple same values to orddict 2015-03-02 18:03:10 +09:00
Scott Lystig Fritchie
8ec5f04903 Bug: PULSE found a way to reach a 'left_off_here' corner case, sweet 2015-03-02 18:03:10 +09:00
Scott Lystig Fritchie
e40394a3a7 Bugfix: yet another race in read_repair, sweet 2015-03-02 18:03:10 +09:00
Scott Lystig Fritchie
370c57b78a Bug: corfurl:read_repair_chain() should use trim when it encounters error_trimmed 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
fd32bcb308 Fix PULSE model to accomodate API change from previous commit.
Now 1+ trim & fill transitions are collapsed to a single 'w_t+' atom.
The atom name is a bit odd; think about regexps and it hopefully
makes sense.
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
431827f65e Allow racing trim/fill and read-repair to simply "win".
This exposes a bug in the PULSE model, now that we can have multiple
successful fill/trim for the same LPN.
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
5edee3a2cf Don't bother adding 2 when picking an LPN for fill & trim 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
d2562588f2 Move the lists:reverse() in make_chains() to preserve input's order in the output 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
e791876212 Fix silly model error when calculating values 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
f5c4474669 Derp, turn off TRIP_no_append_duplicates 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
b3ed9ef51c Add fill checking to PULSE model, minimal API coverage is complete 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
7a46709c13 Change transition type names to make better invalid transition detection 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
8a56771182 Add better condition for perhaps_trip_fill_page() 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
db6fa3d895 Fix two bugs found by PULSE in corfurl_flu.erl, yay! 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
86d4583aef Add fill support to the PULSE model 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
7dba8beae9 Refactor PULSE test for easier checking, prior to adding fill & trim. 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
78019b402f Refactor the PULSE model testing error 'trip' code 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
c80921de25 Add scan_forward() command, no result checking yet 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
fb6b1cdc3c Fix read_page() model problem: no more false positives! 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
e9851767fc Add read_page() temporal check 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
a7aff2f141 Dumbdumbdumb don't interfere with event_logger:event() duh! 2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
c14e1facf4 Add read_approx() to the PULSE model, only 5% correctness checks done 2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
572d1803d0 Add (mostly) temporal logic checking for exactly-once append_page().
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.
2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
25bf64a03c Just in case commit: WIP 2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
58ced8d14c Add PULSE control over sequencer handing out duplicate page numbers 2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
21a3fd6d07 Use temporal logic for check_trace() 2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
e0ec95e8f7 Added small PULSE usage sketch in docs/corfurl.md 2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
b430fa479c PULSE condition checking is only 98% embarassing 2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
bcc6cf1e6a PULSE bugfix: race with finish_init message 2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
a294a0eff0 Skeleton of PULSE test created, first bug (race in sequencer init) is found, huzzah! 2015-03-02 18:03:05 +09:00
Scott Lystig Fritchie
feed231d5e Move EUnit test code to test subdir 2015-03-02 17:59:31 +09:00
Scott Lystig Fritchie
3963ce44f0 More sanity checking for fill() in smoke test 2015-03-02 17:57:31 +09:00
Scott Lystig Fritchie
3d2be7255f Basic smoke test for read repair 2015-03-02 17:57:31 +09:00