Commit graph

948 commits

Author SHA1 Message Date
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
Scott Lystig Fritchie
6014b0584e Fix read() response to a prior fill 2015-03-02 17:57:31 +09:00
Scott Lystig Fritchie
c23aeabc20 Read-repair, not tested 2015-03-02 17:57:30 +09:00
Scott Lystig Fritchie
945635f837 Basic scan_forward done 2015-03-02 17:57:30 +09:00
Scott Lystig Fritchie
05a71eebb0 corfurl:read_page() done, no read-repair yet 2015-03-02 17:57:30 +09:00
Scott Lystig Fritchie
72bf329e1c Add fledgling log implementation based on CORFU papers 2015-03-02 17:57:27 +09:00
Scott Lystig Fritchie
2bf76b5727 Initial documentation import 2015-03-02 17:34:14 +09:00
Scott Lystig Fritchie
ab31a27823 Add APL v2 LICENSE file 2015-03-02 17:34:14 +09:00
Scott Lystig Fritchie
3524d1bc75 Add APL v2 LICENSE file 2015-03-02 17:12:39 +09:00
Scott Lystig Fritchie
75154e0892 Initial documentation import 2015-03-02 13:32:56 +09:00
Scott Lystig Fritchie
880812fb1e Initial commit 2015-02-18 14:40:05 +09:00