Date: Sat, 02 Sep 2023 18:38:41 +0000 From: "Mathew\, Cherry G.*" <c@bow.st> To: Alexander Leidinger <Alexander@Leidinger.net> Cc: adridg@freebsd.org, freebsd-hackers@freebsd.org Subject: Re: ARC model specified in spinroot/promela Message-ID: <85pm304dzi.fsf@bow.st> In-Reply-To: <c2197ad9446eca4edae2db09a859d66b@Leidinger.net> (Alexander Leidinger's message of "Sat, 02 Sep 2023 19:12:24 %2B0200") References: <85jzt96qjz.fsf@bow.st> <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> <858r9o6ee0.fsf@bow.st> <c2197ad9446eca4edae2db09a859d66b@Leidinger.net>
next in thread | previous in thread | raw e-mail | index | archive | help
>>>>> Alexander Leidinger <Alexander@Leidinger.net> writes:
[...]
> Seems to be single threaded (Adrian, this is with spin 6.5.0 from
> an about 2 days old ports tree). Takes only 1 CPU. After 20min it
> is at 25G (20G RES). The system has 64G of RAM and 100G of swap,
> we will see if this is enough.
Thank you so much for this, and the trace output in the subsequent
email!
So there's room for improvement in my Makefile to:
1) Explore multithreaded/CPU
2) Understand state space explosion scale - it is exponential to the
number of processes, I've fixed it to run in a loop - will report
back once I have good progress also with the model extraction part.
3) My model has errors - I'm glad to see that the error reporting is the
same in my new optimised loop, as in the RAM hungry version you ran.
Thanks once again - this is very helpful. I will report back once I have
more progress.
--
~cherry
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?85pm304dzi.fsf>