Merge remote-tracking branch 'origin/otp' into hbbft

cmeiklejohn · cmeiklejohn · commit 75529ac9d460 · 2019-08-14T00:23:05.000-07:00
diff --git a/analysis/partisan-causality-zraft b/analysis/partisan-causality-zraft
@@ -0,0 +1 @@
+[].
diff --git a/annotations/partisan-annotations-zraft b/annotations/partisan-annotations-zraft
@@ -0,0 +1,4 @@
+[
+  {causality, []},
+  {background, []}
+].
diff --git a/bin/check-zraft.sh b/bin/check-zraft.sh
@@ -4,9 +4,19 @@ export MODULE=zraft
 export SUBLIST=0
 export PRELOAD_SCHEDULES=false
 export RECURSIVE=true
-export EXIT_ON_COUNTEREXAMPLE=true
+# export EXIT_ON_COUNTEREXAMPLE=true
 export PRUNING=false
 export SYSTEM_MODEL=prop_partisan_zraft
+export RESTART_NODES=true 
+
+# echo "Running example suite to identify minimal successful example..."
+# rm -rf priv/lager; pkill -9 beam.smp; DISABLE_RANDOM=true RESTART_NODES=${RESTART_NODES} IMPLEMENTATION_MODULE=${MODULE} NUM_TESTS=3 SCHEDULER=single_success bin/counterexample-find.sh
+
+# echo "Replaying existing example..."
+# rm -rf priv/lager; pkill -9 beam.smp; REPLAY=true DISABLE_RANDOM=true RESTART_NODES=${RESTART_NODES} IMPLEMENTATION_MODULE=${MODULE} NUM_TESTS=3 SCHEDULER=single_success bin/counterexample-replay.sh
+
+# echo "Running single run model checker..."
+# rm -rf priv/lager; pkill -9 beam.smp; TRACE_FILE=/tmp/partisan-latest.trace REPLAY_TRACE_FILE=/tmp/partisan-replay.trace PRELOAD_OMISSIONS_FILE=/tmp/partisan-preload.trace SHRINKING=true REPLAY=true SYSTEM_MODEL=${SYSTEM_MODEL} IMPLEMENTATION_MODULE=${MODULE} RESTART_NODES=${RESTART_NODES} ./rebar3 ct --readable=false -v --suite=filibuster_SUITE --case=model_checker_test
 
 echo "Running multi run fault-injector..."
-rm -rf priv/lager; pkill -9 beam.smp; DISABLE_RANDOM=true RESTART_NODES=false IMPLEMENTATION_MODULE=${MODULE} NUM_TESTS=10 SCHEDULER=finite_fault FAULT_INJECTION=true bin/counterexample-find.sh
+rm -rf priv/lager; pkill -9 beam.smp; DISABLE_RANDOM=true RESTART_NODES=${RESTART_NODES} IMPLEMENTATION_MODULE=${MODULE} NUM_TESTS=10 SCHEDULER=finite_fault FAULT_INJECTION=true bin/counterexample-find.sh
diff --git a/src/partisan_util.erl b/src/partisan_util.erl
@@ -301,7 +301,8 @@ gensym(Name) when is_atom(Name) ->
 gensym(Pid) when is_pid(Pid) ->
     {partisan_process_reference, pid_to_list(Pid)};
 gensym(Ref) when is_reference(Ref) ->
-    {partisan_encoded_reference, term_to_binary(Ref)}.
+    % {partisan_encoded_reference, binary_to_list(term_to_binary(Ref))}.
+    {partisan_encoded_reference, 1}.
 
 ref(Ref) ->
     GenSym = gensym(Ref),
@@ -320,14 +321,16 @@ pid(Pid) ->
             case partisan_config:get(register_pid_for_encoding, false) of 
                 true ->
                     Unique = erlang:unique_integer([monotonic, positive]),
-                    Name = "partisan_registered_name_" ++ integer_to_list(Unique),
 
-                    case process_info(Pid, registered_name) of 
+                    Name = case process_info(Pid, registered_name) of 
                         {registered_name, OldName} ->
                             lager:info("unregistering pid: ~p with name: ~p", [Pid, OldName]),
-                            unregister(OldName);
+
+                            %% TODO: Race condition on unregister/register.
+                            unregister(OldName),
+                            atom_to_list(OldName);
                         [] ->
-                            ok
+                            "partisan_registered_name_" ++ integer_to_list(Unique)
                     end,
 
                     lager:info("registering pid: ~p as name: ~p at node: ~p", [Pid, Name, Node]),
@@ -337,25 +340,30 @@ pid(Pid) ->
                     {partisan_remote_reference, Node, {partisan_process_reference, pid_to_list(Pid)}}
             end;
         _ ->
-            %% This is super dangerous.
+            %% This is even mmore super dangerous.
             case partisan_config:get(register_pid_for_encoding, false) of 
                 true ->
                     Unique = erlang:unique_integer([monotonic, positive]),
+
                     Name = "partisan_registered_name_" ++ integer_to_list(Unique),
                     [_, B, C] = string:split(pid_to_list(Pid), ".", all),
                     RewrittenProcessIdentifier = "<0." ++ B ++ "." ++ C,
+
                     RegisterFun = fun() ->
                         RewrittenPid = list_to_pid(RewrittenProcessIdentifier),
 
-                        case process_info(RewrittenPid, registered_name) of 
+                        NewName = case process_info(RewrittenPid, registered_name) of 
                             {registered_name, OldName} ->
                                 lager:info("unregistering pid: ~p with name: ~p", [Pid, OldName]),
-                                unregister(OldName);
+
+                                %% TODO: Race condition on unregister/register.
+                                unregister(OldName),
+                                atom_to_list(OldName);
                             [] ->
-                                ok
+                                Name
                         end,
 
-                        erlang:register(list_to_atom(Name), RewrittenPid)
+                        erlang:register(list_to_atom(NewName), RewrittenPid)
                     end,
                     lager:info("registering pid: ~p as name: ~p at node: ~p", [Pid, Name, Node]),
                     %% TODO: Race here unless we wait.
diff --git a/test/filibuster_SUITE.erl b/test/filibuster_SUITE.erl
@@ -300,7 +300,14 @@ model_checker_test(_Config) ->
 
     %% Compile cover.
     {ok, Base} = file:get_cwd(),
-    {ok, ImplementationModule} = cover:compile(filename:join([Base, "../../../../protocols/" ++ atom_to_list(ImplementationModule) ++ ".erl"])),
+    CoverModule = filename:join([Base, "../../../../protocols/" ++ atom_to_list(ImplementationModule) ++ ".erl"]),
+    case filelib:is_file(CoverModule) of 
+        true ->
+            {ok, _ImplementationModule} = cover:compile(filename:join([Base, "../../../../protocols/" ++ atom_to_list(ImplementationModule) ++ ".erl"])),
+            ok;
+        false ->
+            ok
+    end,
 
     %% Print cover modules.
     % CoverModules = cover:modules(),
@@ -370,6 +377,8 @@ model_checker_test(_Config) ->
 %% ===================================================================
 
 execute(Nodes, PerformPreloads, Replaying, Shrinking, Tracing, {M, F, A}) ->
+    debug("execute starting...", []), 
+
     %% Ensure replaying option is set.
     lists:foreach(fun({ShortName, _}) ->
         ok = rpc:call(?NAME(ShortName), partisan_config, set, [replaying, Replaying])
@@ -419,6 +428,7 @@ execute(Nodes, PerformPreloads, Replaying, Shrinking, Tracing, {M, F, A}) ->
     end, Nodes),
 
     %% Run proper.
+    debug("running proper check for ~p:~p(~p)...", [M, F, A]),
     Result = proper:check(M:F(), A, []),
     debug("execute result: ~p", [Result]),
 
@@ -427,6 +437,8 @@ execute(Nodes, PerformPreloads, Replaying, Shrinking, Tracing, {M, F, A}) ->
 
     %% Stop tracing infrastructure.
     partisan_trace_orchestrator:stop(),
+
+    debug("execute returning: ~p", [Result]),
     
     Result.
 
@@ -977,6 +989,9 @@ message_type(Message) ->
             MessageType1 = element(1, MessagePayload),
 
             ActualType = case MessageType1 of 
+                '$gen_sync_all_state_event' ->
+                    CastMessage = element(2, MessagePayload),
+                    element(1, CastMessage);
                 '$gen_cast' ->
                     CastMessage = element(2, MessagePayload),
                     element(1, CastMessage);
@@ -990,6 +1005,9 @@ message_type(Message) ->
             MessageType1 = element(1, Payload),
 
             ActualType = case MessageType1 of 
+                '$gen_sync_all_state_event' ->
+                    CastMessage = element(2, Payload),
+                    element(1, CastMessage);
                 '$gen_cast' ->
                     CastMessage = element(2, Payload),
                     element(1, CastMessage);
@@ -1272,11 +1290,11 @@ execute_schedule(StartTime, CurrentIteration, Nodes, Counterexample, PreloadOmis
                     ClassificationsExplored = ClassificationsExplored0 ++ [Classification],
                     % debug("=> Classification for this test: ~p~n", [Classification]),
 
-                    % MessageTypes = message_types(FinalTraceLines),
-                    % debug("=> MessageTypes for this test: ~p~n", [MessageTypes]),
+                    MessageTypes = message_types(FinalTraceLines),
+                    debug("=> MessageTypes for this test: ~p~n", [MessageTypes]),
 
-                    % OmissionTypes = message_types(Omissions),
-                    % debug("=> OmissionTypes for this test: ~p~n", [OmissionTypes]),
+                    OmissionTypes = message_types(Omissions),
+                    debug("=> OmissionTypes for this test: ~p~n", [OmissionTypes]),
 
                     %% Run the trace.
                     CommandFun = fun() ->
diff --git a/test/prop_partisan_zraft.erl b/test/prop_partisan_zraft.erl
@@ -60,7 +60,7 @@ value() ->
 
 %% How many nodes to run?
 node_num_nodes() ->
-    5.
+    3.
 
 %% What node-specific operations should be called.
 node_commands() ->
@@ -78,7 +78,7 @@ node_assertion_functions() ->
 
 %% Global functions.
 node_global_functions() ->
-    [check_delivery, sleep].
+    [sleep, check_delivery].
 
 %% What should the initial node state be.
 node_initial_state() ->
@@ -150,7 +150,7 @@ node_next_state(_State, NodeState, Response, Command) ->
 node_postcondition(#node_state{values=Values}, {call, ?MODULE, check_delivery, []}, Results) ->
     node_debug("verifying all written results are found: ~p", [Results]),
 
-    lists:foldl(fun({Key, Value}, All) ->
+    PostconditionResult = lists:foldl(fun({Key, Value}, All) ->
         case dict:find(Key, Values) of 
             {ok, Value} ->
                 node_debug("=> found key ~p with value ~p", [Key, Value]),
@@ -168,7 +168,11 @@ node_postcondition(#node_state{values=Values}, {call, ?MODULE, check_delivery, [
                         false andalso All
                 end
         end
-    end, true, Results);
+    end, true, Results),
+
+    node_debug("=> postcondition result: ~p", [PostconditionResult]),
+
+    PostconditionResult;
 node_postcondition(_NodeState, {call, ?MODULE, session_read, [_Node, _Key]}, {error, timeout}) ->
     node_debug("=> read failed, leader unavailable...", []),
     true;
@@ -198,6 +202,7 @@ node_postcondition(#node_state{values=Values}, {call, ?MODULE, read, [_Node, Key
 node_postcondition(_NodeState, {call, ?MODULE, sleep, []}, _Result) ->
     true;
 node_postcondition(_NodeState, {call, ?MODULE, session_write, [_Node, _Key, _Value]}, {ok, _}) ->
+    node_debug("=> write returned OK.", []),
     true;
 node_postcondition(_NodeState, {call, ?MODULE, write, [_Node, _Key, _Value]}, {ok, _}) ->
     true;
@@ -225,7 +230,7 @@ sleep() ->
     ?PROPERTY_MODULE:command_preamble(RunnerNode, [sleep]),
 
     node_debug("sleeping for convergence...", []),
-    timer:sleep(40000),
+    timer:sleep(1000),
 
     ?PROPERTY_MODULE:command_conclusion(RunnerNode, [sleep]),
 
@@ -344,6 +349,12 @@ node_begin_case() ->
         ok = rpc:call(?NAME(ShortName), partisan_config, set, [pid_encoding, true])
     end, Nodes),
 
+    %% Enable register_pid_for_encoding.
+    lists:foreach(fun({ShortName, _}) ->
+        node_debug("enabling register_pid_for_encoding at node ~p", [ShortName]),
+        ok = rpc:call(?NAME(ShortName), partisan_config, set, [register_pid_for_encoding, true])
+    end, Nodes),
+
     %% Load, configure, and start zraft.
     lists:foreach(fun({ShortName, _}) ->
         % node_debug("starting zraft_lib at node ~p", [ShortName]),

-Original file line number
+Diff line change
@@ @@ -0,0 +1,4 @@ @@
 +[
 +  {causality, []},
 +  {background, []}
 +].