Concuerror assumes instant delivery of {'DOWN', _Mref, ..., noproc} message

[ieQu1]

Describe the bug
It looks like Concuerror assumes that DOWN messages are delivered instantaneously.
Consider the following testcase:

monitor_test() ->
  %% Preparation:
  %%   Create a process:
  Pid = spawn(fun() -> ok end),
  %%   Make sure it's dead:
  MRef1 = monitor(process, Pid),
  receive {'DOWN', MRef1, _, _, _} -> ok end,
  %% Actual test:
  MRef2 = monitor(process, Pid),
  ?assertMatch(received,
               receive
                 {'DOWN', MRef2, _, _, noproc} ->
                   received
               after 0 ->
                   not_received
               end).

This assertion shouldn't hold, because BEAM doesn't guarantee that the second DOWN message will arrive immediately.

To Reproduce
I'm using fairly standard CLI options:

CONCUERROR := $(BUILD_DIR)/Concuerror/bin/concuerror
CONCUERROR_RUN := $(CONCUERROR) \
	-x code -x code_server -x error_handler \
	-pa $(BUILD_DIR)/concuerror+test/lib/optvar/ebin

# Run test:
.PHONY: concuerror_test
concuerror_test: $(CONCUERROR)
	rebar3 as concuerror eunit -m concuerror_tests || true # Actual eunit test fails
	$(call concuerror,monitor_test)

# Recipe to build concuerror
$(CONCUERROR):
	mkdir -p _build/
	cd _build && git clone https://github.com/parapluu/Concuerror.git
	$(MAKE) -C _build/Concuerror/

Erlang version:

Erlang/OTP 25 [erts-13.2.2] [emqx-8639768b7a] [64-bit] [smp:16:16] [ds:16:16:10] [async-threads:1] [jit:ns]

Also reproduces on the upstream OTP26 version.

Expected behavior
Concuerror explores both branches of the receive.
Assertion fails with value not_delivered.

Environment (please complete the following information):

• OS: Linux 5.15.0-76-generic #83-Ubuntu SMP Thu Jun 15 19:16:32 UTC 2023 x86_64 x86_64 x86_64 GNU/Linux
• Concuerror Version: Concuerror 0.21.0+build.2371.refaf91d78

Additional context

[aronisstav]

Thank you for the report, @ieQu1 !

However, have you tested this also with --instant_delivery false?
I suspect that you should get the behavior you expect if you do so, which might be enough for any tests/models you want to write.

[ieQu1]

Hi,

Yes, in fact I did try to disable instant delivery, but strangely enough I got the same result:

_build/Concuerror/bin/concuerror --instant_delivery false -x code -x code_server -x error_handler -pa _build/concuerror+test/lib/optvar/ebin -f _build/concuerror+test/lib/optvar/test/concuerror_tests.beam -t monitor_test || { cat concuerror_report.txt; exit 1; }
Concuerror 0.21.0+build.2371.refaf91d78 started at 02 Aug 2023 00:13:08

* Info: Showing progress ('-h progress', for details)
* Info: Writing results in concuerror_report.txt
* Info: Only logging errors ('--log_all false')
* Info: Automatically instrumented module io_lib
* Info: Showing PIDs as "<symbolic name(/last registered name)>" ('-h symbolic_names').
* Info: "-pa" converted to "--pa"
* Warning: Not instrumenting module code
* Warning: Not instrumenting module code_server
* Warning: Not instrumenting module error_handler
* Info: Instrumented & loaded module concuerror_tests
* Tip: Check `--help attributes' for info on how to pass options via module attributes.
* Info: Automatically instrumented module erlang
* Tip: Running without a scheduling_bound corresponds to verification and may take a long time.
* Info: You can see pairs of racing instructions (in the report and '--graph') with '--show_races true'
Done at 02 Aug 2023 00:13:09 (Exit status: ok)
  Summary: 0 errors, 2/2 interleavings explored