Date: Sat, 02 Sep 2023 10:23:43 +0200 From: Alexander Leidinger <Alexander@Leidinger.net> To: "Mathew, Cherry G.*" <c@bow.st> Cc: freebsd-hackers@freebsd.org Subject: Re: ARC model specified in spinroot/promela Message-ID: <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> In-Reply-To: <85jzt96qjz.fsf@bow.st> References: <85jzt96qjz.fsf@bow.st>
next in thread | previous in thread | raw e-mail | index | archive | help
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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?9c424a574cdd39fc879c9ed9192556c0>