diff --git a/prototype/README.md b/prototype/README.md index c391287..3b2e747 100644 --- a/prototype/README.md +++ b/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 diff --git a/prototype/corfurl/README.md b/prototype/corfurl/README.md index f048333..fb89daf 100644 --- a/prototype/corfurl/README.md +++ b/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. diff --git a/prototype/corfurl/docs/corfurl.md b/prototype/corfurl/docs/corfurl.md index 4298f5f..d991f39 100644 --- a/prototype/corfurl/docs/corfurl.md +++ b/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 diff --git a/prototype/corfurl/docs/corfurl/notes/README.md b/prototype/corfurl/docs/corfurl/notes/README.md index b5757aa..e5deb23 100644 --- a/prototype/corfurl/docs/corfurl/notes/README.md +++ b/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. diff --git a/prototype/corfurl/docs/using-pulse.md b/prototype/corfurl/docs/using-pulse.md index 2504770..7377394 100644 --- a/prototype/corfurl/docs/using-pulse.md +++ b/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. diff --git a/prototype/corfurl/test/corfurl_pulse.erl b/prototype/corfurl/test/corfurl_pulse.erl index d00c2d7..28bdcb2 100644 --- a/prototype/corfurl/test/corfurl_pulse.erl +++ b/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} ])).