modelcheck: update output and documentation
Fixes #330. * tests/ltsmin/README, tests/ltsmin/modelcheck.cc: here.
This commit is contained in:
Etienne Renault
parent
2bd08d956a
commit
a9178fbe64
2 changed files with 91 additions and 27 deletions
|
|
@ -144,31 +144,34 @@ Examples
|
||||||
that the critical section is accessed infinitely often by some
|
that the critical section is accessed infinitely often by some
|
||||||
processes using:
|
processes using:
|
||||||
|
|
||||||
% ./modelcheck beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
|
% ./modelcheck --model beem-peterson.4.dve --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --is-empty
|
||||||
2239039 unique states visited
|
2239039 unique states visited
|
||||||
0 strongly connected components in search stack
|
0 strongly connected components in search stack
|
||||||
11449204 transitions explored
|
11449204 transitions explored
|
||||||
1024245 items max in DFS search stack
|
1024245 items max in DFS search stack
|
||||||
|
111081 pages allocated for emptiness check
|
||||||
no accepting run found
|
no accepting run found
|
||||||
|
|
||||||
Process P_0 can starve, waiting to enter in critical section:
|
Process P_0 can starve, waiting to enter in critical section:
|
||||||
|
|
||||||
% ./modelcheck beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)'
|
% ./modelcheck --model beem-peterson.4.dve --formula '!G(P_0.wait -> F P_0.CS)' --is-empty
|
||||||
2190 unique states visited
|
3978 unique states visited
|
||||||
34 strongly connected components in search stack
|
31 strongly connected components in search stack
|
||||||
4896 transitions explored
|
4723 transitions explored
|
||||||
83 items max in DFS search stack
|
3302 items max in DFS search stack
|
||||||
an accepting run exists (use -C to print it)
|
1099 pages allocated for emptiness check
|
||||||
|
an accepting run exists (use -c to print it)
|
||||||
|
|
||||||
Variable pos[1] is not always < 3 (this formula makes no sense, it
|
Variable pos[1] is not always < 3 (this formula makes no sense, it
|
||||||
is just to demonstrate the use of double quote).
|
is just to demonstrate the use of double quote).
|
||||||
|
|
||||||
% ./modelcheck beem-peterson.4.dve '!G("pos[1] < 3")'
|
% ./modelcheck --model beem-peterson.4.dve --formula '!G("pos[1] < 3")' --is-empty
|
||||||
130 unique states visited
|
130 unique states visited
|
||||||
61 strongly connected components in search stack
|
61 strongly connected components in search stack
|
||||||
132 transitions explored
|
132 transitions explored
|
||||||
130 items max in DFS search stack
|
130 items max in DFS search stack
|
||||||
an accepting run exists (use -C to print it)
|
512 pages allocated for emptiness check
|
||||||
|
an accepting run exists (use -c to print it)
|
||||||
|
|
||||||
|
|
||||||
Two state-compression techniques have been implemented as experiments.
|
Two state-compression techniques have been implemented as experiments.
|
||||||
|
|
@ -177,41 +180,102 @@ than 2^28, it is way faster than -z (which will work for all values).
|
||||||
|
|
||||||
Activating state compression will often reduce runtime. Compare:
|
Activating state compression will often reduce runtime. Compare:
|
||||||
|
|
||||||
% ./modelcheck -T beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
|
$ ./modelcheck --model beem-peterson.4.dve --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --is-empty --timer
|
||||||
|
|
||||||
2239039 unique states visited
|
2239039 unique states visited
|
||||||
0 strongly connected components in search stack
|
0 strongly connected components in search stack
|
||||||
11449204 transitions explored
|
11449204 transitions explored
|
||||||
1024245 items max in DFS search stack
|
1024245 items max in DFS search stack
|
||||||
122102 pages allocated for emptiness check
|
111081 pages allocated for emptiness check
|
||||||
no accepting run found
|
no accepting run found | user time | sys. time | total |
|
||||||
| user time | sys. time | total |
|
|
||||||
name | ticks % | ticks % | ticks % | n
|
name | ticks % | ticks % | ticks % | n
|
||||||
-------------------------------------------------------------------------------
|
-------------------------------------------------------------------------------
|
||||||
loading dve2 | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
loading ltsmin model | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
||||||
parsing formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
parsing formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
||||||
reducing A_f w/ SCC | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
running emptiness chec | 672 100.0 | 13 100.0 | 685 100.0 | 1
|
||||||
running emptiness chec | 1222 100.0 | 18 100.0 | 1240 100.0 | 1
|
|
||||||
translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
||||||
-------------------------------------------------------------------------------
|
-------------------------------------------------------------------------------
|
||||||
TOTAL | 1222 100.0 | 18 100.0 | 1240 100.0 |
|
TOTAL | 672 100.0 | 13 100.0 | 685 100.0 |
|
||||||
|
|
||||||
|
|
||||||
|
$ ./modelcheck --model beem-peterson.4.dve --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --is-empty --timer -z 2
|
||||||
|
|
||||||
% ./modelcheck -T -Z beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
|
|
||||||
2239039 unique states visited
|
2239039 unique states visited
|
||||||
0 strongly connected components in search stack
|
0 strongly connected components in search stack
|
||||||
11449204 transitions explored
|
11449204 transitions explored
|
||||||
1024245 items max in DFS search stack
|
1024245 items max in DFS search stack
|
||||||
78580 pages allocated for emptiness check
|
85991 pages allocated for emptiness check
|
||||||
no accepting run found
|
no accepting run found
|
||||||
| user time | sys. time | total |
|
| user time | sys. time | total |
|
||||||
name | ticks % | ticks % | ticks % | n
|
name | ticks % | ticks % | ticks % | n
|
||||||
-------------------------------------------------------------------------------
|
-------------------------------------------------------------------------------
|
||||||
loading dve2 | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
loading ltsmin model | 40 6.1 | 2 16.7 | 42 6.2 | 1
|
||||||
parsing formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
parsing formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
||||||
reducing A_f w/ SCC | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
running emptiness chec | 620 93.8 | 10 83.3 | 630 93.6 | 1
|
||||||
running emptiness chec | 1051 100.0 | 10 100.0 | 1061 100.0 | 1
|
translating formula | 1 0.2 | 0 0.0 | 1 0.1 | 1
|
||||||
translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
|
||||||
-------------------------------------------------------------------------------
|
-------------------------------------------------------------------------------
|
||||||
TOTAL | 1051 100.0 | 10 100.0 | 1061 100.0 |
|
TOTAL | 661 100.0 | 12 100.0 | 673 100.0 |
|
||||||
|
|
||||||
It's a 15% speedup in this case, be the improvement can be more
|
|
||||||
|
It's a 14% speedup in this case, be the improvement can be more
|
||||||
important on larger models.
|
important on larger models.
|
||||||
|
|
||||||
|
The parallel deadlock detection has also been implemented is this tool:
|
||||||
|
|
||||||
|
% ./modelcheck --model beem-peterson.4.dve --has-deadlock --csv -p 1
|
||||||
|
|
||||||
|
Thread #0: on CPU 0
|
||||||
|
|
||||||
|
---- Thread number : 0
|
||||||
|
1119560 unique states visited
|
||||||
|
3864896 transitions explored
|
||||||
|
78157 items max in DFS search stack
|
||||||
|
1316 milliseconds
|
||||||
|
Find following the csv: thread_id,walltimems,type,states,transitions
|
||||||
|
@th_0,1316,NO-DEADLOCK,1119560,3864896
|
||||||
|
|
||||||
|
Summary :
|
||||||
|
No no deadlock found!
|
||||||
|
Find following the csv: model,walltimems,memused,type,states,transitions
|
||||||
|
#beem-peterson.4.dve,1317,103681,NO-DEADLOCK,1119560,3864896
|
||||||
|
|
||||||
|
|
||||||
|
Running the same algorithm with 3 threads save 40% of the computation time:
|
||||||
|
|
||||||
|
$ ./modelcheck --model beem-peterson.4.dve --has-deadlock --csv -p 3
|
||||||
|
|
||||||
|
Thread #1: on CPU 1
|
||||||
|
Thread #2: on CPU 2
|
||||||
|
Thread #0: on CPU 0
|
||||||
|
|
||||||
|
---- Thread number : 0
|
||||||
|
417923 unique states visited
|
||||||
|
1418775 transitions explored
|
||||||
|
56403 items max in DFS search stack
|
||||||
|
819 milliseconds
|
||||||
|
Find following the csv: thread_id,walltimems,type,states,transitions
|
||||||
|
@th_0,819,NO-DEADLOCK,417923,1418775
|
||||||
|
|
||||||
|
---- Thread number : 1
|
||||||
|
526175 unique states visited
|
||||||
|
1813440 transitions explored
|
||||||
|
69322 items max in DFS search stack
|
||||||
|
819 milliseconds
|
||||||
|
Find following the csv: thread_id,walltimems,type,states,transitions
|
||||||
|
@th_1,819,NO-DEADLOCK,526175,1813440
|
||||||
|
|
||||||
|
---- Thread number : 2
|
||||||
|
404501 unique states visited
|
||||||
|
1411645 transitions explored
|
||||||
|
61888 items max in DFS search stack
|
||||||
|
819 milliseconds
|
||||||
|
Find following the csv: thread_id,walltimems,type,states,transitions
|
||||||
|
@th_2,819,NO-DEADLOCK,404501,1411645
|
||||||
|
|
||||||
|
Summary :
|
||||||
|
No no deadlock found!
|
||||||
|
Find following the csv: model,walltimems,memused,type,states,transitions
|
||||||
|
#beem-peterson.4.dve,820,158211,NO-DEADLOCK,404501,1411645
|
||||||
|
|
||||||
|
One can observe that when possible (i.e., if the OS allows it) we try
|
||||||
|
has much as possible to pin threads to a CPU.
|
||||||
|
|
|
||||||
|
|
@ -340,7 +340,7 @@ static int checked_main()
|
||||||
|
|
||||||
if (!res)
|
if (!res)
|
||||||
{
|
{
|
||||||
std::cout << "no accepting run found";
|
std::cout << "no accepting run found" << std::endl;
|
||||||
}
|
}
|
||||||
else if (!mc_options.compute_counterexample)
|
else if (!mc_options.compute_counterexample)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue