Segmentation fault (core dumped)

[Gizzbow]

When I run the example in the attached folder, Marabou throws a segmentation error. bug1.zip

System Specification: Processor Intel(R) Core(TM) i7-7600U CPU @ 2.80GHz 2.90 GHz Installed RAM 16.0 GB (15.8 GB usable) System type 64-bit operating system, x64-based processor Edition Windows 10 Pro Version 22H2 Experience Windows Feature Experience Pack 1000.19054.1000.0 WSL version 2.1.5.0 Linux kernel version 5.15.146.1-2. Marabou was built using cmake and not pip installed. Please ask if you need any more information.

[wu-haoze]

Hi @Gizzbow , I think this is a out-of-memory issue. If you run

/usr/bin/time -v ../build/Marabou 6126643203156728210/mnist-classifier.onnx 6126643203156728210/robust-query1.txt

I suspect the "Maximum resident set size (kbytes)" is going to be very close to 15.8GB.

I tride your query on a machine with 64 GB, it's able to start solving. I would suggest compile Marabou with Gurobi to improve runtime performance: https://github.com/NeuralNetworkVerification/Marabou#compile-marabou-with-the-gurobi-optimizer-optional

Regardless of compiling with Gurobi or not, you could try multi-threading the abstract interpretation by:

/usr/bin/time -v ../build/Marabou 6126643203156728210/mnist-classifier.onnx 6126643203156728210/robust-query1.txt --num-workers=[number of threads]

After compiling with Gurobi, you could additionally try:

/usr/bin/time -v ../build/Marabou 6126643203156728210/mnist-classifier.onnx 6126643203156728210/robust-query1.txt --num-workers=[number of threads] --milp

[Gizzbow]

It seems like for both of the commands (without Gurobi), it still givew a signal 11 error.

I will update again once I get Gurobi,

[MatthewDaggitt]

I'm pretty sure a signal 11 fault does suggest a segmentation fault rather than out of memory error (signal 9?), but maybe Marabou does something weird with errors?

[wu-haoze]

@Gizzbow I think this is indeed a segfault instead of out-of-memory error. That's interesting because on my machine with 32 GB RAM, I got a memout before hitting this segfault. It seems that the segfault happens after Marbou runs for 6 minutes or so? If so could you send me Marabou's output?

[Gizzbow]

I got Gorubi Academic License and built Marabou with it. It seems to work just fine even when not using --milp. So, maybe there was something wrong with my build previously?

[wu-haoze]

@Gizzbow , good to know with Gurobi you are able to solve the query. When built with Gurobi, even without the --milp flag, Marabou still makes use of Gurobi: it will run the native verification procedure using Gurobi as the LP (not MILP) solver.

I think if you run

../build/Marabou 6126643203156728210/mnist-classifier.onnx 6126643203156728210/robust-query1.txt --lp-solver=native you would get the same issue as before, because that additional flag would use the native LP implementation, which on larger instances, can get a little finicky and requires some tuning of the parameters in src/configurations/GlobalConfigurations.h.

[wu-haoze]

Closing the issue due to inactivity. Feel free to re-open.