Re: ARC model specified in spinroot/promela

Am 2023-09-02 08:24, schrieb Mathew, Cherry G.*:
> Hello hackers,
> 
> I'm writing to introduce a project I've been working on off-and-on for 
> a
> while now - verifying parts of kernel code using a formal specifier[1]
> 
> Please find attached a patch to try out a formal verification run of 
> the
> Adaptive Replacement Cache by Megido et.al. [2]
> 
> You can try it out by installing spin from your favourite package
> manager, and then running "make" in the current directory - it just
> needs the usual C toolchain, afaik.
> 
> I'm hoping that someone can help me complete the current run, as I 
> don't
> have the computing resources required to run the full model (about 16GB
> RAM). Meanwhile I'll keep finding ways to reduce the statespace
> required.

How long is this supposed to take? For me it took about 2 seconds to 
finish.
Note, the Makefile specifies a NetBSD src directory which I don't have 
on this FreeBSD system...

Samstag, 02. September 2023, 10:18:12
(235) root@ttypts/3 # make
cp arc.pml model #mimic modex
cat arc.drv > spinmodel.pml;cat model >> spinmodel.pml;cat arc.inv >> 
spinmodel.pml;
spin -a spinmodel.pml
ltl ltl_0: ((<> ([] ((_nr_pr==1)))) && ([] (((((len(T1.item_list)<=5)) 
&& ((len(B1.item_list)<=5))) && ((len(T2.item_list)<=5))) && 
((len(B2.item_list)<=5))))) && (<> ((p>0)))

Samstag, 02. September 2023, 10:18:14
(236) root@ttypts/3 # ll
total 275
-rw-r--r--  1 root wheel  1,1K  2 Sep. 10:18 _spin_nvr.tmp
-rw-r--r--  1 root wheel  2,6K  2 Sep. 10:15 arc.drv
-rw-r--r--  1 root wheel  555B  2 Sep. 10:15 arc.inv
-rw-r--r--  1 root wheel  4,6K  2 Sep. 10:15 arc.pml
-rw-r--r--  1 root wheel  3,3K  2 Sep. 10:15 Makefile
-rw-r--r--  1 root wheel  4,6K  2 Sep. 10:18 model
-rw-r--r--  1 root wheel  2,9K  2 Sep. 10:18 pan.b
-rw-r--r--  1 root wheel  335K  2 Sep. 10:18 pan.c
-rw-r--r--  1 root wheel   18K  2 Sep. 10:18 pan.h
-rw-r--r--  1 root wheel   42K  2 Sep. 10:18 pan.m
-rw-r--r--  1 root wheel   55K  2 Sep. 10:18 pan.p
-rw-r--r--  1 root wheel   30K  2 Sep. 10:18 pan.t
-rw-r--r--  1 root wheel  7,8K  2 Sep. 10:18 spinmodel.pml

Bye,
Alexander.

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