Fix up PULSE code & documentation

prototype/README.md

@@ -12,6 +12,15 @@ purposes.  The code is preserved here for use as:
 * Some code might actually be reusable, as-is or after some
   refactoring.
 
+The prototype code here is not meant for long-term use or
+maintenance.  We are unlikely to accept changes/pull requests for adding
+large new features or to build full Erlang/OTP applications using this
+code only.
+
+However, pull requests for small changes, such as support for
+newer Erlang versions (e.g., Erlang 17), will be gladly accepted.
+We will also accept fixes for bugs in the test code.
+
 ## The chain-manager prototype
 
 TODO

prototype/corfurl/README.md

@@ -27,7 +27,8 @@ flawed or broken.
 that the logic still works without any active sequencer.
 * Includes logic to allow the sequencer to give
 **faulty sequencer assignments**, including duplicate page numbers and
-gaps of unused pages.
+gaps of unused pages.  Even if the sequencer **lies to us**, all other
+CORFU operation should remain 100% correct.
 
 If you have a Quviq QuickCheck license, then you can also use the
 `make pulse` target.

prototype/corfurl/docs/corfurl.md

@@ -1,3 +1,17 @@
+## Notes on developing & debugging this CORFU prototype
+
+I've recorded some notes while developing & debugging this CORFU
+prototype.  See the `corfurl/notes` subdirectory.
+
+Most of the cases mentioned involve race conditions that were notable
+during the development cycle.  There is one case that IIRC is not
+mentioned in any of the CORFU papers and is probably a case that
+cannot be fixed/solved by CORFU itself.
+
+Each of the scenario notes includes an MSC diagram specification file
+to help illustrate the race.  The diagrams are annotated by hand, both
+with text and color, to point out critical points of timing.
+
 ## CORFU papers
 
 I recommend the "5 pages" paper below first, to give a flavor of

prototype/corfurl/docs/corfurl/notes/README.md

@@ -1,3 +1,16 @@
+## NOTE
+
+The Git commit numbers used below refer to a private Git
+repository and not to the https://github.com/basho/machi repo.  My
+apologies for any confusion.
+
+## Generating diagrams of the race/bug scenarios
+
+Each of the scenario notes includes an MSC diagram
+(Message Sequence Chart) specification file
+to help illustrate the race, each with an `.mscgen` suffix.  Use the
+`mscgen` utility to render the diagrams into PNG, Encapsulated Postscript,
+or other graphic file formats.
 
 ## read-repair-race.1.
 

prototype/corfurl/docs/using-pulse.md

@@ -128,8 +128,7 @@ REPL interactive work can be done via:
 ## Seeing an PULSE scheduler interleaving failure in action
 
 1. Edit `corfurl_pulse:check_trace()` to uncomment the
-   use of `conjunction()` that mentions `bogus_order_check_do_not_use_me`
-   and comment out the real `conjunction()` call below it.
+   use of `conjunction()` that mentions the `{bogus_no_gaps, ...}` tuple.
 2. Recompile & reload.
 3. Check.
 

prototype/corfurl/test/corfurl_pulse.erl

@@ -477,7 +477,9 @@ check_trace(Trace0, _Cmds, _Seed) ->
                fun(x)-> [] end,
                Events),
     {_, _, Perhaps} = lists:last(eqc_temporal:all_future(PerhapsR)),
-    %%?QC_FMT("*Perhaps: ~p\n", [Perhaps]),
+    %% ?QC_FMT("*Perhaps: ~p\n", [Perhaps]),
+    _PerhapsLPNs = lists:sort([LPN || {perhaps, LPN, _} <- Perhaps]),
+    %% ?QC_FMT("*_PerhapsLPNs: ~p\n", [_PerhapsLPNs]),
     Reads = eqc_temporal:stateful(
                fun({call, Pid, {read, LPN, _, _}}) ->
                        {read, Pid, LPN, []}
@@ -555,13 +557,12 @@ check_trace(Trace0, _Cmds, _Seed) ->
         InvalidTransitions == []},
        {no_bad_reads,
         eqc_temporal:is_false(eqc_temporal:all_future(BadReads))},
-       %% If you want to see PULSE causing crazy scheduling, then
-       %% change one of the "true orelse" -> "false orelse" below.
        %% {bogus_no_gaps,
-       %%  true orelse
-       %%          (AppendLPNs == [] orelse length(range_ify(AppendLPNs)) == 1)},
+       %%  (_PerhapsLPNs == [] orelse length(range_ify(_PerhapsLPNs)) == 1)},
        %% {bogus_exactly_1_to_N,
-       %%  true orelse (AppendLPNs == lists:seq(1, length(AppendLPNs)))},
+       %%  (_PerhapsLPNs == lists:seq(1, length(_PerhapsLPNs)))},
+       %% Do not remove the {true, true}, please.  It should always be the
+       %% last conjunction test.
        {true, true}
       ])).