From nobody Mon Sep 4 19:47:27 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 4RffMN4D5Gz4sTfr for ; Mon, 4 Sep 2023 19:48:32 +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 4RffMN18fzz4R0w; Mon, 4 Sep 2023 19:48:32 +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 C80F04571; Mon, 4 Sep 2023 21:47:43 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=leidinger.net; s=outgoing-alex; t=1693856897; 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: in-reply-to:in-reply-to:references:references; bh=Bd9R3bVsArga+cpgqU3XhUNvBCdYC9UT36lugVRLjAQ=; b=WL/DX61S2TexX3eq9Jt/nHdPdMOiI0hEnXMkjmj5VCEE3DT5/joePEGDzklc1OKNRIOPl1 12lJ4jT7eVJJc8YgapDJQS5awkcbyXxCOrB5shxCfc/8x2tdCXvRe/cb+l9cVvJXC1b1jH EEM86M7Mu+W0ZnLLu8RUx4owkoAHeHilWkXuHuQjfc0wAQWNjnMYJM7L/tyFXr8jJ144/g 7bJ1vgIq93B6PNxgVwrutV8hG1QRq4Sy4W/xpFL2B5yxcp3uC6hjc95m9/t4YENZkzpY5B C2h9bkDq2K6WedMo/PqsnlQFk4N3+EUZPPlZy1O+V8/47zBalLQ3BYE20kkwKg== 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: Mon, 04 Sep 2023 21:47:27 +0200 From: Alexander Leidinger To: "Mathew, Cherry G.*" Cc: adridg@freebsd.org, freebsd-hackers@freebsd.org Subject: Re: ARC model specified in spinroot/promela In-Reply-To: <85a5u22oxx.fsf@bow.st> References: <85jzt96qjz.fsf@bow.st> <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> <858r9o6ee0.fsf@bow.st> <85pm304dzi.fsf@bow.st> <85a5u22oxx.fsf@bow.st> Message-ID: <1e3a17e39094a9630eebce9f91f00e30@Leidinger.net> X-Sender: Alexander@Leidinger.net Content-Type: multipart/signed; protocol="application/pgp-signature"; boundary="=_485de4d893b5ac7101fde483e9b6fbed"; micalg=pgp-sha256 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: 4RffMN18fzz4R0w This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --=_485de4d893b5ac7101fde483e9b6fbed Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; format=flowed Am 2023-09-04 12:49, schrieb Mathew, Cherry G.*: >>>>>> Mathew, Cherry G * writes: > > [...] > > > So there's room for improvement in my Makefile to: > > > 1) Explore multithreaded/CPU > > 2) Understand state space explosion scale - it is exponential to > > the number of processes, I've fixed it to run in a loop - will > > report back once I have good progress also with the model > > extraction part. > > 3) My model has errors - I'm glad to see that the error reporting > > is the same in my new optimised loop, as in the RAM hungry > version > > you ran. > > > Thanks once again - this is very helpful. I will report back once > > I have more progress. > > Hi Again, > > So just wanted to report back with a patch (absolute patch, not > relative, > so please nuke your existing arc/ if you tried the old one and apply in > a clean new subdirectory) on the following: # make spin-run cp arc.pml model #mimic modex cat model > spinmodel.pml;cat arc.drv >> spinmodel.pml;cat arc.inv >> spinmodel.pml; spin -am spinmodel.pml ltl ltl_0: (((((((((<> ([] ((_nr_pr==1)))) && ([] (((((len(T1.item_list)+len(B1.item_list))+len(T2.item_list))+len(B2.item_list))<=(2*64))))) && ([] (((len(T1.item_list)+len(B1.item_list))<=64)))) && ([] (((len(T2.item_list)+len(B2.item_list))<(2*64))))) && ([] (((len(T1.item_list)+len(T2.item_list))<=64)))) && ([] ((! (((((len(T1.item_list)+len(B1.item_list))+len(T2.item_list))+len(B2.item_list))<64))) || (((len(B1.item_list)==0)) && ((len(B2.item_list)==0)))))) && ([] ((! (((((len(T1.item_list)+len(B1.item_list))+len(T2.item_list))+len(B2.item_list))>=64))) || (((len(T1.item_list)+len(T2.item_list))==64))))) && ([] ((p<=64)))) && (<> (((len(T1.item_list)==p)) && ((len(T2.item_list)==(64-p)))))) && (<> ((p>0))) cc -DVECTORSZ=65536 -o pan pan.c ./pan -a #Generate arc.pml.trail on error error: max search depth too small (Spin Version 6.5.0 -- 1 July 2019) + Partial Order Reduction Full statespace search for: never claim + (ltl_0) assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 2124 byte, depth reached 9999, errors: 0 1 states, stored 11 states, matched 12 transitions (= stored+matched) 109989 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.002 equivalent memory usage for states (stored*(State-vector + overhead)) 12.456 actual memory usage for states 128.000 memory used for hash table (-w24) 0.534 memory used for DFS stack (-m10000) 5.686 memory lost to fragmentation 140.500 total actual memory usage unreached in init spinmodel.pml:80, state 28, "D_STEP80" spinmodel.pml:80, state 53, "D_STEP80" spinmodel.pml:154, state 70, "B1.item_list?_" spinmodel.pml:80, state 79, "D_STEP80" spinmodel.pml:90, state 85, "D_STEP90" spinmodel.pml:78, state 86, "(((len(T1.item_list)!=0)&&((len(T1.item_list)>p)||(B2.item_list??[eval(x[x_iid].iid)]&&(len(T1.item_list)==p)))))" spinmodel.pml:78, state 86, "else" spinmodel.pml:73, state 88, "D_STEP73" spinmodel.pml:159, state 90, "assert((len(B1.item_list)==0))" spinmodel.pml:160, state 94, "D_STEP160" spinmodel.pml:152, state 95, "((len(T1.item_list)<64))" spinmodel.pml:152, state 95, "else" spinmodel.pml:183, state 100, "B2.item_list?_" spinmodel.pml:198, state 128, "(1)" spinmodel.pml:268, state 155, "-end-" (13 of 155 states) unreached in claim ltl_0 _spin_nvr.tmp:70, state 108, "-end-" (1 of 108 states) pan: elapsed time 0.164 seconds pan: rate 6.0952381 states/second No trail file generated... Bye, Alexander. -- http://www.Leidinger.net Alexander@Leidinger.net: PGP 0x8F31830F9F2772BF http://www.FreeBSD.org netchild@FreeBSD.org : PGP 0x8F31830F9F2772BF --=_485de4d893b5ac7101fde483e9b6fbed Content-Type: application/pgp-signature; name=signature.asc Content-Disposition: attachment; filename=signature.asc; size=833 Content-Description: OpenPGP digital signature -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEER9UlYXp1PSd08nWXEg2wmwP42IYFAmT2NF8ACgkQEg2wmwP4 2IYhuQ/+KvWE/uUmjPAsNoDIyaMZTFWq51fxWUZUVERNUIbUtCKLA2u3YqfT/BUM g353QgBLaJ/o9D+b8yufymXa1AQCsUUQLVtxdSAaUdi+mbJg45t/ZLuJftmp8qFu SaktD+UVpPymQO6PRABPAyHL5wYF1+Hhl4qquccLeooyYOC65Bhk6Ei2IM+tNpkM pnzn05CM+Yxy6+syHuwCXv0o/M+M7dF8FziiKaj7YnVvvBK34XcRjnMiLF5k+TxJ MS0fei0jobqD4NIwyUKcx2oaTwoiIrZ8pcU67F+IhErjm7JBNi0/1IL03QeUIEA5 ko+OBFe7IVEG3S3OSDyjFZPs9no2g07oRb3T8ihI1ecOcYIGlTSPoFT1//pkzA1g 4P/dy7Dsz042inhVTJOQSH3YuhszIa/2NcpSsWKv2m1sgSgVMwbMLnNBb6xcoXxY nQ8SOrOielbofZSBsUvXq8am6pIbnKDQR0yoIPXXTIBF/tVZ9+tUXc6DkZXSg3Yh Zd4CDbOA1Xb6jFJwZVLkGrtN+zPM6EALhs+HWgAz7JWNxWHPfb4DImxvkEfeAl+m lXW9ffzyBUrXv2iC5ipUAvWzwmUj+cS02q4uj9uC5Wy+v3XyOoJUCtZPVf7zLZV6 XBmr9ZfexXPtbXhDkt/KoyT4Qdyx5Q9eMgaqejbv6Ov2ux+QYdM= =+w6P -----END PGP SIGNATURE----- --=_485de4d893b5ac7101fde483e9b6fbed--