promela expl done (minus ltl)

This commit is contained in:
Claudio Maggioni 2023-05-10 16:47:52 +02:00
parent 422c06c7aa
commit 1e25f0d9d1
2 changed files with 112 additions and 1 deletions

Binary file not shown.

View file

@ -159,7 +159,118 @@ init {
Each of the enumerated sections is surrounded by curly braces to emulate the Each of the enumerated sections is surrounded by curly braces to emulate the
effect of locally scoped variables in procedures, which do not exist in effect of locally scoped variables in procedures, which do not exist in
\textit{ProMeLa} aside the cuncurrency-like \texttt{proctype} construct. \textit{ProMeLa} aside the concurrency emulating \texttt{proctype} construct.
The array initialization is carried out as follows:
\begin{minted}{c}
int i;
for (i in to_reverse) {
int value;
select(value: 0 .. R);
to_reverse[i] = value;
printf("to_reverse[%d]: %d\n", i, value);
}
\end{minted}
As specified above, the array is initialized with values in $[0,R]$.
Specifically, values are generated using a nondeterministic \texttt{select}
statement to allow the model checker to try all possible values efficiently.
The sequential reversed algorithm is implemented with the following code:
\begin{minted}{c}
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;
\end{minted}
which is a direct translation of the Java implementation to verify.
The sequential reverser is used to implement each thread of the parallel
reverser through the \textit{ThreadedReverser} class. In the model, the class is
translated in a Spin process through the \texttt{proctype} construct with the
following implementation:
\begin{minted}{c}
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("reversed_par[%d] = to_reverse[%d]\n", LENGTH - k - 1, k);
reversed_par[LENGTH - k - 1] = to_reverse[k];
}
printf("proc[%d]: ended\n", n);
done[n] = true;
}
\end{minted}
The implementation is closely related to the sequential one, as it differs only
in \texttt{reversed\_par} being used as the destination array and limiting the
reversal between \texttt{from} and \texttt{to}. The argument \texttt{n} is used
to identify the thread in the \texttt{done} array to store the termination
state. Following the indexing rules of \texttt{done} given earlier, the i-th
spawned thread corresponds to a \texttt{proctype} call with $n = i$, so that at
termination \mintinline{c}{done[i]} is set to \mintinline{c}{true}.
The actual thread-spawning part of the parallel reverser, i.e.\ class
\textit{ParallelReverser} itself, is represented by the following
\textit{ProMeLa} code placed in the \texttt{init} section of the model:
\begin{minted}{c}
int n;
int s = LENGTH / N;
for (n: 0 .. (N - 1)) { // fork loop
int from = n * s;
int to;
if
:: (n == N - 1) -> to = LENGTH;
:: else -> to = n * s + s;
fi
run ThreadedReverser(from, to, n + 1); // fork here
}
for (n: 1 .. N) { // join loop
(done[n] == true); // join n-th thread here
printf("[%d] joined\n", n);
}
\end{minted}
Here the values of \texttt{n}, \texttt{s}, \texttt{from} and \texttt{to}
replicate exactly the values used in the Java implementation. The \texttt{n + 1}
parameter identifies maps each \texttt{proctype} invocation to its place in the
invocation order (e.g.\ for $n=0$, \texttt{ThreadedReverser} is called with
$n+1=1$, since this is the 1st invocation of the process).
The second ``join'' loop waits for each process to complete in order of
invocation, replication the thread joining behaviour of the parallel reverser
implementation in the Java program. Note that the \textit{ProMeLa} statement
\mintinline{c}{(done[n] == true);} will ``wait'' for the value of
\mintinline{c}{done[n]} to be \mintinline{c}{true} before executing the
following statement, thus being an adequate analogy for
\mintinline{java}{Thread.join()}.
Finally, the congruence check between the arrays produced by both implementation
is implemented with the following code:
\begin{minted}{c}
int i;
for (i: 0 .. (LENGTH - 1)) {
if
:: (reversed_seq[i] != reversed_par[i]) -> seq_eq_to_parallel = false;
fi
}
\end{minted}
Should any matching pair of elements be different,
\texttt{seq\_eq\_to\_parallel} will be set to \mintinline{c}{false}. Note that
this boolean variable is used to implement one of the LTL properties, hence why
it is declared and set to a meaningful value in this block of the model.
\subsection{LTL properties}
The citation \cite{tange_2023_7855617}. The citation \cite{tange_2023_7855617}.
The citation \cite{spin}. The citation \cite{spin}.