Opened 11 months ago

Last modified 10 months ago

#44 new defect

Multi-Threaded Performance Doesn't Scale

Reported by: John Lång Owned by: mornfall
Priority: minor Milestone: 5.0
Component: other Keywords:


On my Debian laptop, I noticed that running divine check on my model took 30s for one thread, 23s for two threads, and 21s for four threads. The serial part in the beginning took around 10 seconds. I'm currently running divine check on a bigger model on a virtual machine (Also running Debian 9) with 32 CPUs and the performance, in terms of Mips and states per second, doesn't seem to be basically any better than with a single thread. It looks like all the CPU cores do produce heat, but they're spending most of the time in kernel space. Could there be a race for locks going on between the model checking threads or something?

My models are part of the ADAPRO project in GitLab?:
I wrote this nice BASH script for running DIVINE on them. It requires some extra utilities, like bc, pgrep, and gnuplot, though.

Change History (1)

comment:1 Changed 10 months ago by mornfall

Milestone: future5.0

Milestone renamed

Note: See TracTickets for help on using tickets.