Skip site navigation (1)Skip section navigation (2)
Date:      Sat, 02 Sep 2023 19:12:24 +0200
From:      Alexander Leidinger <Alexander@Leidinger.net>
To:        "Mathew, Cherry G.*" <c@bow.st>
Cc:        adridg@freebsd.org, freebsd-hackers@freebsd.org
Subject:   Re: ARC model specified in spinroot/promela
Message-ID:  <c2197ad9446eca4edae2db09a859d66b@Leidinger.net>
In-Reply-To: <858r9o6ee0.fsf@bow.st>
References:  <85jzt96qjz.fsf@bow.st> <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> <858r9o6ee0.fsf@bow.st>

next in thread | previous in thread | raw e-mail | index | archive | help
Am 2023-09-02 12:47, schrieb Mathew, Cherry G.*:
> Hi Alexander,
> 
>>>>>> "AL" == Alexander Leidinger <Alexander@Leidinger.net> writes:
> 
> 
> [...]
> 
> 
>     AL> How long is this supposed to take? For me it took about 2
>     AL> seconds to finish.
> 
> Apologies, I should have given more detailed instructions.
> 
> I've organised the process in three steps:
> 
> 1) Generate the model from spec: make spin-gen
> 2) Build the model: make spin-build
> 3) Run the model: make spin-run
> 
> This is the heavy duty part, which takes up quite a bit of vmem (my
> process dies at about 8GB due to lack of swap etc. - makes no sense to
> thrash it beyond that without RAM - it slows down a lot).

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.

I will report back when it is finished.

Bye,
Alexander.

-- 
http://www.Leidinger.net Alexander@Leidinger.net: PGP 0x8F31830F9F2772BF
http://www.FreeBSD.org    netchild@FreeBSD.org  : PGP 0x8F31830F9F2772BF



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?c2197ad9446eca4edae2db09a859d66b>