Parallel crash fix, #224

src/proper_statem.erl

@@ -603,7 +603,8 @@ safe_apply(M, F, A) ->
 %%   concurrent tasks.</li>
 %% <li>`Result' specifies the outcome of the attemp to serialize command
 %%   execution, based on the results observed. It can be one of the following:
-%%   <ul><li> `ok' </li><li> `no_possible_interleaving' </li></ul> </li>
+%%   <ul><li> `ok' </li><li> `no_possible_interleaving' </li>
+%%   <li> `{exception, Kind, Reason, StackTrace}' </li></ul> </li>
 %% </ul>
 
 -spec run_parallel_commands(mod_name(), parallel_testcase()) ->
@@ -620,52 +621,78 @@ run_parallel_commands(Mod, {_Sequential, _Parallel} = Testcase) ->
 	 {history(),[parallel_history()],statem_result()}.
 run_parallel_commands(Mod, {Sequential, Parallel}, Env) ->
     case run(Mod, Sequential, Env) of
-	{{Seq_history, State, ok}, SeqEnv} ->
-	    F = fun(T) -> execute(T, SeqEnv, Mod) end,
-	    Parallel_history = pmap(F, Parallel),
-	    case check(Mod, State, SeqEnv, false, [], Parallel_history) of
-		true ->
-		    {Seq_history, Parallel_history, ok};
-		false ->
-		    {Seq_history, Parallel_history, no_possible_interleaving}
-	    end;
-	{{Seq_history, _, Res}, _} ->
-	    {Seq_history, [], Res}
+    {{Seq_history, State, ok}, SeqEnv} ->
+        F = fun(T) -> execute(T, SeqEnv, Mod) end,
+        case pmap(F, Parallel) of
+        {ok, Parallel_history} ->
+            case check(Mod, State, SeqEnv, false, [], Parallel_history) of
+            true ->
+                {Seq_history, Parallel_history, ok};
+            false ->
+                {Seq_history, Parallel_history,
+                 no_possible_interleaving}
+            end;
+        {error, Exc, Parallel_history} ->
+            {Seq_history, Parallel_history, Exc}
+        end;
+    {{Seq_history, _, Res}, _} ->
+        {Seq_history, [], Res}
     end.
 
 %% @private
 -spec execute(command_list(), proper_symb:var_values(), mod_name()) ->
-	 parallel_history().
-execute([], _Env, _Mod) -> [];
-execute([{set, {var,V}, {call,M,F,A}} = Cmd|Rest], Env, Mod) ->
+                     {ok, parallel_history()} | {error, term(), parallel_history()}.
+execute(Cmds, Env, Mod) -> execute(Cmds, Env, Mod, []).
+
+-spec execute(command_list(), proper_symb:var_values(), mod_name(),
+              parallel_history()) -> {ok, parallel_history()} |
+                                     {error, proper:exception(), parallel_history()}.
+execute([], _Env, _Mod, Hist) -> {ok,lists:reverse(Hist)};
+execute([{set, {var,V}, {call,M,F,A}} = Cmd|Rest], Env, Mod, Hist) ->
     M2 = proper_symb:eval(Env, M),
     F2 = proper_symb:eval(Env, F),
     A2 = proper_symb:eval(Env, A),
-    Res = apply(M2, F2, A2),
-    Env2 = [{V,Res}|Env],
-    [{Cmd,Res}|execute(Rest, Env2, Mod)].
+
+    case safe_apply(M2, F2, A2) of
+    {ok,Res} ->
+        Env2 = [{V,Res}|Env],
+        execute(Rest, Env2, Mod, [{Cmd,Res}|Hist]);
+    {error, Exc} ->
+        {error, Exc, lists:reverse(Hist)}
+    end.
 
 -spec pmap(fun((command_list()) -> parallel_history()), [command_list()]) ->
-         [parallel_history()].
+                  {ok, [parallel_history()]} |
+                  {error, proper:exception(), [parallel_history()]}.
 pmap(F, L) ->
     await(spawn_jobs(F, L)).
 
 -spec spawn_jobs(fun((command_list()) -> parallel_history()),
 		 [command_list()]) -> [pid()].
 spawn_jobs(F, L) ->
     Parent = self(),
-    [spawn_link_cp(fun() -> Parent ! {self(),catch {ok,F(X)}} end) || X <- L].
-
--spec await([pid()]) -> [parallel_history()].
-await([]) -> [];
-await([H|T]) ->
+    [spawn_link_cp(fun() -> Parent ! {self(), F(X)} end) || X <- L].
+
+-spec await([pid()]) ->
+                   {ok, [parallel_history()]} |
+                   {error, proper:exception(), [parallel_history()]}.
+await(Pids) -> await(Pids, [], false).
+
+-spec await([pid()], [parallel_history()], false | proper:exception()) ->
+                   {ok, [parallel_history()]} |
+                   {error, proper:exception(), [parallel_history()]}.
+await([], Hist, false) -> {ok, lists:reverse(Hist)};
+await([], Hist, Exc) -> {error, Exc, lists:reverse(Hist)};
+await([H|T], Hist, MaybeExc) ->
     receive
-	{H, {ok, Res}} ->
-        [Res|await(T)];
-	{H, {'EXIT',_} = Err} ->
-	    _ = [exit(Pid, kill) || Pid <- T],
-	    _ = [receive {P,_} -> d_ after 0 -> i_ end || P <- T],
-	    erlang:error(Err)
+    {H, {ok, Res}} ->
+        await(T, [Res|Hist], MaybeExc);
+    {H, {error, Exc, Res}} ->
+        Exc2 = case MaybeExc of
+                   false -> Exc;
+                   E -> E
+               end,
+        await(T, [Res|Hist], Exc2)
     end.
 
 %% @private

test/command_props.erl

@@ -110,7 +110,7 @@ prop_check_true() ->
 		?MOD:clean_up(),
 		?MOD:set_up(),
 		{{_, State, ok}, Env} = proper_statem:run(?MOD, Seq, []),
-		Res = [proper_statem:execute(C, Env, ?MOD) || C <- Par],
+		Res = [begin {ok, R}=proper_statem:execute(C, Env, ?MOD), R end || C <- Par],
 		V = proper_statem:check(?MOD, State, Env, false, [], Res),
 		equals(V, true)
 	    end).

test/parallel_statem.erl

@@ -0,0 +1,77 @@
+%%% -*- coding: utf-8 -*-
+%%% -*- erlang-indent-level: 2 -*-
+%%% -------------------------------------------------------------------
+%%% From X4lldux
+%%%
+%%% When there was a crash in sequential phase of `run_parallel_commands`
+%%% the returned result was `{exception,_,_,_}` tuple, but when a crash
+%%% occurred in the parallel phase, then the `run_parallel_commands`
+%%% also crashed.
+%%%
+%%% -------------------------------------------------------------------
+
+-module(parallel_statem).
+
+%% -compile(export_all).
+-export([initial_state/0, next_state/3, precondition/2, postcondition/3]).
+-export([foo/1, crash/0]).
+-export([prop_parallel_crash/0, prop_sequential_crash/0]).
+
+-include_lib("proper/include/proper.hrl").
+
+
+initial_state() ->
+    [].
+
+precondition(_, _) ->
+    true.
+
+next_state(S, _V, {call,_,_,[_Arg]}) ->
+    S.
+
+postcondition(_, _, _) ->
+    true.
+
+foo(_) ->
+    ok.
+
+crash() ->
+    erlang:error(boom).
+
+
+parallel_crash_commands() ->
+    exactly(
+      {
+       [{set,{var,1},{call,?MODULE,foo,[1]}}],       % seq
+       [
+        [{set,{var,2},{call,?MODULE,crash,[]}}],     % proc 1
+        []                                           % proc 2
+       ]
+      }).
+
+sequential_crash_commands() ->
+    exactly(
+      {
+       [{set,{var,1},{call,?MODULE,crash,[]}}],      % seq
+       [
+        [{set,{var,2},{call,?MODULE,foo,[1]}}],      % proc 1
+        []                                           % proc 2
+       ]
+      }).
+
+prop_parallel_crash() ->
+    ?FORALL(Cmds, parallel_crash_commands(),
+            begin
+                {_S,_P,Res} = run_parallel_commands(?MODULE, Cmds),
+                assert_exception(Res)
+            end).
+
+prop_sequential_crash() ->
+    ?FORALL(Cmds, sequential_crash_commands(),
+            begin
+                {_S,_P,Res} = run_parallel_commands(?MODULE, Cmds),
+                assert_exception(Res)
+            end).
+
+assert_exception({exception, error, boom, _}) -> true;
+assert_exception(_) -> false.

test/proper_tests.erl

@@ -898,6 +898,10 @@ native_type_props_test_() ->
 -record(untyped, {a, b = 12}).
 -type untyped() :: #untyped{}.
 
+parallel_statem_test_() ->
+    [?_passes(parallel_statem:prop_parallel_crash()),
+     ?_passes(parallel_statem:prop_sequential_crash())].
+
 true_props_test_() ->
     [?_passes(?FORALL(X,integer(),X < X + 1)),
      ?_passes(?FORALL(A,atom(),list_to_atom(atom_to_list(A)) =:= A)),