is it possible to restrict eldarica to one thread?

[dbueno]

I've looked through the options and the code a little but didn't find anything. Is there a way to run eldarica so that it only uses one thread, regardless of how many cores are available on the machine?

[pruemmer]

At the moment there is no such option. What is the use case of this? Eldarica (at least with the default settings) does not by itself use multiple threads/cores, but the JVM will spawn several threads to take care of garbage collection, etc. CPU loads >100% tend to occur mostly during the first couple of seconds of Eldarica running. One could make sure that all threads execute on only a single core through tools like benchexec, if this is an important for benchmarking.

[dbueno]

I should have said: the use case, ultimately, is benchmarking. Right now I am only trying to get an idea of how hard some instances are.

I ran, in parallel, 30 difficult-ish instances of eldarica on a 64-core machine; within 30 minutes the load average was ~950. (None had solved within 30 minutes.) So, really, I was wondering why there were so many processes spawned by eldarica. Is this behavior expected?

(I realize now I asked about threads but really I wanted to know about processes. Sorry about that.)

I don't have any experience with benchexec. I was able to get what I needed quickly in other ways, at least until now. Do you recommend benchexec for ensuring all the threads/processes use one core?

[pruemmer]

Can you test which load you get with just a single process? The behavior you describe might be due to some of the instances running out of memory. In those cases the GC threads tend to consume a lot of CPU. You could try increasing the heap memory limit in “eldEnv” (option -Xmx).

[dbueno]

I tested just one process. The load average climbed to 40 after about 3 minutes.

I changed the Java parameters to -Xmx8192m -Xss80000k; just multiplied by 4.

The load average climbed to 40 after about 4 minutes.

[pruemmer]

Interesting, I don’t think I have seen this behavior before. If you can make any test case available that reproduces it, that would be great!