From 2317899fca8fe90f369b35003e5cf91e6e145675 Mon Sep 17 00:00:00 2001 From: Claudio Maggioni Date: Wed, 10 May 2023 18:08:00 +0200 Subject: [PATCH] correction on promela model to follow indications in the assignment --- ReversalModel/reversal.pml.m4 | 92 +++++++------- .../reversal_seq_eq_parallel_2_3_2.pml | 118 ++++++++++++++++++ ReversalModel/run.sh | 29 +++++ report.tex | 13 ++ 4 files changed, 208 insertions(+), 44 deletions(-) create mode 100644 ReversalModel/reversal_seq_eq_parallel_2_3_2.pml create mode 100755 ReversalModel/run.sh diff --git a/ReversalModel/reversal.pml.m4 b/ReversalModel/reversal.pml.m4 index bdb7064..e9d2c3c 100644 --- a/ReversalModel/reversal.pml.m4 +++ b/ReversalModel/reversal.pml.m4 @@ -5,9 +5,9 @@ define(`for',`ifelse($#,0,``$0'',`ifelse(eval($2<=$3),1, `pushdef(`$1',$2)$4`'popdef(`$1')$0(`$1',incr($2),$3,`$4')')')') */ -int to_reverse[LENGTH]; // array to reverse -int reversed_seq[LENGTH]; // for SequentialReverser: where the reverse is stored -int reversed_par[LENGTH]; // for ParallelReverser: where the reverse is stored +int a[LENGTH]; // array to reverse +int r_s[LENGTH]; // for SequentialReverser: where the reverse is stored +int r_p[LENGTH]; // for ParallelReverser: where the reverse is stored // stores termination of each reverser // index 0 is for the sequential algorithm @@ -22,70 +22,74 @@ proctype ThreadedReverser(int from; int to; int n) { int k; for (k: from .. (to - 1)) { - printf("reversed_par[%d] = to_reverse[%d]\n", LENGTH - k - 1, k); - reversed_par[LENGTH - k - 1] = to_reverse[k]; + printf("r_p[%d] = a[%d]\n", LENGTH - k - 1, k); + r_p[LENGTH - k - 1] = a[k]; } printf("proc[%d]: ended\n", n); done[n] = true; } +// SequentialReverser implementation +proctype SequentialReverser() { + int k; + for (k: 0 .. (LENGTH - 1)) { + r_s[LENGTH - k - 1] = a[k]; + printf("r_s[%d] = a[%d]\n", LENGTH - k - 1, k); + } + done[0] = true; // mark sequential end +} + +// ParallelReverser implementation +proctype ParallelReverser() { + int n; + int s = LENGTH / N; + + // fork section + for (n: 0 .. (N - 1)) { + int from = n * s; + int to; + if + :: (n == N - 1) -> to = LENGTH; + :: else -> to = n * s + s; + fi + run ThreadedReverser(from, to, n + 1); // run as "thread n" + } + + // join section + for (n: 1 .. N) { + (done[n] == true); // wait "thread n" + printf("[%d] joined\n", n); + } +} + init { printf("program start\n"); // array initialization { int i; - for (i in to_reverse) { + for (i in a) { int value; select(value: 0 .. R); - to_reverse[i] = value; - printf("to_reverse[%d]: %d\n", i, value); + a[i] = value; + printf("a[%d]: %d\n", i, value); } } printf("sequential start\n"); - // SequentialReverser implementation - { - int k; - for (k: 0 .. (LENGTH - 1)) { - reversed_seq[LENGTH - k - 1] = to_reverse[k]; - printf("reversed_seq[%d] = to_reverse[%d]\n", LENGTH - k - 1, k); - } - done[0] = true; // mark sequential end - } - printf("sequential end\n"); + run SequentialReverser(); printf("parallel start\n"); - // ParallelReverser implementation - { - int n; - int s = LENGTH / N; - - // fork section - for (n: 0 .. (N - 1)) { - int from = n * s; - int to; - if - :: (n == N - 1) -> to = LENGTH; - :: else -> to = n * s + s; - fi - run ThreadedReverser(from, to, n + 1); // run as "thread n" - } + run ParallelReverser(); - // join section - for (n: 1 .. N) { - (done[n] == true); // wait "thread n" - printf("[%d] joined\n", n); - } - } - printf("parallel end\n"); + (done[0] == true && done[N] == true); // test if seq and parallel are the same { int i; for (i: 0 .. (LENGTH - 1)) { if - :: (reversed_seq[i] != reversed_par[i]) -> seq_eq_to_parallel = false; + :: (r_s[i] != r_p[i]) -> seq_eq_to_parallel = false; fi } } @@ -112,7 +116,7 @@ ltl termination { // ifelse(LTL, correctness_seq, ` ltl correctness_seq { [] (done[0] == true -> (true for(`k', 0, LENGTH-1, ` && - reversed_seq[eval(LENGTH - k - 1)] == to_reverse[k]'))) + r_s[eval(LENGTH - k - 1)] == a[k]'))) } // ', `') @@ -120,6 +124,6 @@ ltl correctness_seq { // ifelse(LTL, correctness_par, ` ltl correctness_par { [] (done[2] == true -> (true for(`k', 0, LENGTH / N - 1, ` && - reversed_par[eval(LENGTH - k - 1)] == to_reverse[k]'))) + r_p[eval(LENGTH - k - 1)] == a[k]'))) } -// ', `') \ No newline at end of file +// ', `') diff --git a/ReversalModel/reversal_seq_eq_parallel_2_3_2.pml b/ReversalModel/reversal_seq_eq_parallel_2_3_2.pml new file mode 100644 index 0000000..ac4d138 --- /dev/null +++ b/ReversalModel/reversal_seq_eq_parallel_2_3_2.pml @@ -0,0 +1,118 @@ +/* +m4 for loop definition + + +*/ + +int a[3]; // array to reverse +int r_s[3]; // for SequentialReverser: where the reverse is stored +int r_p[3]; // for ParallelReverser: where the reverse is stored + +// stores termination of each reverser +// index 0 is for the sequential algorithm +// indices 1-2 are for the ThreadedReverser instances +bool done[2 + 1]; // initialized to false + +bool seq_eq_to_parallel = true; + +// ThreadedReverser implementation +proctype ThreadedReverser(int from; int to; int n) { + printf("proc[%d]: started from=%d to=%d\n", n, from, to); + + int k; + for (k: from .. (to - 1)) { + printf("r_p[%d] = a[%d]\n", 3 - k - 1, k); + r_p[3 - k - 1] = a[k]; + } + + printf("proc[%d]: ended\n", n); + done[n] = true; +} + +// SequentialReverser implementation +proctype SequentialReverser() { + int k; + for (k: 0 .. (3 - 1)) { + r_s[3 - k - 1] = a[k]; + printf("r_s[%d] = a[%d]\n", 3 - k - 1, k); + } + done[0] = true; // mark sequential end +} + +// ParallelReverser implementation +proctype ParallelReverser() { + int n; + int s = 3 / 2; + + // fork section + for (n: 0 .. (2 - 1)) { + int from = n * s; + int to; + if + :: (n == 2 - 1) -> to = 3; + :: else -> to = n * s + s; + fi + run ThreadedReverser(from, to, n + 1); // run as "thread n" + } + + // join section + for (n: 1 .. 2) { + (done[n] == true); // wait "thread n" + printf("[%d] joined\n", n); + } +} + +init { + printf("program start\n"); + // array initialization + { + int i; + for (i in a) { + int value; + select(value: 0 .. 2); + a[i] = value; + printf("a[%d]: %d\n", i, value); + } + } + + printf("sequential start\n"); + run SequentialReverser(); + + printf("parallel start\n"); + run ParallelReverser(); + + (done[0] == true && done[2] == true); + + // test if seq and parallel are the same + { + int i; + for (i: 0 .. (3 - 1)) { + if + :: (r_s[i] != r_p[i]) -> seq_eq_to_parallel = false; + fi + } + } +} + +// ltl syntax: https://spinroot.com/spin/Man/ltl.html + +ltl seq_eq_parallel { + // the variable seq_eq_to_parallel will never be false if all the elements + // between the sequential and parallel reversed arrays are equal + [] (seq_eq_to_parallel == true) +} + +ltl termination { + // termination happens when the sequential reverser terminates + // (done[0] is true) and the last process in the parallel reverser joins + // (done[2] is true) + <> (done[0] == true && done[2] == true) +} + +// Due to avoid excessive parser complexity when checking the model +// with other ltl properties the correctness_seq is excluded by m4 from the +// ProMeLa source when there is no need to check it +// + +// Similar exclusion logic is applied to correctness_par +// diff --git a/ReversalModel/run.sh b/ReversalModel/run.sh new file mode 100755 index 0000000..a88a837 --- /dev/null +++ b/ReversalModel/run.sh @@ -0,0 +1,29 @@ +#!/bin/bash + +set -e + +SCRIPT_DIR=$(cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd) + +cc="gcc-13" + +if [ "$#" -ne 54]; then + echo "$0: [ltl-prop] [n] [length] [r]" > /dev/stderr + exit 1 +fi + +id="${1}_${2}_${3}_${4}" +filename="reversal_$id.pml" +pan_name="pan_$id" + +compile_dir="$(mktemp -d)" +cp "$SCRIPT_DIR/reversal.pml.m4" "$compile_dir" +cd "$compile_dir" + +m4 -DN="$2" -DLENGTH="$3" -DR="$4" -DLTL="$1" reversal.pml.m4 > "$filename" +spin -a "$filename" +"$cc" -Wno-format-overflow -o "$pan_name" pan.c + +"./$pan_name" -a -N "$1" + +cd "$SCRIPT_DIR" +rm -rf "$compile_dir" diff --git a/report.tex b/report.tex index 30c6161..bac5877 100644 --- a/report.tex +++ b/report.tex @@ -271,6 +271,19 @@ it is declared and set to a meaningful value in this block of the model. \subsection{LTL properties} +In this section I cover the LTL property definitions I included in the model. + +The following LTL property definition checks that once both reversers have +terminated, the content of + +\begin{minted}{c} +ltl seq_eq_parallel { + [] (seq_eq_to_parallel == true) +} +\end{minted} + + + The citation \cite{tange_2023_7855617}. The citation \cite{spin}.