Skip to content

Python crash in ./run-cbmc-proofs.py -jN when N is large #235

@rod-chapman

Description

@rod-chapman

In the proof of the mldsa-native project, running the run-cbmc-proofs.py script with -jN
for N >= 2, we always see a Python crash (exactly once per run). For example, on an EC2 r7g.16xlarge instance
with 64 cores, and running CBMC 6.8.0:

$ time ./run-cbmc-proofs.py --summarize --no-coverage -j64

For your convenience, the output of this run will be symbolically linked to  /home/ubuntu/pqcp/mldref/proofs/cbmc/output/latest/html/index.html 

Configuring CBMC proofs: 138 / 138
[1145/2071] crypto_sign_keypair: checking function contracts                                                                                  Contract 'randombytes' not found, deriving empty pure contract 'contract::randombytes' from function 'randombytes'

[1824/2071] polyveck_unpack_t0: checking safety properties                                                                                    Exception ignored in: <function BaseSubprocessTransport.__del__ at 0xfffff61d6b60>

Traceback (most recent call last):

  File "/nix/store/40qg7a2iaxnxkra9wk327xi50687pap9-python3-3.12.11/lib/python3.12/asyncio/base_subprocess.py", line 126, in __del__

    self.close()

  File "/nix/store/40qg7a2iaxnxkra9wk327xi50687pap9-python3-3.12.11/lib/python3.12/asyncio/base_subprocess.py", line 104, in close

    proto.pipe.close()

  File "/nix/store/40qg7a2iaxnxkra9wk327xi50687pap9-python3-3.12.11/lib/python3.12/asyncio/unix_events.py", line 568, in close

    self._close(None)

  File "/nix/store/40qg7a2iaxnxkra9wk327xi50687pap9-python3-3.12.11/lib/python3.12/asyncio/unix_events.py", line 592, in _close

    self._loop.call_soon(self._call_connection_lost, exc)

  File "/nix/store/40qg7a2iaxnxkra9wk327xi50687pap9-python3-3.12.11/lib/python3.12/asyncio/base_events.py", line 799, in call_soon

    self._check_closed()

  File "/nix/store/40qg7a2iaxnxkra9wk327xi50687pap9-python3-3.12.11/lib/python3.12/asyncio/base_events.py", line 545, in _check_closed

    raise RuntimeError('Event loop is closed')

RuntimeError: Event loop is closed

This "event loop is closed" appears to be a common problem with concurrent programming in Python.

Can it be fixed please?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions