more report work

ReversalModel/reversal.pml.m4

@@ -22,12 +22,12 @@ proctype ThreadedReverser(int from; int to; int n) {
 
     int k;
     for (k: from .. (to - 1)) {
-        printf("r_p[%d] = a[%d]\n", LENGTH - k - 1, k);
         r_p[LENGTH - k - 1] = a[k];
+        printf("proc[%d]: r_p[%d] = a[%d]\n", n, LENGTH - k - 1, k);
     }
 
-    printf("proc[%d]: ended\n", n);
     done[n] = true;
+    printf("proc[%d]: ended\n", n);
 }
 
 // SequentialReverser implementation

ReversalModel/run.sh

@@ -21,11 +21,23 @@ cd "$compile_dir"
 
 echo "Compiling in: $compile_dir"
 
+if [ "$PRINTF" == "true" ]; then
+    defs="-DPRINTF "
+else
+    defs=""
+fi
+
 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
-
+"$cc" -Wno-format-overflow $defs -o "$pan_name" pan.c
 "./$pan_name" -a -N "$1" 
 
+# Execute trail if check fails
+if [ -f "$filename.trail" ]; then
+    echo "FAILED" >> /dev/stderr
+    "./$pan_name" -S -N "$1" "$filename.trail"
+fi
+
 cd "$SCRIPT_DIR"
+echo "Compiling in: $compile_dir"
 rm -rf "$compile_dir"

report.tex

@@ -233,7 +233,7 @@ 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:
+\textit{ProMeLa} code placed in the \texttt{ParallelReverser proctype}:
 
 \begin{minted}{c}
 int n;
@@ -377,6 +377,32 @@ ltl correctness_par {
 This property is clearly not generally true as the first thread may not complete
 the reversal process before the second thread terminates due to concurrency.
 
+Here is the counterexample Spin provides to show that the property does not hold
+for some executions with $N = 2$, $\text{LENGTH} = 3$ and $R = 2$:
+
+\begin{verbatim}program start
+a[0]: 1
+a[1]: 0
+a[2]: 0
+sequential start
+parallel start
+r_s[2] = a[0]
+r_s[1] = a[1]
+r_s[0] = a[2]
+proc[1]: started from=0 to=1
+proc[2]: started from=1 to=3
+proc[2]: r_p[1] = a[1]
+proc[2]: r_p[0] = a[2]
+proc[2]: ended
+\end{verbatim}
+
+Indeed, the output shows that the second thread can terminate before the first
+does. Here, the first thread (\texttt{proc[1]}) is just started but does not
+manage to execute \mintinline{c}{r_p[2] = a[0]} before the second thread
+terminates. Indeed, this is a realistic counterexample that could be reproduced
+in the Java program.
+
+
 
 The citation \cite{tange_2023_7855617}.