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