From nobody Sat Sep 02 17:15:29 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 4RdM406m2nz4sLBH for ; Sat, 2 Sep 2023 17:15:44 +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 4RdM403mRTz4cFc; Sat, 2 Sep 2023 17:15:44 +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 C0B444781; Sat, 2 Sep 2023 19:15:29 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=leidinger.net; s=outgoing-alex; t=1693674932; 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=5004KhCJFKI7unae0yugPQutFVcpvDGQKKd6Y3clMPY=; b=r7+SDvoLRQGn2Wzjwq0Lkiw+IHWP+0A8Ltp+I0VL4tBJXAJ9SmtZSz2vOiYy5oOVp8e/ku muM4LxMQIQ1XptKeW7UgkcLgvJnrYf+st2L0tXDcjB5peIVLQebBzTuLbHtm7mGrDUtbLJ QRlM8/Y+GbA7CYyOI/GWab3/em28v2LaPBZNHHvHPP490pVl1zAmaHF/QXDP06yATV4BLy S7ktjNkfJ3pLKTbRNahjd0Om6zGplABsRuDJuLdUO/0VJb6wt2NwJTFUuaOukMWBknhqAz PuCkUocazmsnXQUyh2yuugcyxQ0am4dZuOHoXwZj6+FFGmEdQwCHo5ZEBCDDFg== 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 19:15:29 +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: <858r9o6ee0.fsf@bow.st> References: <85jzt96qjz.fsf@bow.st> <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> <858r9o6ee0.fsf@bow.st> Message-ID: <0b73ec6dd871c8e0c646f31614570058@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: 4RdM403mRTz4cFc Am 2023-09-02 12:47, schrieb Mathew, Cherry G.*: > 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. And just when I've send the mail, it finished... :) ---snip--- Samstag, 02. September 2023, 18:51:21 (203) root@ttypts/1 # time make spin-gen 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))) make spin-gen 0,04s user 0,11s system 24% cpu 0,585 total Samstag, 02. September 2023, 18:51:29 (204) root@ttypts/1 # time make spin-build cc -o pan pan.c make spin-build 0,47s user 0,26s system 56% cpu 1,286 total Samstag, 02. September 2023, 18:51:37 (205) root@ttypts/1 # time make spin-run cc -o pan pan.c ./pan -a #Generate arc.pml.trail on error Depth= 271 States= 1e+06 Transitions= 2.04e+06 Memory= 194.550 t= 4.47 R= 2e+05 Depth= 271 States= 2e+06 Transitions= 4.09e+06 Memory= 264.081 t= 9.16 R= 2e+05 Depth= 271 States= 3e+06 Transitions= 6.16e+06 Memory= 334.101 t= 13.5 R= 2e+05 Depth= 271 States= 4e+06 Transitions= 8.25e+06 Memory= 410.370 t= 18.4 R= 2e+05 Depth= 271 States= 5e+06 Transitions= 1.04e+07 Memory= 485.272 t= 23.4 R= 2e+05 Depth= 271 States= 6e+06 Transitions= 1.25e+07 Memory= 560.175 t= 28 R= 2e+05 Depth= 271 States= 7e+06 Transitions= 1.46e+07 Memory= 635.077 t= 33.1 R= 2e+05 Depth= 271 States= 8e+06 Transitions= 1.67e+07 Memory= 710.077 t= 38 R= 2e+05 Depth= 271 States= 9e+06 Transitions= 1.88e+07 Memory= 787.812 t= 43.2 R= 2e+05 Depth= 271 States= 1e+07 Transitions= 2.09e+07 Memory= 867.987 t= 48.5 R= 2e+05 Depth= 271 States= 1.1e+07 Transitions= 2.3e+07 Memory= 948.163 t= 53.5 R= 2e+05 Depth= 271 States= 1.2e+07 Transitions= 2.51e+07 Memory= 1028.339 t= 58.7 R= 2e+05 Depth= 271 States= 1.3e+07 Transitions= 2.72e+07 Memory= 1108.515 t= 63.8 R= 2e+05 Depth= 271 States= 1.4e+07 Transitions= 2.93e+07 Memory= 1188.202 t= 69.1 R= 2e+05 Depth= 271 States= 1.5e+07 Transitions= 3.15e+07 Memory= 1267.401 t= 74.5 R= 2e+05 Depth= 271 States= 1.6e+07 Transitions= 3.36e+07 Memory= 1346.503 t= 79.9 R= 2e+05 Depth= 271 States= 1.7e+07 Transitions= 3.58e+07 Memory= 1425.605 t= 85.2 R= 2e+05 [...] Depth= 271 States= 2.07e+08 Transitions= 4.44e+08 Memory= 20175.351 t= 1.22e+03 R= 2e+05 Depth= 271 States= 2.08e+08 Transitions= 4.46e+08 Memory= 20262.558 t= 1.22e+03 R= 2e+05 Depth= 271 States= 2.09e+08 Transitions= 4.49e+08 Memory= 20349.667 t= 1.23e+03 R= 2e+05 pan:1: acceptance cycle (at depth 270) pan: wrote spinmodel.pml.trail (Spin Version 6.5.0 -- 1 July 2019) Warning: Search not completed + 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 184 byte, depth reached 271, errors: 1 1.0465042e+08 states, stored (2.09301e+08 visited) 2.4007432e+08 states, matched 4.4937506e+08 transitions (= visited+matched) 44667618 atomic steps hash conflicts: 63844226 (resolved) Stats on memory usage (in Megabytes): 21158.112 equivalent memory usage for states (stored*(State-vector + overhead)) 18344.457 actual memory usage for states (compression: 86.70%) state-vector as stored = 156 byte + 28 byte overhead 2048.000 memory used for hash table (-w28) 0.534 memory used for DFS stack (-m10000) 17.170 memory lost to fragmentation 20375.839 total actual memory usage pan: elapsed time 1.23e+03 seconds pan: rate 169922.52 states/second make spin-run 1199,05s user 34,46s system 99% cpu 20:33,94 total ---snip--- Hope this helps, Alexander. -- http://www.Leidinger.net Alexander@Leidinger.net: PGP 0x8F31830F9F2772BF http://www.FreeBSD.org netchild@FreeBSD.org : PGP 0x8F31830F9F2772BF