Date: Sat, 02 Sep 2023 10:47:03 +0000 From: "Mathew\, Cherry G.*" <c@bow.st> To: Alexander Leidinger <Alexander@Leidinger.net>, adridg@freebsd.org Cc: freebsd-hackers@freebsd.org Subject: Re: ARC model specified in spinroot/promela Message-ID: <858r9o6ee0.fsf@bow.st> In-Reply-To: <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> (Alexander Leidinger's message of "Sat, 02 Sep 2023 10:23:43 %2B0200") References: <85jzt96qjz.fsf@bow.st> <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net>
next in thread | previous in thread | raw e-mail | index | archive | help
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).
If all goes well with step 3) , then you will see a summary of the run
on console. However, if there was an inconsistency or error detected in
the run, then a tracefile is generated (spinmodel.pml.trail). I've
included a target to dump a human friendly version of this trace.
4) Print trace from debug trail: make spin-trace
AL> Note, the Makefile specifies a NetBSD src directory which I
AL> don't have on this FreeBSD system...
Sorry, I should have mentioned - you can safely ignore that - no
specific external source layout is currently assumed - in fact I run
these tests on a Linux VM at the moment.
The source files become relevant only when the "model extraction" is
done - I haven't got there yet for this project.
>>>>> "ade" == Adriaan de Groot <adridg@freebsd.org> writes:
ade> For what it's worth, spin is available from ports (devel/spin),
ade> which I've just adopted and updated to 6.5.2, so it is quite
ade> straightforward to get this running on any recent FreeBSD
ade> system.
Hi ade,
Nice! I'd be curious to know performance comparisons viz Linux etc. esp
because there seems to be a threaded version of spin (not sure if the
FreeBSD package build enables this).
ade> I tested only with the ancient Peterson's mutual exclusion,
ade> which resolves instantly. Mailing-list archives don't preserve
ade> attachments, so, Cherry, if you could send it me directly that
ade> would be lovely. I spotted A. Mader's PLC Controller in the
ade> SPIN documents, that is one I am familiar with, and then
ade> realised that academic papers from the 2000s don't come with
ade> source code :(
Thanks, I noticed that after checking the archives, and did send a
second mail with an inline patch. Will also send you a private one after
this.
Thanks so much for your interest - mainly, I'd like to understand how
bad the statespace explosion is for this model. This will help me get a
sense of what complexity of models we can attempt to verify like this,
with current "commodity" hardware.
Many Thanks,
--
~cherry
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?858r9o6ee0.fsf>