From 5c7c075891aead4afd57642f0f56d5224e1c3f9e Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 17 Nov 2021 15:39:05 +0100
Subject: [PATCH] [eacsl] Update documentation
---
src/plugins/e-acsl/doc/userman/changes.tex | 6 ++
src/plugins/e-acsl/doc/userman/provides.tex | 95 +++++++++++++++++++
src/plugins/e-acsl/man/e-acsl-gcc.sh.1 | 16 +++-
src/plugins/e-acsl/scripts/e-acsl-gcc.sh.comp | 2 +-
4 files changed, 113 insertions(+), 6 deletions(-)
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index 23a76db9472..1b8489a9bb5 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -6,6 +6,12 @@ release. First we list changes of the last release.
% Next version
%\section*{E-ACSL \eacslpluginversion \eacslplugincodename}
+\section*{E-ACSL \eacslpluginversion \eacslplugincodename}
+
+\begin{itemize}
+\item New section \textbf{Concurrency Support}.
+\end{itemize}
+
\section*{E-ACSL 24.0 Chromium}
\begin{itemize}
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 8c7055d64dc..d4c58858c66 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -305,6 +305,101 @@ further passed \shortopt{m64} or \shortopt{m32} options to generate code using
At the present stage of implementation \eacsl does not support generating
executables with ABI different to the default one.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Concurrency Support}\label{sec:eacsl-gcc:concurrency}
+
+\subsubsection{How to Activate Concurrency}
+
+\eacsl supports the monitoring of Linux's \texttt{pthreads} concurrent code by
+using the option \longopt{concurrency} of \eacslgcc.
+
+Example of compilation with concurrency support using \eacslgcc:
+\begin{shell}
+ \$ e-acsl-gcc.sh -c foo.c --concurrency -o foo.frama.c -O foo
+\end{shell}
+
+The concurrency support is a two part activation: first the
+\longopt{e-acsl-concurrency} \framac option is enabled to generate concurrent
+ready code, then when compiling the generated code, the preprocessor variable
+\texttt{E\_ACSL\_CONCURRENCY\_PTHREAD} is defined and the linker option
+\shortopt{pthread} is added.
+
+Example of compilation with concurrency support using \framac and \gcc directly
+(where \texttt{\$E\_ACSL\_SHARE} points to the \texttt{share/frama-c/e-acsl}
+folder of \framac and \texttt{\$E\_ACSL\_LIB} points to the
+\texttt{lib/frama-c/e-acsl} folder of \framac):
+\begin{shell}
+ \$ frama-c \
+ -remove-unused-specified-functions \
+ -machdep gcc_x86_64 \
+ -cpp-extra-args="-std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE \
+ -D__FC_MACHDEP_X86_64" \
+ -no-frama-c-stdlib \
+ foo.c \
+ -e-acsl -e-acsl-concurrency \
+ -then-last -print -ocode foo.frama.c
+ \$ gcc \
+ -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants \
+ -Wno-attributes -Wno-implicit-function-declaration \
+ -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_CONCURRENCY_PTHREAD \
+ -I\$E_ACSL_SHARE \
+ -o foo.e-acsl \
+ foo.frama.c \
+ \$E_ACSL_SHARE/e_acsl_rtl.c \
+ -pthread \
+ \$E_ACSL_LIB/libeacsl-dlmalloc.a \
+ -lgmp -lm
+\end{shell}
+
+\subsubsection{Function Contracts Limitations}
+
+For now, the \eacsl language~\cite{eacsl} does not support concurrent access
+indications, so some care should be taken when writing specifications that
+access to the shared memory. As a workaround, the memory accesses inside the
+specification can be protected code outside the specification, for instance by
+acquiring and releasing a lock around \eacsl assertions.
+
+As an example, the following code acquire the lock on a mutex before accessing
+the shared global variable \texttt{a}. However, \eacsl will place the
+translation of the precondition before acquiring the lock, and the translation
+of the postcondition after releasing the lock. Therefore, their validity status
+may vary with respect to the thread interleaving.
+
+\begin{minipage}{\linewidth}
+\begin{ccode}
+/*@ requires \valid(a) && \initialized(a);
+ requires \valid(b) && \initialized(b);
+ ensures *a == \old(*a) + 1;
+ ensures *b == \old(*b) + *a; */
+void f() {
+ pthread_mutex_lock(&lock);
+ *a += 1;
+ *b += *a;
+ pthread_mutex_unlock(&lock);
+}
+\end{ccode}
+\end{minipage}
+
+The workaround here is to move the function contract to a statement contract
+surrounded by the lock:
+
+\begin{minipage}{\linewidth}
+\begin{ccode}
+void f() {
+ pthread_mutex_lock(&lock);
+ /*@ requires \valid(a) && \initialized(a);
+ requires \valid(b) && \initialized(b);
+ ensures *a == \old(*a) + 1;
+ ensures *b == \old(*b) + *a; */
+ {
+ *a += 1;
+ *b += *a;
+ }
+ pthread_mutex_unlock(&lock);
+}
+\end{ccode}
+\end{minipage}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Documentation}\label{sec:eacsl-gcc:doc}
diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
index c8e2e1fc53e..c8b71244e57 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -102,6 +102,9 @@ use the \fBFrama-C\fP standard library instead of a system-wide one.
.B -M, --full-mtracking
maximize memory-related instrumentation.
.TP
+.B --concurrency
+enable concurrency support.
+.TP
.B --temporal
enable checking for temporal memory errors in \\\fBvalid\fP and \\\fBvalid_read\fP predicates.
.TP
@@ -167,11 +170,14 @@ Valid arguments are:
restrict annotations to a given list of functions.
\fIOPTSTRING\fP is a comma-separated string comprising function names.
.TP
-.B --stack-size=\fI<NUMBER>
-set the size (in MB) of the stack shadow space
-.TP
-.B --heap-size=\fI<NUMBER>
-set the size (in MB) of the heap shadow space
+.B --zone-sizes=\fI<NAME1:SIZE1,...,NAMEN:SIZEN>
+set the size (in MB) of the given zones.
+
+Valid zone names are:
+ \fIstack\fP \- stack shadow space
+ \fIheap\fP \- heap shadow space
+ \fItls\fP \- TLS shadow space
+ \fIthread-stack\fP \- thread stack shadow space
.TP
.B -k, --keep-going
continue execution after an assertion failure
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh.comp
index da945788460..face0dc29f1 100644
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh.comp
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh.comp
@@ -41,7 +41,7 @@ _eacsl_gcc() {
--gmp --full-mtracking --rte= --rte-select=
--frama-c-stdlib --libc-replacements
--temporal --free-valid-address --weak-validity --validate-format-strings
- --heap-size --stack-size
+ --zone-sizes=
--with-dlmalloc --dlmalloc-from-sources --dlmalloc-compile-only
--dlmalloc-compile-flags --odlmalloc"
--
GitLab