Opened 9 months ago

Last modified 9 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:
Cc:

Description

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?: https://gitlab.com/jllang/adapro
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 9 months ago by mornfall

Milestone: future5.0

Milestone renamed

Note: See TracTickets for help on using tickets.