-
Notifications
You must be signed in to change notification settings - Fork 41
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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 crashed
error 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.refedc846d
Additional context
This apparently is related to restarting a named process, and also to some internal process in Concuerror that injects
rand_seed
into the process dictionary. After the process is restarted during exploration, it lacksrand_seed
and thereplay_mismatch
error 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: