diff --git a/src/proper_statem.erl b/src/proper_statem.erl index 96794985..117848a3 100644 --- a/src/proper_statem.erl +++ b/src/proper_statem.erl @@ -603,7 +603,8 @@ safe_apply(M, F, A) -> %% concurrent tasks. %%
  • `Result' specifies the outcome of the attemp to serialize command %% execution, based on the results observed. It can be one of the following: -%%
    • +%% %% -spec run_parallel_commands(mod_name(), parallel_testcase()) -> @@ -620,33 +621,49 @@ 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)). @@ -654,18 +671,28 @@ pmap(F, L) -> [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 diff --git a/test/command_props.erl b/test/command_props.erl index 7b9fe35e..d848088a 100644 --- a/test/command_props.erl +++ b/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). diff --git a/test/parallel_statem.erl b/test/parallel_statem.erl new file mode 100644 index 00000000..69f38e5b --- /dev/null +++ b/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. diff --git a/test/proper_tests.erl b/test/proper_tests.erl index 44429f95..cb9e764f 100644 --- a/test/proper_tests.erl +++ b/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)),