Backend bug-reporting broken due to request enumeration being reset

[PetarMax]

When running a proof in Kontrol, I obtained the following transcript:

INFO 2024-06-25 12:49:42,378 pyk.kore.rpc - Sending request to localhost:63691: 1 - add-module
INFO 2024-06-25 12:49:42,388 pyk.utils - Added file to bug report report.tar:rpc_contracts%model%TestContract.test_function():0/001_request.json: /var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T/tmp0hu85pb0
INFO 2024-06-25 12:49:42,391 pyk.utils - Added file to bug report report.tar:commands/000.sh: /var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T/tmpb30mcxu6
[proxy] Processing request 1
INFO 2024-06-25 12:49:44,773 pyk.utils - Added file to bug report report.tar:rpc_contracts%model%TestContract.test_function():0/001_response.json: /var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T/tmpi_tbcqf1
INFO 2024-06-25 12:49:44,774 pyk.utils - Added file to bug report report.tar:commands/001.sh: /var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T/tmp49hcofxp
INFO 2024-06-25 12:49:44,774 pyk.kore.rpc - Received response from localhost:63691: 1 - add-module
INFO 2024-06-25 12:49:44,862 pyk.kore.rpc - Sending request to localhost:63691: 2 - add-module
INFO 2024-06-25 12:49:44,866 pyk.utils - Added file to bug report report.tar:rpc_contracts%model%TestContract.test_function():0/002_request.json: /var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T/tmpxatv6btc
INFO 2024-06-25 12:49:44,867 pyk.utils - Added file to bug report report.tar:commands/002.sh: /var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T/tmpeolr2l1s
[proxy] Processing request 2
INFO 2024-06-25 12:49:46,644 pyk.utils - Added file to bug report report.tar:rpc_contracts%model%TestContract.test_function():0/002_response.json: /var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T/tmpmmfm1z02
INFO 2024-06-25 12:49:46,646 pyk.utils - Added file to bug report report.tar:commands/003.sh: /var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T/tmpkj2k4cih
INFO 2024-06-25 12:49:46,646 pyk.kore.rpc - Received response from localhost:63691: 2 - add-module
INFO 2024-06-25 12:49:46,654 pyk.kore.rpc - Connecting to host: localhost:63691
INFO 2024-06-25 12:49:46,655 pyk.kore.rpc - Connected to host: localhost:63691
INFO 2024-06-25 12:49:47,035 pyk.kore.rpc - Sending request to localhost:63691: 1 - execute
INFO 2024-06-25 12:49:47,043 pyk.utils - Added file to bug report report.tar:rpc_contracts%model%TestContract.test_function():0/001_request.json: /var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T/tmpyiceo5tt
INFO 2024-06-25 12:49:47,045 pyk.utils - Added file to bug report report.tar:commands/004.sh: /var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T/tmp_50b95ei
[proxy] Processing request 1

which means that the request enumeration is reset after the first two requests, resulting in the third request being marked as request 1, overwriting the original request 1 and corrupting the bug report.

[tothtamas28]

I wonder why the request ID is reset for a given client. Perhaps it's related to parallel exploration, @nwatson22, can you look into this?

[PetarMax]

I can confirm that parallel exploration does result in requests with same identifiers, starting from 1 for each thread. In this specific case, I did not use parallel exploration.

[nwatson22]

This is indeed parallelization related. The issue is because there are multiple KoreClients which each have their own bug report. Every BugReport has a _command_id which it increments internally for each command it outputs. Even in the 1-worker case, there is one for the main thread, which is sending these add-module requests and one for the one worker. I think we need to change the way bug reports work so, e.g., there is a shared command ID being accessed with synchronization primitives.

Edit: I was too hasty, this is not quite right. It's actually _req_id in JsonRPCClient which is being reset. However, the _command_id could cause a race condition in the > 1 worker case because we are actually passing the same BugReport object to different clients making requests on different threads.

[tothtamas28]

However, the _command_id could cause a race condition in the > 1 worker case because we are actually passing the same BugReport object to different clients making requests on different threads.

Are these commands not logged under a directory within the BugReport unique to the client?

It's actually _req_id in JsonRPCClient which is being reset.

Where does this occur?

[nwatson22]

Are these commands not logged under a directory within the BugReport unique to the client?

@tothtamas28 Right now the BugReport is not unique. All the clients are pointing to the same BugReport object.

Where does this occur?

In parallel_advance_proof where we call with create_prover() as main_prover: it creates one prover with one new underlying JsonRpcClient, and then creates a second prover with a second JsonRpcClient in _ProverPool._with_prover() for the worker thread. Each of these JsonRpcClients tracks its own _req_id starting from 1.