From nobody Sat Sep 02 08:23:43 2023 X-Original-To: freebsd-hackers@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4Rd7Gj1pYwz4sMdm for ; Sat, 2 Sep 2023 08:24:13 +0000 (UTC) (envelope-from Alexander@Leidinger.net) Received: from mailgate.Leidinger.net (mailgate.leidinger.net [IPv6:2a00:1828:2000:313::1:5]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature ECDSA (P-256) client-digest SHA256) (Client CN "mailgate.leidinger.net", Issuer "R3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4Rd7Gh1KrCz3VrC for ; Sat, 2 Sep 2023 08:24:12 +0000 (UTC) (envelope-from Alexander@Leidinger.net) Authentication-Results: mx1.freebsd.org; none Received: from webmail2.leidinger.net (roundcube.Leidinger.net [192.168.1.123]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature ECDSA (prime256v1) server-digest SHA256) (Client did not present a certificate) (Authenticated sender: Alexander@Leidinger.net) by outgoing.leidinger.net (Postfix) with ESMTPSA id 204A7E944; Sat, 2 Sep 2023 10:23:44 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=leidinger.net; s=outgoing-alex; t=1693643033; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=GGXxohyLideG07ncKmZ+imAhqlSArWSZdg1aiKA/aRE=; b=0qpoAE+Q/9AIqRnVOzZBsjkvhoMxYu4BYnTBg6qWM1FF8IOzr7aB4sV7DN5Ha9mIeFrEK5 VWvO5JYeGfYl2jh6Fr7KOH3A/tjJA8ynod6s3qubC5G9gWcnW81FjB6fS/g9J/eYY4++zz BneZWQbiC7vB8d179FL8XnFxxl1BPQb1cBIrk1EWYB2JLmfaNDgTm4ffp3qqKT3Q5rHuph 2BxrNCBse8qe6vJiz9NAqH6hiEb2aNgP/+YR+RZkRIKO+k1sWpUx7cxgN90QvUoB0CV5X/ r5b8ZN4cPZM3td/idm3wZqoM7PLGLPVukHq+et0Ig2ri3X8Tws0LTDkYn5D0uw== List-Id: Technical discussions relating to FreeBSD List-Archive: https://lists.freebsd.org/archives/freebsd-hackers List-Help: List-Post: List-Subscribe: List-Unsubscribe: Sender: owner-freebsd-hackers@freebsd.org MIME-Version: 1.0 Date: Sat, 02 Sep 2023 10:23:43 +0200 From: Alexander Leidinger To: "Mathew, Cherry G.*" Cc: freebsd-hackers@freebsd.org Subject: Re: ARC model specified in spinroot/promela In-Reply-To: <85jzt96qjz.fsf@bow.st> References: <85jzt96qjz.fsf@bow.st> Message-ID: <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> X-Sender: Alexander@Leidinger.net Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit X-Spamd-Bar: ---- X-Rspamd-Pre-Result: action=no action; module=replies; Message is reply to one we originated X-Spamd-Result: default: False [-4.00 / 15.00]; REPLY(-4.00)[]; ASN(0.00)[asn:34240, ipnet:2a00:1828::/32, country:DE] X-Rspamd-Queue-Id: 4Rd7Gh1KrCz3VrC 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