Cryptol RPC server sometimes hangs

[atomb]

We've seen mention of cases where the Cryptol RPC server can hang when loading Cryptol modules, but haven't been able to reproduce it locally yet.

@pnwamk, do you have some more detail you can fill in?

[pnwamk]

As it was described to me, the client hangs on c.load_module() after having successfully loading many previous modules in a script such as the following while the server is running in a docker container:

import cryptol
import os

# Steps to clone example repo and set up server:

# git clone https://github.com/GaloisInc/cryptol-specs.git
# git checkout rpc-load-module-test

# docker run --rm -ti \
# -v $PWD/Common:/cryptol/Common \
# -v $PWD/Primitive:/cryptol/Primitive \
# -v $PWD/McEliece_KEM:/cryptol/McEliece_KEM \
# -p 8080:8080 \
# -e CRYPTOLPATH='/cryptol' \
# ghcr.io/galoisinc/cryptol-remote-api:nightly


# After server is running, simply execute this script, e.g.:
# python3 load.py

c = cryptol.connect(url="http://localhost:8080", reset_server=True)

for root, dir, files in os.walk("."):
    for name in files:
        if name.endswith(".cry"):
            new_file = os.path.join(root, name)[2:-4].replace("/", "::")
            print("Loading ", new_file, flush=True)
            c.load_module(new_file).result()
            c.reset_server()

N.B., the above script and it's accompanying instructions don't quite work as is, as the cryptol-specs repository has some modules that fail to load at present.

[pnwamk]

This may be reproducing the error we've had reported. At least observationally it appears similar:

# Steps to clone example repo and set up server:

# git clone https://github.com/GaloisInc/BLST-Verification.git
# cd BLST-Verification
# git submodule update --init

# docker run --rm -ti \
# -v $PWD/spec:/cryptol/spec \
# -v $PWD/cryptol-specs:/cryptol/cryptol-specs \
# -p 8080:8080 \
# -e CRYPTOLPATH='/cryptol/spec:/cryptol/cryptol-specs' \
# ghcr.io/galoisinc/cryptol-remote-api:nightly


# After server is running, simply execute the following script from the `spec` directory, e.g.:
# cd spec
# curl -o load.py https://gist.githubusercontent.com/pnwamk/e2173de4e1d8c69e389cdb9680a80915/raw/dc0a3f4006bd0eab84f9dde4246baf44f106a4ce/load.py
# python3 load.py
import cryptol
import os

c = cryptol.connect(url="http://localhost:8080", reset_server=True)

for root, dir, files in os.walk("."):
    for name in files:
        if name.endswith(".cry"):
            new_file = os.path.join(root, name)[2:-4].replace("/", "::")
            print(f'Loading {new_file}... ', flush=True, end='')
            c.load_module(new_file).result()
            print("done!", flush=True)
            c.reset_server()

It happily loads module after module until it gets to keygen_implementation, at which point it hangs. If you change the script so that, instead of loading modules in a loop, it only loads that file, i.e.:

c.load_module('keygen_implementation').result()

then you immediately get an error reported from the server regarding an error that occurred while loading:

$ python3 load.py
Traceback (most recent call last):
  File "/Users/andrew/Repos/GRINDSTONE/client-debug/BLST-Verification/spec/load.py", line 24, in <module>
    c.load_module('keygen_implementation').result()
  File "/usr/local/lib/python3.9/site-packages/argo_client/interaction.py", line 168, in result
    return self.process_result(self._result_and_state_and_out_err()[0])
  File "/usr/local/lib/python3.9/site-packages/argo_client/interaction.py", line 153, in _result_and_state_and_out_err
    raise self.process_error(exception)
argo_client.interaction.ArgoException: [error] :1:1--1:1:
    File name does not match module name:
    Saw: Main
    Expected: keygen_implementation

So, my currently hypothesis is that something exceptional is happening in the server but for some reason the error sometimes isn't properly getting reported/received/etc.

Will have to dig a little deeper.

Semi-related: some updates to both the cryptol server and client are about to land which should hopefully make it easier to narrow these kinds of errors without necessarily rebuilding the server to add log statements. (Well we'll see if it helps in this particular case I guess...)

[pnwamk]

I believe we confirmed in all the observed cases where this was occurring, it was related to SMT solvers hanging on the server side. #1258 appears to effectively help mitigate this.

[weaversa]

Thank you @pnwamk!