AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
104 stars 6 forks source link

Use `why3server` #1263

Closed treiher closed 1 year ago

treiher commented 1 year ago

The use of why3server could allow running multiple gnatprove instances in parallel without the potential issue of getting a memory shortage due to too many provers running in parallel.

treiher commented 1 year ago

Unfortunately, using why3server -j $(nproc) with gnatprove -j 1 does not sufficiently reduce the required memory.

Failing CI test: https://github.com/Componolit/RecordFlux/actions/runs/3621700551/jobs/6105479206 Used setup: https://github.com/Componolit/RecordFlux/blob/ba411ffdb2b6627125b245e3600442ed36f2d28c/Makefile#L180-L186

treiher commented 1 year ago

With the current configuration, two gnatprove processes are run in parallel. At most, two provers (due to why3server -j 2) and two gnatwhy3 process (due to two parallel gnatprove -j 1) are run in parallel.

I discussed the issue with @kanigsson. We see only two options:

  1. Try to reduce --memlimit to reduce the memory required by gnatwhy3.
  2. Only run one gnatprove instance (no why3server needed).
treiher commented 1 year ago

Reducing --memlimit works. I will create a PR for allowing multiple parallel GNATprove processes. But I do not see an advantage in using a why3server when running GNATprove with -j 1, which restricts GNATprove to just use one gnatwhy3 or one prover in parallel, as parallelization is only achieved by multiple GNATprove processes. So I think it doesn't make sense to follow this route, as long as there is no possibility to limit the number of gnatwhy3 processes independently of the number of parallel provers.