From nobody Sat Sep 02 10:47:03 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 4RdBSG3mG1z4rcj4 for ; Sat, 2 Sep 2023 10:47:42 +0000 (UTC) (envelope-from c@bow.st) Received: from comms.drone (in.bow.st [71.19.146.166]) (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 did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 4RdBSD0B9Kz4R5B; Sat, 2 Sep 2023 10:47:39 +0000 (UTC) (envelope-from c@bow.st) Authentication-Results: mx1.freebsd.org; dkim=none; spf=pass (mx1.freebsd.org: domain of c@bow.st designates 71.19.146.166 as permitted sender) smtp.mailfrom=c@bow.st; dmarc=none Received: from homebase (unknown [IPv6:fe80::ff1d:976a:a7e4:ee6a]) by comms.drone (Postfix) with ESMTPSA id 81175FCFE; Sat, 2 Sep 2023 10:47:34 +0000 (UTC) From: "Mathew\, Cherry G.*" To: Alexander Leidinger , adridg@freebsd.org Cc: freebsd-hackers@freebsd.org Subject: Re: ARC model specified in spinroot/promela References: <85jzt96qjz.fsf@bow.st> <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> Date: Sat, 02 Sep 2023 10:47:03 +0000 In-Reply-To: <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> (Alexander Leidinger's message of "Sat, 02 Sep 2023 10:23:43 +0200") Message-ID: <858r9o6ee0.fsf@bow.st> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (berkeley-unix) 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 Content-Type: text/plain X-Spamd-Bar: - X-Spamd-Result: default: False [-1.87 / 15.00]; HFILTER_HELO_IP_A(1.00)[comms.drone]; NEURAL_HAM_MEDIUM(-1.00)[-0.998]; NEURAL_HAM_LONG(-0.99)[-0.989]; NEURAL_HAM_SHORT(-0.99)[-0.988]; HFILTER_HELO_NORES_A_OR_MX(0.30)[comms.drone]; R_SPF_ALLOW(-0.20)[+mx]; MIME_GOOD(-0.10)[text/plain]; ONCE_RECEIVED(0.10)[]; TO_DN_SOME(0.00)[]; R_DKIM_NA(0.00)[]; FROM_EQ_ENVFROM(0.00)[]; MIME_TRACE(0.00)[0:+]; RCVD_TLS_ALL(0.00)[]; ASN(0.00)[asn:47066, ipnet:71.19.146.0/24, country:US]; FROM_HAS_DN(0.00)[]; MLMMJ_DEST(0.00)[freebsd-hackers@freebsd.org]; ARC_NA(0.00)[]; RCPT_COUNT_THREE(0.00)[3]; RCVD_COUNT_ONE(0.00)[1]; DMARC_NA(0.00)[bow.st]; TO_MATCH_ENVRCPT_SOME(0.00)[]; MID_RHS_MATCH_FROM(0.00)[]; RCVD_VIA_SMTP_AUTH(0.00)[] X-Rspamd-Queue-Id: 4RdBSD0B9Kz4R5B Hi Alexander, >>>>> "AL" == Alexander Leidinger 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 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