From 1386bb0810d2adf99dc4b5539adbf79236b71224 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Wed, 14 Mar 2018 16:31:16 +0100 Subject: [PATCH] modelcheck: update output and documentation Fixes #330. * tests/ltsmin/README, tests/ltsmin/modelcheck.cc: here. --- tests/ltsmin/README | 116 ++++++++++++++++++++++++++++--------- tests/ltsmin/modelcheck.cc | 2 +- 2 files changed, 91 insertions(+), 27 deletions(-) diff --git a/tests/ltsmin/README b/tests/ltsmin/README index 9947a9e84..6aaf5bba4 100644 --- a/tests/ltsmin/README +++ b/tests/ltsmin/README @@ -144,31 +144,34 @@ Examples that the critical section is accessed infinitely often by some 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 0 strongly connected components in search stack 11449204 transitions explored 1024245 items max in DFS search stack + 111081 pages allocated for emptiness check no accepting run found Process P_0 can starve, waiting to enter in critical section: - % ./modelcheck beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)' - 2190 unique states visited - 34 strongly connected components in search stack - 4896 transitions explored - 83 items max in DFS search stack - an accepting run exists (use -C to print it) + % ./modelcheck --model beem-peterson.4.dve --formula '!G(P_0.wait -> F P_0.CS)' --is-empty + 3978 unique states visited + 31 strongly connected components in search stack + 4723 transitions explored + 3302 items max in DFS search stack + 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 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 61 strongly connected components in search stack 132 transitions explored 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. @@ -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: -% ./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 0 strongly connected components in search stack 11449204 transitions explored 1024245 items max in DFS search stack -122102 pages allocated for emptiness check -no accepting run found - | user time | sys. time | total | +111081 pages allocated for emptiness check +no accepting run found | user time | sys. time | total | 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 - reducing A_f w/ SCC | 0 0.0 | 0 0.0 | 0 0.0 | 1 -running emptiness chec | 1222 100.0 | 18 100.0 | 1240 100.0 | 1 +running emptiness chec | 672 100.0 | 13 100.0 | 685 100.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 0 strongly connected components in search stack 11449204 transitions explored 1024245 items max in DFS search stack -78580 pages allocated for emptiness check +85991 pages allocated for emptiness check no accepting run found - | user time | sys. time | total | + | user time | sys. time | total | 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 - reducing A_f w/ SCC | 0 0.0 | 0 0.0 | 0 0.0 | 1 -running emptiness chec | 1051 100.0 | 10 100.0 | 1061 100.0 | 1 - translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1 +running emptiness chec | 620 93.8 | 10 83.3 | 630 93.6 | 1 + translating formula | 1 0.2 | 0 0.0 | 1 0.1 | 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. + +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. diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index 97ec168a6..12f08f9ff 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -340,7 +340,7 @@ static int checked_main() if (!res) { - std::cout << "no accepting run found"; + std::cout << "no accepting run found" << std::endl; } else if (!mc_options.compute_counterexample) { -- GitLab