Date: Sat, 02 Sep 2023 19:15:29 +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: <0b73ec6dd871c8e0c646f31614570058@Leidinger.net> In-Reply-To: <858r9o6ee0.fsf@bow.st> References: <85jzt96qjz.fsf@bow.st> <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> <858r9o6ee0.fsf@bow.st>
next in thread | previous in thread | raw e-mail | index | archive | help
Am 2023-09-02 12:47, schrieb Mathew, Cherry G.*:
> Hi Alexander,
>
>>>>>> "AL" == Alexander Leidinger <Alexander@Leidinger.net> 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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?0b73ec6dd871c8e0c646f31614570058>