replaying a built-in returned a different result than expected when a process is restarted
#360
Comments
|
Hi! Definitely a bug, but the suggested fix breaks the fundamental assumption that "functions that can return different results shouldn't do so on replays" (otherwise we can't be sure we are "back" at the same state), so it cannot be used. The right fix requires to find the builtin op that has been missed (or identify why concuerror injected the rand_seed) and will be more involved... I may be able to suggest workarounds if you can share some relatively minimal example that breaks, but I can't promise a lot these days. |
|
Hi! I didn't suggest the patch above as a fix at all, it's not a proper fix. 😅 I already shared an example in the issue that breaks without the patch at the current HEAD of the repo. Would you need for it to be even smaller? |
|
I shrank the example module a bit more, hope it helps. 🤞 /tmp/test.erl-module(test).
%% rm concuerror_report.txt; clear; (bin/concuerror -f /tmp/test.erl -t spin_down_test --treat-as-normal spindown --treat_as_normal shutdown -x error_handler -x logger || {cat concuerror_report.txt; exit 1})
-compile([export_all]).
start_monitor() ->
gen_server:start_monitor({local, ?MODULE}, ?MODULE, [], []).
ensure_started() ->
case start_monitor() of
{ok, _} ->
ok;
{error, {already_started, _}} ->
ok
end.
stop() ->
catch gen_server:stop(?MODULE),
ok.
request(X) ->
case whereis(?MODULE) of
undefined ->
ok = ensure_started(),
request(X);
Pid ->
Ref = monitor(process, Pid),
Pid ! {req, Ref, self(), X},
receive
{Ref, Resp} ->
Resp;
{'DOWN', Ref, process, _Pid, spindown} ->
ok = ensure_started(),
request(X);
{'DOWN', Ref, process, _Pid, noproc} ->
ok = ensure_started(),
request(X)
end
end.
init(_) ->
{ok, #{}}.
handle_cast(spindown, State) ->
{stop, spindown, State}.
handle_info({req, Ref, From, _X}, State) ->
From ! {Ref, ok},
{noreply, State};
handle_info(_, State) ->
{noreply, State}.
spin_down_test() ->
Me = self(),
spawn(fun() ->
Resp = request(go),
Me ! {ok, Resp}
end),
spawn(fun() ->
Resp = request(go),
Me ! {ok, Resp}
end),
spawn(fun() ->
gen_server:cast(?MODULE, spindown)
end),
receive
{ok, _} -> ok
end,
receive
{ok, _} -> ok
end,
stop(),
ok. |
Describe the bug
While trying to model an algorithm where a named process is restarted, I get a
Concuerror crashederror that saysreplaying a built-in returned a different result than expected.To Reproduce
Steps to reproduce the behavior:
Module with code and test at `/tmp/test.erl`
Concuerror command:
Output
concuerror_report.txt
Highlighting the main error:
Expected behavior
There should be no replay mismatch mentioning
rand_seed, since it's not used. I've tried setting it explicitly to a fixed value when initializing the gen_server process, but I still get a replay mismatch.Environment (please complete the following information):
Concuerror 0.21.0+build.2381.refedc846dAdditional context
This apparently is related to restarting a named process, and also to some internal process in Concuerror that injects
rand_seedinto the process dictionary. After the process is restarted during exploration, it lacksrand_seedand thereplay_mismatcherror is hit.Using the following patch, the model is verified successfully. Of course, this is not a proper fix. But I don't expect that the correctness in this case relies on the process dictionary.
Output with patch
The text was updated successfully, but these errors were encountered: