6-Revue_litterature.tex

\Chapter{REVUE DE LITTÉRATURE}\label{sec:RevLitt}

Le \emph{model-checking} rassemble des techniques permettant de vérifier
et valider des systèmes. Historiquement, le model-checking a
tout d'abord été utilisé pour la vérification de composants
électroniques. Les techniques ont ensuite été adaptées afin de permettre
la validation de programmes. On parle alors de model-checking logiciel.
Nous allons par la suite nous intéresser à celui-ci uniquement.

Le principe du model-checking est de mener une recherche
exhaustive à travers une modélisation du système plutôt que de
construire une preuve formelle de validité. Alors qu'une telle preuve
peut demander une certaine part d'intuition, le model-checking permet
une approche plus systématique, qui peut être plus facilement
automatisée.

De nombreux algorithmes de model-checking ont été développés en fonction
des propriétés à vérifier sur le système, du formalisme dans lequel est
décrit le système et de la complexité de celui-ci.
Dans ce chapitre, nous présentons les principales techniques de
model-checking logiciel et nous identifions leurs avantages et
inconvénients respectifs.

Nous identifions les outils les plus performants implémentant chacune de ces
techniques, à l'heure actuelle. Nous restreignons cependant cette étude aux
outils qui nous intéresseront pour la suite de ce rapport. Ces outils sont donc
susceptibles d'être utilisés en arrière-plan (backend) pour la vérification des
codes sources considérés dans ce mémoire. Nous ne considérerons donc que
des outils capables de vérifier des programmes concurrents en C, suivant le
modèle d'exécution défini par la norme POSIX (pThread).

\textbf{Structure :} Dans la section~\ref{sec:model-checking-logiciel}, nous
définissons le model-checking logiciel ainsi que les formalismes associés.
Dans la section~\ref{sec:specification}, nous présentons
les types de propriétés des programmes vérifiables grâce au model-checking et
les formalismes utilisés pour les exprimer et les représenter formellement.
Enfin, dans la section~\ref{sec:techniques-et-outils-de-model-checking}, nous
présentons différentes techniques utilisées pour le model-checking de programmes
multi thread ainsi que les outils qui les implémentent.

\section{Model-checking logiciel}\label{sec:model-checking-logiciel}

Le model-checking permet de prouver qu'un modèle d'un système vérifie une
spécification. Avant de nous intéresser davantage aux différentes techniques de
model-checking, nous allons présenter les notions de modèle et de spécification.
Nous définissions aussi un certain nombre de notions et termes techniques liés à
cette problématique.

\subsection{Modèle}

Le point caractéristique du model-checking est l'utilisation de
\emph{modèles} des systèmes à vérifier. Un modèle est une représentation
abstraite du système. Au lieu de vérifier un système directement, les techniques
de model-checking s'appliquent sur le modèle du système. On considère un
système comme correct lorsque son modèle ne contient pas d'erreurs.

L'origine des modèles est liée au domaine d'application initial du
model-checking : la vérification du design de composants électroniques. Il
était nécessaire de représenter ces derniers de manière abstraite afin de les
vérifier, ce qui a donné naissance à la notion de modèles.

L'utilisation d'un modèle permet de simplifier les tâches de vérification : un
modèle bien conçu capture le fonctionnement du système en retirant les détails
n'ayant pas d'impact sur les propriétés à vérifier. Cette version simplifiée du
système permet ainsi de réaliser des tâches de vérification complexes, qui ne
pourraient aboutir autrement. Cependant, le modèle doit être suffisamment fidèle
pour préserver les propriétés à vérifier. Un modèle trop simple pourrait
provoquer l'apparition de faux positifs ou pire, ne pas contenir une erreur
pourtant bien présente dans le système.

La phase de modélisation est donc une phase délicate et propice aux erreurs. Il
est nécessaire de bâtir un équilibre entre l'abstraction du système et le
respect de son fonctionnement. Cet équilibre dépend des propriétés que l'on
souhaite vérifier. La modélisation demande donc une bonne connaissance
du système et des outils de model-checking utilisés. Les tendances actuelles
visent à réduire l'intervention humaine dans la phase de modélisation en
automatisant celle-ci.

\subsection{Système de transitions et trace d'exécution}

Un modèle prend souvent la forme d'un système de transitions.

\paragraph{Système de transitions}
Formellement, un système de transitions est un triplet \((S, s_0, \rightarrow)\),
avec :

\begin{itemize}
\item
  \(S\) l'ensemble des états du système ;
\item
  \(s_0 \in S\) l'état initial du système ;
\item
  \(\rightarrow \subset S \times S\) la relation de transitions du
  système ;
\end{itemize}

Intuitivement, les états d'un système de transitions représentent un
statut possible du système, tandis que les transitions représentent les
actions qui peuvent le faire évoluer.

\paragraph{Trace d'exécution}
Une trace d'exécution est un chemin dans le système de transition représentant
le modèle, possiblement infini, dont le premier état est l'état initial du
système de transition. Une trace d'exécution est donc formée d'une suite \(s_0,
s_1, .. \in S\) d'états, avec \(s_0\) l'état initial, et d'une suite \(t_0, t_1,
... \in \rightarrow\) de transitions telles que \(\forall i, t_i = (s_i,
s_{i+1})\).

Le model-checking consiste à examiner l'ensemble des traces
d'exécution du modèle afin de vérifier si elles respectent la spécification.

\subsection{Vocabulaire technique}

Nous allons définir ici un certain nombre de termes liés au model-checking ou
aux méthodes formelles de manière générale, que nous réutiliserons par la suite.

\paragraph{Faux positif / Faux négatif}

Lorsqu'un outil de vérification indique une erreur dans un système alors que ce
dernier est en fait correct, on parle de \emph{faux positif}. À l'inverse, si un
outil reporte un système comme correct alors qu'il contient une erreur, on parle
de \emph{faux négatif}.

\paragraph{Complet / Correct}

Un outil ou une technique de vérification est complet s’il est conçu de sorte à
ne jamais faire de faux négatif : si une erreur existe dans un système, elle
sera toujours signalée.
Un outil ou une technique de vérification est correct s’il est conçu de sorte à
ne jamais faire de faux positif : si une erreur est signalée dans un système,
elle est réellement présente dans ce système.

Concevoir un outil de model-checking logiciel à la fois complet et correct est
extrêmement difficile, voire impossible, dans la plupart des cas. En effet, le
théorème de Rice indique que toute propriété sémantique non triviale d'un
programme est indécidable. Une technique de vérification ne respecte donc généralement
qu'une seule de ces caractéristiques, ou aucune des deux.

\subsection{Le cas du model-checking logiciel}

Le model-checking logiciel, ou \emph{software model-checking}, est un cas
particulier de model-checking. Le système à vérifier est un programme, et le
modèle va être extrait automatiquement à partir de son code source.
On automatise ainsi la conception du modèle, ce qui présente les avantages
suivants :

\begin{itemize}
\item
  on réduit le risque d'erreur lors de la modélisation du système,
  en supprimant l'intervention humaine ;
\item
  on automatise davantage le procédé de vérification, ce qui le rend
  plus facilement utilisable en pratique.
\end{itemize}

Cependant, le code doit encore être compilé afin d'obtenir le système,
ce qui constitue une encore une certaine distance entre le modèle et le
système. Afin de réduire cette distance, certains
model-checkers logiciels se basent sur des représentations intermédiaires
plus proches de l'assembleur, comme la représentation intermédiaire de
LLVM\footnote{L'utilisation de cette représentation est aussi expliquée
  par des raisons de compatibilité. De nombreux langages, dont C, C++ et
  C\# peuvent en effet être compilés vers la représentation
  intermédiaire de LLVM, un model-checker utilisant cette dernière est
  alors compatible avec tous ces langages.}.

La programmation impérative consiste à considérer un programme comme un état que
l'on fait évoluer à l'aide d'instructions. L'état du programme est
principalement défini par l'état de la mémoire du programme.
On peut alors modéliser un programme par un système de transition. L'ensemble
des états du système de transition est une partition de l'ensemble des états du
programme. Les états du système de transition sont donc caractérisés par :

\begin{itemize}
\item
  la configuration du tas du programme ;
\item
  la valeur des variables globales du programme ;
\item
  la configuration de la pile de chaque thread ;
\item
  la valeur du pointeur d'instruction de chaque thread.
\end{itemize}

Les instructions permettant de faire évoluer l'état du programme sont
représentées par des transitions entre les états de son modèle. Une transition
représente plus précisément l'action d'une instruction atomique du programme sur
les trois zones mémoires citées précédemment. Les transitions peuvent aussi
dépendre de facteurs externes, comme les entrées du programme.

Dans le cadre du model-checking logiciel, deux hypothèses sont fréquemment
faites sur le système :

\begin{itemize}
\item
  la consistance séquentielle. On considère alors que les écritures et
  les lectures mémoires ont lieu dans l'ordre où les instructions sont
  rencontrées dans une trace d'exécution. En pratique, cette hypothèse
  n'est pas toujours vérifiée. Les compilateurs et les processeurs
  peuvent modifier l'ordre de ces opérations pour optimiser un
  programme. On parle alors de modèle mémoire \emph{faible}.
\item
  la sémantique d'entrelacement. Dans le cas d'un système multi thread,
  on considère que les traces d'exécution possibles sont produites par
  un entrelacement des instructions atomiques de chaque thread. Cette
  hypothèse n'est pas valide si le programme est exécuté par plusieurs
  processeurs : il est alors possible d'exécuter plusieurs instructions
  simultanément, ce qui peut produire des traces d'exécution
  supplémentaires.
\end{itemize}

\paragraph{Exemple}

Considérons le programme suivant, formé de deux threads.

\noindent\begin{minipage}{.45\textwidth}
\begin{lstlisting}[caption=Thread 1, frame=single]
a <- 1
a <- 2
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[caption=Thread 2,frame=tlrb]
c <- 1
d <- a + c
\end{lstlisting}
\end{minipage}

Ce programme contient trois variables globales, \texttt{a}, \texttt{c} et
\texttt{d}, et deux threads. Les états du système sont donc définis par les
valeurs de ces variables et la position des pointeurs d'instruction de chaque
thread. On peut modéliser ce programme par le système de transitions en Figure
\ref{fig:model_example}. L'étiquette de chaque état représente la valeur des
variables. Les transitions représentent l'exécution d'une instruction. On
remarque l'existence de nombreuses traces d'exécution, pouvant mener à trois
résultats différents.

\begin{figure}
\begin{center}
\includegraphics[width=\textwidth]{model_example}
\end{center}
\caption{Système de transition modélisant un programme simple.}
\label{fig:model_example}
\end{figure}

\subsection{Non-déterminisme}

Un système est rarement complètement déterministe. De nombreux facteurs (les
données en entrée du système, l'instant où un évènement a lieu, la réussite des
allocations mémoires, la concurrence) tendent généralement à rendre l'évolution
d'un système non déterministe.

Face à un choix non déterministe, les techniques de model-checking doivent
explorer toutes les alternatives possibles.

Lors de la modélisation, certaines sources de non-déterminisme sont ignorées.
Elles sont alors remplacées par une exécution déterministe.
C'est généralement le cas pour les appels système ayant la possibilité
d'échouer (les allocations de mémoire, par exemple).

Pour représenter les évènements et les paramètres extérieurs du programme,
une fonction simulant le non-déterminisme est généralement mise à disposition
de l'utilisateur par les outils de model-checking.

\subsection{Explosion combinatoire}

Le nombre d'états d'un programme augmente exponentiellement selon de nombreux
paramètres (nombre de variables du programme, taille des types de données, degré
de concurrence\dots). Il peut éventuellement être infini si des appels de
fonctions ou de l'allocation dynamique de mémoire entrent en jeu. Cependant, afin
de vérifier un système, un model-checker doit explorer l'ensemble de ces états.
Cette tâche devient donc extrêmement coûteuse en temps et en mémoire quand le
nombre d'états devient trop important.
Ce problème, nommé l'explosion combinatoire, est la principale limite du
model-checking.

Le non-déterminisme est une des principales raisons de l'explosion combinatoire :
le nombre d'exécutions est exponentiel selon le nombre de choix non déterministe.

Cela explique les difficultés rencontrées par les techniques de model-checking
face aux programmes concurrents : l'ordonnancement entre les instructions est
non-déterministe. Il existe un nombre d'entrelacements exponentiel en fonction
du nombre d'instructions du programme.

Les différents algorithmes de model-checking utilisent tous des
techniques afin de limiter l'explosion combinatoire. Elle reste
cependant le plus grand obstacle rencontré par le model-checking et
limite le passage à l'échelle de la plupart des techniques.

\section{Formalismes de spécification}\label{sec:specification}

Afin de vérifier un système, il faut tout d'abord établir ce que signifie être
correct pour ce système. Un ingénieur responsable du design d'un système a
généralement une connaissance informelle de la manière dont le système doit se
comporter. Il est alors nécessaire de traduire cette connaissance d'une manière
non ambiguë et compréhensible par des outils. On réalise pour cela une
spécification du système.

Une spécification est constituée d'un ensemble de propriétés, qui représentent
des invariants logiques que le système doit respecter. Si l'un de ces invariants
est brisé, une erreur est présente : le système ne se comporte pas de la manière
attendue. Un outil de vérification peut alors inspecter un système afin de
vérifier si l'ensemble de la spécification est respecté.

Une spécification peut prendre de nombreux aspects : il existe des langages de
spécification (UML par exemple), elle peut être constituée de formules logiques
portant sur les variables du système ou prendre la forme d'un système de
transitions. Un langage de programmation constitue en lui même une spécification
bas niveau du comportement d'un programme.

Les propriétés d'une spécification se répartissent en plusieurs catégories. Une
propriété peut être un comportement généralement attendu pour le type de système
concerné. Par exemple, on attend généralement d'un programme qu'il ne contienne
pas de comportements indéterminés. Une propriété peut aussi être spécifique au
système et à son comportement. On peut par exemple spécifier qu'une variable ne
doit jamais dépasser un certain seuil.

\subsection{\texorpdfstring{Propriétés ``built-in''}{Propriétés built-in}}

Certaines propriétés sont fortement --- si ce n'est toujours --- désirables
pour une catégorie de systèmes. Un model-checker ciblant cette catégorie
de systèmes peut alors implémenter la vérification de ces propriétés
nativement, sans qu'il soit nécessaire de les spécifier. On parle alors
de propriétés \emph{built-in}.

Dans le cas du model-checking logiciel, des propriétés built-in
classiques sont la vérification de la validité des pointeurs et des
opérations arithmétiques, l'initialisation des variables et, de manière
plus générale, l'absence de tout comportement ne respectant pas la norme
du langage.
Dans le cas de programmes concurrents, on cherche généralement à s'assurer de
l'absence de dreadlocks (lorsque tous les threads du programme sont bloqués par une
condition, et que le système ne peut plus évoluer) et de data-races (plusieurs
accès simultanés à une même adresse mémoire, dont au moins un en écriture).

Les propriétés built-in sont souvent des propriétés qu'il serait difficile à
l'utilisateur de spécifier, parce qu'elles impliquent la plupart des variables
du système.

Pour vérifier des propriétés plus spécifiques au système (des propriétés
fonctionnelles par exemple, qui portent sur le résultat que le système doit
produire) il est cependant nécessaire de permettre à l'utilisateur d'exprimer
lui-même la spécification.

\subsection{Assertions}

Dans un article de son blog, John Regehr aborde le sujet des
assertions\cite{assertion_regehr}.
Il reprend en particulier la définition suivante :

\begin{quotation}
\selectlanguage{english}
An assertion is a Boolean expression at a specific point in a program which will
be true unless there is a bug in the program.
\hfill \cite{assertion_regehr}
\end{quotation}

%% \begin{quotation}
%% ASSERT(expr)

%% Asserts that an expression is true. The expression may or may not be evaluated.

%% If the expression is true, execution continues normally.
%% If the expression is false, what happens is undefined.
%% \hfill \cite{assertion_regehr}
%% \end{quotation}

\selectlanguage{french}

Cette définition présente les assertions comme un mécanisme de spécification
exécutable. Si une assertion n'est pas respectée, une erreur est présente dans
le programme. Les assertions sont présentes dans la plupart des langages de
programmation. Elles ont été naturellement reprises par les méthodes de
vérification formelle, dont le model-checking logiciel.

Les assertions permettent de vérifier des propriétés d'accessibilité. Ces
propriétés consistent à vérifier s’il est possible d'atteindre un état donné du
modèle. Cet état est appelé un état d'erreur. On peut aussi considérer
l'accessibilité d'un ensemble d'états d'erreurs.

Les propriétés d'accessibilité sont des propriétés relativement simples :
déterminer si un état est un état d'erreur ne dépend que de cet état. Un
programme contient donc une erreur dès qu'il est possible d'atteindre un état
d'erreur, indépendamment des états et des transitions empruntées au cours de
l'exécution. Une propriété d'accessibilité peut ainsi être déterminée par une
exploration (en largeur par exemple) du système.

Dans un programme, une assertion prend la forme d'une instruction telle que :\\
\texttt{assert(condition);}.
Si elle est exécutée et que la condition est évaluée à vrai, alors l'exécution
du programme continue normalement.
Sinon, le programme a atteint un état d'erreur. Son comportement est alors
indéterminé, bien que le comportement le plus fréquent soit de stopper son
exécution.

Plus formellement, l'assertion \texttt{assert(c)} désigne comme étant des
états d'erreur tous les états tels que :

\begin{itemize}
\item
  un des pointeurs d'instruction du programme pointe sur l'assertion
\item
  l'expression \texttt{c} s'évalue à faux
\end{itemize}

Dans le code suivant, une assertion permet de spécifier que la variable
\texttt{b} doit être non nulle. Dans le cas contraire, une erreur
arithmétique (division par zéro) pourrait avoir lieu à la ligne suivante.

\begin{lstlisting}[language=C, frame=single]
int int_div(int a, int b) {
    assert(b != 0);
    return a / b;
}
\end{lstlisting}

Les assertions sont très utilisées en raison de leur simplicité.
Elles peuvent de plus être placées en tant que spécification pour un outil de
vérification, ou permettre de signaler une erreur dans une version exécutable
du programme (il ne faut cependant pas les confondre avec un mécanisme de
gestion d'erreurs).

Cependant, le pouvoir d'expression des assertions est limité. Toutes les
propriétés d'accessibilité ne peuvent pas être exprimées par une assertion : il
n'est par exemple pas possible d'utiliser dans la condition d'une assertion des
variables hors du contexte courant. Il n'est pas non plus possible d'exprimer un
problème d'exclusion mutuelle : il faudrait pour cela référer à la position des
autres pointeurs d'exécution du code, ce qui n'est pas possible à l'aide d'une
assertion.

\subsection{Logique temporelle}

Pour exprimer des propriétés plus complexes et en particulier des propriétés qui
portent sur l'ensemble d'une trace d'exécution et l'ordre d'apparition de
certains évènements, il est plus approprié d'utiliser une logique temporelle.

Supposons que notre système soit le code d'un distributeur automatique.
On voudrait s'assurer que le distributeur ne délivre jamais le produit
avant que le client ait payé, ce qui va revenir dans le code à vérifier
que la fonction \texttt{livrer\_produit} (qui commanderait au système
de donner au client l'objet commandé) n'est jamais appelée avant la
fonction \texttt{accepter\_paiement} (qui validerait que le paiement a
été correctement effectué), au cours d'une transaction. Des assertions
permettent de déterminer si chacune de ces fonctions est atteinte, mais
sans introduire des variables auxiliaires, il n'est pas possible de
déterminer l'ordre des appels.

Les logiques temporelles permettent d'exprimer ce type de propriétés. On
peut ainsi spécifier, pour un programme, des propriétés sur la
succession des états d'une trace d'exécution.

Ci-dessous sont listés quelques-un des schémas de propriétés les plus
courantes. Davantage sont présenté par \citep{LTL_scheme}. Soit \(p\) une
propriété portant sur les états du système.

\begin{itemize}
\item
  propriété de sûreté : tous les états atteints pendant l'exécution
  vérifient la propriété \(p\).
\item
  propriété d'accessibilité : en un temps fini, un état vérifiant la
  propriété \(p\) est atteint.
\item
  propriété d'équité : on atteindra infiniment souvent un état vérifiant la
  propriété \(p\).
\end{itemize}

Les logiques temporelles les plus utilisées sont : \acl{LTL} (\ac{LTL})
et \ac{CTL}.

\ac{LTL} et \ac{CTL} différent principalement par leur vision de l'ensemble des
traces d'exécution. \ac{LTL} considère chaque trace indépendamment. Un
système est valide par rapport à une propriété \ac{LTL} si toutes ses traces
d'exécution respectent la propriété. \ac{CTL} considère l'ensemble des traces
comme un arbre et permet de quantifier universellement
ou existentiellement sur les successeurs de chaque nœud.

Les pouvoirs d'expressivités de \ac{LTL} et \ac{CTL} ne sont ni équivalents, ni même
comparables. En effet, \ac{LTL} ne permet pas de quantifier existentiellement :
une formule \ac{CTL} utilisant une quantification existentielle n'a donc pas
toujours d'équivalent en \ac{LTL}. La réciproque peut être présentée à l'aide de
la propriété \ac{LTL} \(F (p \land X p)\) (pour toutes les traces, on atteint un
état vérifiant \(p\) et dont le successeur vérifie \(p\)) n'a pas d'équivalent
dans \ac{CTL}. La formule \ac{CTL} \(AF (p \land AX p)\) (quelque soit le chemin
emprunté, on atteint un état vérifiant \(p\) et dont tous les successeurs
vérifient \(p\)) pourrait sembler un bon candidat, mais la Figure
\ref{LTL_vs_CTL} présente un modèle vérifiant \(F (p \land X p)\) mais ne
vérifiant pas \(AF (p \land AX p)\).

\begin{figure}
\begin{center}
\includegraphics[width=0.4\textwidth]{LTL_CTL_non_equivalent.png}
\caption{Modèle vérifiant \(F (p \land X p)\) mais pas \(AF (p \land AX p)\).}
\label{LTL_vs_CTL}
\end{center}
\end{figure}

\ac{CTL} est considérée comme plus difficile à comprendre par les ingénieurs,
plus habitués à penser à une unique exécution linéaire plutôt qu'à un arbre
d'exécution\cite{RCTL_formulas}. \ac{CTL} est par conséquent moins utilisée que
\ac{LTL} dans le cadre du model-checking logiciel. Par la suite, nous allons
donc nous concentrer sur \ac{LTL} uniquement.

\subsection{LTL : Logique Temporelle Linéaire}

La définition de \ac{LTL}\cite{pnueli_LTL} ajoute deux opérateurs temporels à la
logique classique, \(next\) (\(X\)) et \(until\) (\(U\)). La syntaxe d'une
formule \ac{LTL} est définie de la manière suivante, pour \(\phi\) et \(\psi\)
deux formules \ac{LTL} :

\[
\phi, \psi := \text{true }| \text{ false } | \text{ p } |
             \phi \land \psi | \lnot \phi | X \phi | \psi U \phi
\]

\(p\) est une proposition sur l'état du système. On nommera par la suite
ces propriétés des \emph{propositions atomiques}. On identifiera aussi
une proposition atomique avec sa fonction d'évaluation, c'est-à-dire la
fonction qui indique si un état du système vérifie la propriété ou non.

Étant donnée une trace d'exécution infinie \(s = (s_0, s_1, ...)\), \ac{LTL} a
la sémantique suivante :

\[
\begin{aligned}
s \models p & \equiv s_0 \models p \\
s \models X \phi & \equiv (s_1, s_2, \dots) \models \phi \\
s \models \phi U \psi & \equiv \exists k, (s_k, s_{k+1}, \dots) \models \psi
                        \land \forall i <= k, (s_i, s_{i+1}, \dots) \models \phi \\
\end{aligned}
\]

\(\lnot\), \(\land\), \(true\) et \(false\) s'interprètent de la manière
usuelle.

Une trace d'exécution est un modèle d'une proposition atomique si son premier
état est un modèle de la proposition atomique.
L'opérateur \(next\) signifie donc que la propriété \ac{LTL} passée en
paramètre doit être valide sur la trace privée de son premier état.
L'opérateur \(until\) signifie que la première propriété passée en
paramètre doit être vérifiée par tout les états de la trace jusqu'à ce qu'un
état vérifie la seconde formule.

À partir de ces opérateurs base, on définit les opérateurs \(\lor\),
\(\implies\), \dots de la manière classique. On définit aussi les
opérateurs temporels \(always\) (\(G\)), signifiant qu'une propriété est
vraie pour tous les états d'une trace et \(finally\) (\(F\)), signifiant
qu'un état vérifiant une propriété est atteint dans le futur.

\[
\begin{aligned}
F p & \equiv \text{true} U p \\
G p & \equiv \lnot F (\lnot p)\\
\end{aligned}
\]

Enfin, on définit un système comme étant valide par rapport à une
formule \ac{LTL} si toutes les exécutions de ce système sont des modèles de
la formule.

\subsection{Automates de Büchi}

Vérifier si un système respecte une proposition \ac{LTL} demande d'être capable de
manipuler efficacement ces dernières. On utilise pour cela les automates de
Büchi. Ils permettent de représenter une propriété \ac{LTL}. Sous cette forme, elles
sont plus simples à manipuler pour un model-checker. Toute formule \ac{LTL} peut être
représentée par un automate de Büchi. Il existe des algorithmes pour construire
efficacement et automatiquement cet automate\citep{ltl2ba}.

Afin de vérifier si un système respecte une propriété \ac{LTL}, une méthode classique
est de construire un automate de Büchi qui représente la négation de cette
formule \ac{LTL} et d'explorer la composition entre cet automate et le système de
transitions modélisant le système. Un chemin acceptant représente alors une
exécution du système qui viole la propriété.

\paragraph{Automates de Büchi}
Un automate de Büchi est un automate qui accepte un langage de mots
infinis. Formellement, un automate de Büchi est un quintuplé
\(B = (S, \Sigma, I, \delta, F)\), avec :

\begin{itemize}
\item
  \(S\) un ensemble d'états ;
\item
  \(\Sigma\) un alphabet ;
\item
  \(I \subset S\) est un ensemble d'états initiaux ;
\item
  \(\delta \subset (S, \Sigma, S)\) est la relation de transition ;
\item
  \(F \subset S\) est l'ensemble des états finaux.
\end{itemize}

Un calcul (les mots chemin ou trace sont aussi utilisés) dans \(B\) est une
suite infinie de transitions consécutives \(c \in \delta^\omega\), dont l'état
de départ est un état initial :

\[
c = (s_0, a_0, s_1)(s_1, a_1, s_2)\dots(s_n, a_n, s_{n+1})\dots
\]

L'étiquette de ce chemin est le mot infini \(a = (a_0, a_1, \dots, a_n) \in
\Sigma^\omega\). Le chemin \(c\) est réussi si et seulement s’il passe une
infinité de fois par un état final de \(B\).

L'automate \(B\) accepte un mot \(a\) si et seulement s’il existe un calcul réussi dans \(B\) ayant le mot \(a\) pour étiquette.

Pour représenter une formule \ac{LTL}, on prend \(\Sigma = 2^P\), avec \(P\)
l'ensemble des propositions atomiques de la formule. Une lettre de
l'alphabet représente ainsi une configuration des propositions atomiques
du système.

\paragraph{Exemples}

La figure \ref{fig:buchi_example} présente les automates de Büchi pour trois propriétés
\ac{LTL} simples : \(Gp\), \(F(p \lor q)\) et \(G(Fp)\). Seule la partie accessible des automates
est représentée, et les transitions ayant les mêmes sources et destinations sont fusionnées,
leurs étiquettes étant remplacées par une garde sous la forme d'une expression logique.

\begin{figure}
\begin{center}
\includegraphics[height=.17\textheight]{buchi_1.png}
\includegraphics[height=.3\textheight]{buchi_3.png}
\includegraphics[height=.3\textheight]{buchi_2.png}
\end{center}
\caption{Automates de Büchi pour les formules LTL $G p$, $F(p \lor q)$ et
$GF p$.}
\label{fig:buchi_example}
\end{figure}

\paragraph{Automate produit}

Soient un automate de Büchi \(B = (S_B, \Sigma, I_B, \delta, F_B)\) représentant
une propriété \ac{LTL} \(\phi\) et un système de transitions \(T = (S_T, \rightarrow,
I_B)\) modélisant un système.

L'automate produit de \(B\) et \(T\) est définit comme étant \(P = (S_P, \Sigma,
I_P, \delta_P, F_P)\), avec :

\begin{itemize}
\item
  \(S_P = S_B \times S_T\)
\item
  \(I_P = I_B \times I_T\)
\item
  \(F_P = F_B \times S_T\)
\item
  \(((p, q), s, (p', q')) \in \delta_P\) si et seulement si :

  \begin{itemize}
  \item
    \((p, p') \in \rightarrow\)
  \item
    \((q, s, q') \in \lambda\)
  \item
    \(p \models s\)
  \end{itemize}
\end{itemize}

Un mot est accepté par l'automate produit si et seulement s’il représente
une exécution valide dans le modèle du système et qu'il appartient au langage
de l'automate de Büchi.
L'automate produit \(P\) reconnaît donc exactement le langage des exécutions du
modèle \(T\) qui vérifient la propriété \ac{LTL} représentée par l'automate de
Büchi \(B\).

\paragraph{Vérifier une propriété LTL}

Vérifier si le modèle \(T\) respecte la propriété \(\phi\), revient à calculer
si le langage des exécutions valide de \(T\) est inclus dans le langage de
l'automate de Büchi \(B\). Cependant, vérifier une inclusion est une opération
complexe. Il est plus simple de calculer si langage est vide ou non. On va donc
reformuler le problème : on va chercher à déterminer si le langage \(L\) des
exécutions valides dans \(T\) et ne respectant \emph{pas} \(\phi\) est vide.
Si c'est le cas, le système est correct. Sinon, une erreur est présente et les
éléments de \(L\) représentent des contre-exemples.

Pour calculer le langage \(L\), on va construire le produit entre le système de
transitions du modèle et l'automate de Büchi représentant la \emph{négation} de
\(\phi\). Le langage de l'automate produit est alors constitué des exécutions valides du
modèle qui ne respectent pas \(\phi\), soit \(L\).

Il suffit alors d'explorer l'automate produit. S’il est possible, à partir
de l'état initial, d'atteindre un cycle contenant au moins un état final, alors,
\(L\) n'est pas vide : il contient au moins le mot composé par l'étiquette du
chemin allant jusqu'au cycle et d'une infinité de répétitions de l'étiquette du
cycle. Ce mot correspond à une exécution du système qui viole la propriété \(\phi\),
et pourra servir de contre-exemple à l'utilisateur.

L'encodage des propriétés \ac{LTL} à l'aide des automates de Büchi permet ainsi de
vérifier des propriétés complexes sur les modèles. Cependant, la taille d'un
automate de Büchi augmente exponentiellement avec la profondeur de la formule
qu'il représente. Dans le cas de formules de grande taille, il peut donc devenir
problématique de générer l'automate. Sa taille et son aspect non déterministe
viennent renforcer le problème d'explosion combinatoire déjà rencontré par les
techniques de model-checking.

\section{Techniques et outils de model-checking}
\label{sec:techniques-et-outils-de-model-checking}

Différents algorithmes sont utilisés par les outils de model-checking
afin d'explorer l'ensemble des états d'un modèle. Afin de lutter contre
l'explosion combinatoire, ils établissent des compromis au niveau de la
précision de la vérification et du type de propriétés qu'ils prennent en charge.
Leurs performances dépendent aussi fortement de la
structure du programme : les boucles, le non-déterminisme ou la gestion
de la concurrence sont plus ou moins bien supportés selon
les algorithmes.

À l'exception des techniques de séquentialisation, ces algorithmes ont été
initialement appliqués à des programmes séquentiels. Le support des programmes
concurrents est venu ensuite\footnote{Les algorithmes inspirés du model-checking
  de composants électroniques supportent des modèles concurrents depuis
  longtemps. Cependant, le support de la concurrence pour le model-checking
  logiciel a été ralenti par l'explosion combinatoire.}.
Ce dernier n'est pas forcément complexe, d'un point de vue théorique : un
programme multi thread peut s'exprimer comme un système de transitions
non déterministe. Les model-checkers sont capables de vérifier des modèles
non déterministes --- ils sont utilisés pour simuler les entrées possibles d'un
système par exemple --- les algorithmes de model-checking peuvent donc
théoriquement être étendus.
Le problème est bien plus complexe en pratique, en raison des contraintes de
temps et de mémoire que rencontrent les model-checkers. En raison de l'explosion
combinatoire provoquée par le nombre exponentiel d'entrelacements possibles
entre les threads, il est difficile de concevoir un algorithme performant.

Nous présentons dans cette partie les principaux algorithmes utilisés dans le
cadre du model-checking de logiciel multi thread, ainsi que certains des outils
qui les implémentent. Pour chaque algorithme, nous avons choisi les outils qui
nous ont parus les plus aboutis et ceux qui présentaient une approche originale.
Pour chaque algorithme et outil, nous tentons de mettre en valeur ses points
forts, ses faiblesses et ses spécificités.

\subsection{Model-checking explicite}

Le model-checking explicite consiste à énumérer individuellement les
états accessibles du modèle afin de les explorer. Le modèle prend la
forme d'un système de transitions et son exploration est réalisée à
l'aide d'algorithmes de graphes (exploration en largeur ou en
profondeur\dots).

Les algorithmes de model-checking explicite modélisent le programme par un
système de transitions. Ils construisent et explorent ce système de transitions
à la volée : partant de l'état de départ, les successeurs sont déterminés à
partir des instructions du programme. Ils sont alors visités à leur tour, leurs
successeurs sont calculés et ainsi de suite.
Pour ne pas explorer plusieurs fois un même état (l'exploration entrerait alors
dans un cycle infini), il est nécessaire de stocker les états du chemin
emprunté.

Le model-checking explicite est extrêmement vulnérable à l'explosion
combinatoire. Les états accessibles du système sont examinés individuellement.
S’ils sont en nombre infinis, une analyse peut ne pas terminer. Le stockage des
états explorés peut aussi devenir problématique. Plusieurs techniques existent
pour réduire l'impact de l'explosion combinatoire.

\paragraph{Stateless Model-checking}
Certains outils choisissent de ne pas maintenir la liste des états
visités afin de ne pas être limités par l'utilisation de la mémoire. On
parle alors de \emph{stateless model-checking}. Ces outils ne sont pas
capables de détecter un cycle dans le programme à analyser. Il est donc
nécessaire que toutes les exécutions du programme à analyser terminent.

\paragraph{State Hashing}
Le \emph{state hashing} consiste à ne conserver qu'une valeur de hachage des
états visités, et non pas l'état complet. L'utilisation de la mémoire est ainsi
réduite, et les performances peuvent être améliorées par l'utilisation de
structures de données capables de rechercher un élément de manière efficace
(ensemble ordonné, \dots). Cependant, il est possible (bien que très peu
probable) que deux états aient la même valeur de hachage. Ces états sont alors
considérés comme égaux, ce qui peut mener à un résultat faux de l'analyse.
Le state hashing rend donc les model-checkers incomplets.

\paragraph{Runtime model-checking}
Certains outils explorent l'espace d'états en se basant sur des
exécutions réelles du programme. Le modèle est alors le programme lui-même.
Son exécution est contrôlée par le model-checker. Ce dernier contrôle le
non-déterminisme de chaque exécution. Cette approche permet de
bénéficier des performances réelles du programme lors de l'exploration,
cependant le backtracking est plus compliqué : les outils de runtime
model-checking relancent en général une exécution du programme à tester
depuis l'état initial chaque fois qu'il est nécessaire de revenir à un
état précédent. Il est aussi complexe de mémoriser les états explorés,
cette technique est donc souvent combinée avec le \emph{stateless model
checking}.

\paragraph{Réduction par ordre partiel}
Les techniques de réduction par ordre partiel visent à réduire le nombre de
chemins à explorer dans un système concurrent. Elles permettent de supprimer les
chemins équivalents par rapport aux propriétés à vérifier, souvent en supprimant
des changements de contextes entre des instructions indépendantes. Un cas simple
de réduction consiste à regrouper en un bloc atomique une série d'instructions
manipulant uniquement des variables locales. L'entrelacement de ces instructions
avec d'autres threads n'a pas d'impact sur leur résultat, on peut donc conserver
uniquement l'ordonnancement consistant à les exécuter sans changement de
contexte.

La plupart des variantes ci-dessus sont aussi utilisées par les autres
algorithmes que nous présentons par la suite, en particulier les
techniques de réduction par ordre partiel. Cependant, le model-checking
explicite est particulièrement dépendant de ces techniques afin de
gagner en performances.

La principale force du model-checking explicite est sa précision. Explorer
l'ensemble des états de manière explicite permet de vérifier la plupart des
propriétés, spécifiées à l'aide d'assertions ou par une formule \ac{LTL}. Cependant,
il est extrêmement dépendant des techniques de réduction et a plus de
difficultés face à des programmes de grande taille.

\subsubsection{Outils}

SPIN\cite{SPIN} est l'un des premiers projets de model-checking
explicite. Il permet de vérifier des propriétés de la logique temporelle
\ac{LTL} sur des modèles exprimés en \bsc{PROMELA}. SPIN supporte nativement
les modèles concurrents et implémente de nombreuses méthodes de réduction
(ordre partiel, bit state hashing\dots). SPIN ne supporte pas le langage
C nativement, cependant des travaux ont été menés afin de traduire C
vers \bsc{Promela}\cite{jiang_C_to_Promela}, ce qui permet à SPIN de
vérifier un programme en C de manière indirecte. Cependant, cette traduction
ne supporte que partiellement les manipulations de la mémoire (pointeurs,
allocation dynamique\dots).

Pancam\cite{Pancam} se base sur SPIN pour vérifier du bytecode
LLVM\footnote{le bytecode LLVM peut être produit à partir d'un code C à
l'aide d'un compilateur tel que CLANG ou GCC}. Pancam exécute le
bytecode LLVM dans une machine virtuelle et utilise SPIN comme un
moniteur d'exécution afin de générer les différents entrelacements à
explorer.

CHESS\cite{Chess} est un outil de runtime model-checking. Étant donné un
scénario de test, il permet d'explorer l'ensemble des entrelacements à l'aide
d'un ordonnanceur. Celui-ci a la particularité de ne pas autoriser un changement
de contexte en tout point du programme : un changement de contexte est possible
lorsque une primitive de synchronisation ou un point défini par l'utilisateur
sont atteints ou lorsqu'un thread est dans une situation de livelock (son
exécution boucle en attendant une action d'un autre thread). Il permet ainsi de
limiter l'explosion combinatoire due à la concurrence.

\texttt{inspect}\cite{inspect} vérifie du code C et C++
multi thread en se basant sur un algorithme de runtime model-checking
avec une exploration \emph{stateless}. \texttt{inspect} instrumente
le programme à vérifier par des instructions lui permettant de
communiquer avec un ordonnanceur, selon une architecture client/serveur.
Le programme est ensuite exécuté pour chaque combinaison d'entrelacements,
afin d'explorer l'ensemble des traces possibles.

Divine\cite{Divine_3_0} est un model-checker capable de vérifier des
propriétés \ac{LTL} et des propriétés d'accessibilités. Il se base sur un
langage interne, DVE. Il est capable de traiter du bytecode LLVM en le
traduisant vers DVE, ce qui lui permet de supporter des langages comme C
et C++. La particularité de Divine est de mettre en place une analyse
concurrente et distribuée afin d'améliorer ses performances. Il utilise
aussi des méthodes de réduction de l'espace d'état (compression de
chemins, réduction par ordre partiel).

On retrouve à travers ces outils le besoin de performance des outils de
model-checking explicite. Divine est implémenté dans une architecture
concurrente pour améliorer ses performances, alors que \texttt{inspect} et
Pancam se basent sur du runtime model-checking. SPIN, \texttt{inspect}, Pancam
et Divine sont tous capables de vérifier des violations d'assertions et des
propriétés built-in, comme les deadlocks et les data-races, cependant, seul
Divine et SPIN sont capables de vérifier des propriétés \ac{LTL}.
\texttt{inspect} nécessite un système fermé, et n'est pas capable de gérer le
non-déterminisme. Il est donc dépendant d'une suite de tests pour fixer les
paramètres du programme à vérifier. Divine est arrivé sixième de la catégorie
portant sur les programmes concurrents lors de l'édition de 2016 de la
compétition de vérification logicielle SV-COMP\citep{svcomp_2016_result} (les
autres outils présentés ci-dessus n'ont pas participé à ces compétitions).

\subsection{Model-checking symbolique}

Les algorithmes de model-checking symbolique manipulent des ensembles d'états
du modèle représentés de manière abstraite, plutôt que d'énumérer chaque état
individuellement. Il est ainsi possible de manipuler des ensembles
d'états importants ou infinis de manière efficace. Contrairement au
model-checking explicite, le model-checking symbolique n'est donc pas limité à
un modèle fini.

L'abstraction utilisée pour représenter les ensembles d'états est un élément
clef du model-checking symbolique. Cette représentation doit permettre de
réaliser les opérations classiques sur les ensembles (union, intersection,
comparaison) de manière efficace. Les abstractions suivantes sont les plus
utilisées :

\begin{itemize}
\item
  les BDD (\emph{Binary Decision Diagrams}, Diagrammes de Décision Booléens) ;
\item
  les formules de la logique propositionnelle ;
\item
  automates finis.
\end{itemize}

Ces représentations permettent de définir des opérations efficaces sur les
ensembles. L'opération la plus complexe est généralement la comparaison de deux
ensembles, qui nécessite le choix d'une représentation canonique.

Cependant, la taille de la représentation d'un ensemble peut varier très
fortement selon le choix de la représentation canonique. Le défi du
model-checking symbolique est donc de construire et de maintenir efficacement
une représentation canonique de taille raisonnable.

\subsubsection{Représentation symbolique par des BDD}

Nous allons utiliser l'exemple des BDD pour illustrer les forces et les
défis rencontrés par les représentations symboliques.

Un BDD permet de représenter une fonction booléenne.
On va donc représenter un ensemble d'états par une fonction prenant
en paramètre un état (encodé par des variables booléennes) et indiquant s’il est dans l'ensemble représenté par la fonction ou non.

\paragraph{Encoder les états}
La première étape est d'encoder les états du système par des variables
booléennes. Une manière simple de le faire dans le cas d'un ensemble fini
d'états est de les numéroter, puis d'utiliser une variable booléenne pour chaque
chiffre de la représentation binaire (il faut donc \(log_2 n\) variables
booléennes pour \(n\) états).

Prenons l'exemple d'un système à huit états. En numérotant les états de 0 à 7 et
en prenant leur représentation binaire (sur trois bits), on obtient les
représentations suivantes : (\(000\), \(001\), \(010\), \dots, \(111\)).


Pour représenter l'ensemble composé des états \(110\) et \(111\), il suffit
de prendre sa fonction caractéristique, c'est-à-dire la fonction qui s'évalue à
vrai pour les éléments de l'ensemble et à faux sinon.

\begin{align}
  f \colon \{0, 1\}^3 & \to \{0, 1\} \\
  (x_1, x_2, x_3) & \mapsto
  \begin{cases*}
    1 & si \((x_1, x_2, x_3) \in \{(1,1,0), (1,1,1)\}\) \\
    0 & sinon
  \end{cases*}
\end{align}

Nous allons ensuite construire un BDD pour représenter cette fonction.

La construction d'un BDD repose sur la propriété suivante :

\paragraph{Décomposition des fonctions booléennes}
Soit \(k > 0\) et \(f: \mathbf{B}^k \to \mathbf{B}\) une
fonction booléenne. Alors il existe deux fonctions booléennes
\(g, h : \mathbf{B}^{k-1} \to \mathbf{B}\) telles que :

\[
f(x_1, ..., x_k) =
\begin{cases*}
  g(x_2, ..., x_k) \text{ si $x_0$ est vrai}\\
  h(x_2, ..., x_k) \text{ si $x_0$ est faux}
\end{cases*}
\]

Il est ainsi possible de définir une fonction booléenne par récursion
sur le nombre de ses variables. On va se servir de cette propriété pour
représenter la fonction booléenne par un arbre binaire de décision. On
fixe tout d'abord un ordre des variables (dans notre exemple, on prend
le bit de poids le plus fort en premier). On construit alors l'arbre
par induction :

\begin{itemize}
\item
  si la fonction est constante, on la représente par une feuille
  étiquetée par \(vrai\) ou \(faux\).
\item
  sinon, on décompose \(f\) entre \(g\) et \(h\) selon la propriété. On
  construit alors l'arbre dont le fils gauche est la représentation de
  \(g\) et le fils droit celle de \(h\) (construites selon la même méthode).
  On étiquette l'arrête vers le fils gauche par \(0\) et celle vers le fils
  droit par \(1\).
\end{itemize}

Les étiquettes d'un chemin de la racine de l'arbre à une feuille représentent
alors une valuation des variables de la fonction. L'étiquette de la feuille
indique la valeur de la fonction pour cette valuation.

Pour notre exemple, nous obtenons l'arbre de la Figure \ref{fig:BDD_tree}.

\begin{figure}[ht!]
\begin{center}
  \includegraphics[height=0.3\textheight]{BDD_tree.png}
\end{center}
\caption{Arbre binaire de la fonction \((x,y,z) \mapsto x \land y\).}
\label{fig:BDD_tree}
\end{figure}

La représentation par un arbre de décision contient \(2^{n+1} - 1\) nœuds pour
une fonction booléenne à \(n\) variables, on ne peut donc pas encore parler de
représentation efficace. Cependant, cet arbre de décision contient aussi
beaucoup de sous-arbres redondants. On va donc réduire cet arbre en un BDD en
fusionnant tous les sous-arbres identiques et en supprimant les états n'ayant
qu'un unique successeur. Dans notre exemple, on obtient alors le BDD de la
Figure \ref{fig:BDD_graph}.

\begin{figure}[h]
\begin{center}
\includegraphics[height=0.25\textheight]{BDD_graph.png}
\end{center}
\caption{BDD de la fonction \((x,y,z) \mapsto x \land y\).}
\label{fig:BDD_graph}
\end{figure}

Cependant, la taille du BDD est très dépendante de l'ordre choisi pour
les variables\cite{OBDD}. Dans cet exemple, l'ordre n'a pas une grande importance
mais lorsque le nombre de variables et la complexité de la fonction
augmentent, la taille du BDD peut exploser\footnote{Pour s'en
  convaincre, on peut calculer les BDD de la fonction
  \(x, y, z, t \mapsto x.z + y.t\), avec les ordres \(x<z<y<t\), puis
  \(x<y<z<t\).}.

À partir de la représentation sous forme de BDD, on peut évaluer la
fonction \(f\) efficacement, mais aussi réaliser des opérations logiques
performantes, en construisant le BDD résultant à partir des
feuilles et en réduisant au fur et à mesure. \cite{OBDD} explique cet
algorithme plus en détail . Dans le cas (simple) de la
négation, il suffit par exemple d'échanger les deux feuilles du BDD.

\paragraph{Vérification à l'aide des BDD}

On peut définir l'ensemble des états vérifiant une propriété \(\Phi\)
comme le point fixe d'une fonction (dépendant de \(\Phi\)). On calcule
alors ce point fixe de manière itérative, en utilisant les opérations définies
sur les BDD. Si l'état initial du système fait partie des états vérifiant la
propriété, le système est valide.

Par exemple, dans le cas d'une assertion, l'ensemble des états valides est
l'ensemble des états à partir desquels il n'est pas possible de déclencher
l'assertion. On peut le définir comme étant le point fixe de la fonction \(X
\mapsto E \cup X \cup Pre(X)\), avec \(X\) un ensemble d'états, \(E\) l'ensemble
des états d'erreurs et \(Pre\) la fonction qui associe à un ensemble d'états ses
prédécesseurs dans le modèle de système.

Tout comme les BDD, les autres représentations symboliques sont fortement
dépendantes d'un ordre des variables afin de conserver une taille
raisonnable. Les formules de la logique propositionnelle sont très
utilisées actuellement en raison des progrès des solveurs SAT.

Les techniques de model-checking symbolique sont efficaces afin de
prouver la validité d'une propriété (ce qui est le point faible du
model-checking de manière générale). Elles supportent bien l'explosion
combinatoire mais sont très dépendantes des performances des
représentations symboliques utilisées.

\subsubsection{Outils}

CIVL\cite{CIVL} est un framework pour la vérification de programmes concurrents.
Il définit un langage intermédiaire, CIVL-C, proche du C11, vers lequel plusieurs
langages et types de concurrence peuvent être traduits (dont pThread, OpenMP et
CUDA). CIVL utilise un mélange de model-checking explicite et symbolique : les
différents entrelacements d'un programme sont explorés de manière explicite et
une analyse symbolique est utilisée pour analyser chacun de ces entrelacements.
Les états sont représentés à travers des formules SMT, manipulées à l'aide de la
bibliothèque SARL\cite{SARL}. CIVL a pour ambition de constituer un point de
jonction commun entre plusieurs frontends et backends, afin de découpler les
problèmes de modélisation d'un langage et les problèmes de vérification. CIVL
adopte une approche conservatrice : il se veut correct mais il n'est pas
complet, il peut donc signaler des faux positifs.

SymDivine\cite{SymDivine} permet la vérification de propriétés \ac{LTL} sur du
bytecode LLVM concurrent (et donc, par extension, pour des programmes en C).
Tout comme CIVL, SymDivine utilise une combinaison de model-checking explicite
et symbolique. Le non-déterminisme au niveau des données est géré de manière
symbolique tandis que celui au niveau du contrôle est traité explicitement : tous
les entrelacements sont explorés individuellement. SymDivine peut utiliser les
formules SMT ou des BDD pour représenter les ensembles abstraits, les premières
étant plus efficaces dans la plupart de leurs expérimentations.

SymDivine et CIVL utilisent des méthodes de vérification semblables, mais
diffèrent par leurs langages de modélisation. CIVL utilise CIVL-C, un langage
relativement haut niveau pour faciliter la conception de modèles et la prise en
charge de plusieurs langages et paradigmes de concurrence. SymDivine
privilégie le bytecode LLVM, plus proche du programme compilé final afin de
réduire la distance entre le modèle et le système. CIVL a terminé troisième
(respectivement quatrième) lors des éditions 2016 (respectivement 2017) de
SV-COMP\cite{svcomp_2016_result, svcomp_2017_result}, dans la catégorie portant
sur la concurrence.

\subsection{Predicate abstraction}

L'abstraction par prédicat (\emph{predicate abstraction}) est une technique
proche de l'interprétation abstraite, dont nous avons parlé dans l'introduction
de ce mémoire. Elle consiste à construire un modèle du programme dans un
domaine abstrait, déterminé en partitionnant l'ensemble des états du système
selon un ensemble de prédicats. Le domaine abstrait utilisé par
l'interprétation abstraite est en général fixé par l'outil et
indépendant du programme analysé. Les techniques d'abstraction par prédicat
diffèrent sur ce point : elles construisent un modèle sur mesure pour le système
considéré et la propriété à vérifier\cite{abstract_state_graph, dsilva_survey_2008}.

L'objectif des techniques d'abstraction par prédicat est de construire une
abstraction du programme exacte par rapport à la propriété à vérifier. Cette
abstraction est réalisée en choisissant un certain nombre de prédicats portant
sur les états du programme. Le choix des prédicats est une étape cruciale,
puisque la précision de l'abstraction en dépend. Si l'abstraction n'est pas
suffisamment précise, des faux positifs ou des faux négatifs peuvent avoir lieu.

Une fois les prédicats choisis, les états de l'abstraction sont définis comme
les classes d'équivalence obtenues en partitionnant l'ensemble des états du
système par l'ensemble des prédicats. Une transition existe entre un état
abstrait \(A\) et un état abstrait \(B\) si une transition existe dans le
système d'origine entre un des états de \(A\) et un des états de \(B\).

On peut représenter le système abstrait comme un programme booléen, c'est-à-dire
un programme possédant les structures de contrôle classique du C, mais
uniquement des variables booléennes. Les variables de ce programme représentent
chacune un prédicat, et leur valeur dans un état du programme représente si
le prédicat est vérifié dans cet état ou non. On peut alors vérifier le système
abstrait à l'aide d'un model-checker pour programmes booléens (ceux-ci utilisent
fréquemment des méthodes de model-checking symbolique).

\paragraph{Exemple}

Considérons l'exemple du listing \ref{lst:bool_prog_init}. L'erreur qui a lieu
lorsque \texttt{x = 0} pourrait ici correspondre à une division par
zéro. Considérons les prédicats \(p_1 = (y == 1)\) et \(p_2 = (x == 0)\).

On détermine quatre états abstraits pour chaque position du programme,
correspondant aux différentes valeurs de \((p_1, p_2)\). On peut ensuite
déduire le programme booléen associé en supprimant les variables du programme
initial et en rajoutant des instructions pour actualiser les prédicats. On
obtient le programme booléen présenté dans le listing \ref{lst:bool_prog_bool}.

\noindent\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, caption=Code initial, frame=single, numbers=left,
    label=lst:bool_prog_init, xleftmargin=1.6em]
x = 3;
y = 2;
if (y == 1)
   x = 0;
if (x==0)
   assert(false);
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, caption=Programme booléen,frame=single, numbers=left,
    label=lst:bool_prog_bool]
p_2 = false;
p_1 = false;
if (p_1)
    p_2 = true;
if (p_2)
    assert(false);
\end{lstlisting}
\end{minipage}

Ce programme peut facilement être analysé par un model-checker pour programmes
booléens.

Il reste cependant à déterminer automatiquement les prédicats utilisés. La
méthode la plus connue pour construire choisir les prédicats et construire une
abstraction dans le cas du model-checking logiciel est la méthode
\ac{CEGAR}\cite{dsilva_survey_2008}.

\subsubsection{Counter-Example Guided Abstraction Refinement (CEGAR)}

La méthode \ac{CEGAR} permet de construire une abstraction en itérant quatre phases :
Abstraction, Vérification, Simulation et Raffinement. Une première abstraction
(peu précise) du programme est réalisée. Si la vérification fournit un
contre-exemple, celui-ci est simulé dans le système initial afin de vérifier
qu'il y existe (afin d'éviter un faux-positif). Si ce n'est pas le cas, on
utilise cette information pour
construire une abstraction plus précise qui permet de rejeter cette trace et on
itère le processus.

Reprenons le programme du listing \ref{lst:bool_prog_init} comme exemple.

\begin{enumerate}
\def\labelenumi{\arabic{enumi})}
\item
  \textbf{Abstraction :} Dans un premier temps, on considère une abstraction
  basée sur un ensemble de prédicats vide. Il n'y a donc qu'une seule classe
  d'équivalence, contenant tous les états du programme. On ne conserve que les
  structures de contrôle du programme. Une analyse statique du programme peut
  aussi être utilisée pour définir ce premier ensemble de prédicats.
  Toutes les variables sont rendues abstraites, et leurs valeurs dans
  les structures de contrôle sont non déterministes. On obtient alors
  l'abstraction présentée dans le listing \ref{lst:CEGAR_1}.
\item
  \textbf{Vérification :} Un model-checker pour programmes booléens permet de
  trouver la trace exécutant les lignes 1, 2, 3, 5, et 6 qui mène à une erreur
  dans l'abstraction.
\item
  \textbf{Simulation :} Une simulation symbolique permet de constater que la
  trace n'est pas réalisable. En effet, \texttt{x} est non-nul lors
  du test à la ligne 5 donc la transition de la ligne 5 à la ligne 6 n'est pas
  réalisable.
\item
  \textbf{Raffinement :} L'incohérence présente dans la trace est utilisée pour
  raffiner l'abstraction, de manière à éliminer les chemins invalides. Ici, un
  prédicat \texttt{{x = 0}} indiquant si \texttt{x} est nul est ajouté. On
  obtient alors l'abstraction plus précise du listing \ref{lst:CEGAR_2}.
\item
  \textbf{Vérification :} Le model-checker trouve cette fois l'exécution
  passant par les lignes 1, 2, 3, 4, 5 et 6.
\item
  \textbf{Simulation :} cette trace est encore une fois incorrecte, puisque
  \texttt{y} ne vaut pas \texttt{1} à la ligne 3.
\item
  \textbf{Raffinement :} un prédicat \texttt{{y = 1}} est ajouté. On obtient
  l'abstraction du listing \ref{lst:CEGAR_3}.
\item
  \textbf{Vérification :} Le model-checker ne trouve pas de trace menant à une
  erreur dans l'abstraction. L'absence d'erreur est donc prouvée pour le
  programme.
\end{enumerate}

\noindent\begin{minipage}{.45\textwidth}
  \begin{lstlisting}[language=C, label=lst:CEGAR_1, numbers=left, frame=single,
    caption=Abstraction initiale, xleftmargin=1.6em]
;
;
if (*)
    ;
if (*)
   assert(false);
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
  \begin{lstlisting}[language=C, label=lst:CEGAR_2, numbers=left, frame=single,
    caption=Premier raffinement, xleftmargin=1.6em]
{x = 0} = {false};
;
if (*)
    {x = 0} = true;
if ({x = 0})
   assert(false);
\end{lstlisting}
\end{minipage}

\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, label=lst:CEGAR_3, numbers=left, frame=single,
  caption=Second raffinement, xleftmargin=1.6em]
{x = 0} = false;
{y = 1} = false;
if ({y = 1})
    {x = 0} = true;
if ({x = 0})
   assert(false);
\end{lstlisting}
\end{minipage}

La phase de raffinement est critique pour les performances de la méthode
\ac{CEGAR}, puisque améliorer le choix des nouveaux prédicats peut éviter des
itérations supplémentaires de l'algorithme. Des techniques d'analyse statique
sont souvent utilisées pour trouver les prédicats les plus forts éliminant un
chemin impossible du modèle. On peut en particulier calculer les plus faibles
préconditions d'un chemin impossible --- c'est-à-dire la plus faible propriété
qui implique que ce chemin va être emprunté.

\subsubsection{Lazy Abstraction with Interpolant (IMPACT)}

Les méthodes d'abstraction par prédicat, dont l'algorithme \ac{CEGAR}, se basent sur
le calcul d'une ou plusieurs abstractions du modèle. Calculer cette abstraction,
et en particulier les successeurs de chaque état abstrait est une tâche
coûteuse.

L'algorithme IMPACT\cite{IMPACT} permet d'éviter le calcul des successeurs des
états abstraits. Au lieu de raffiner une abstraction de manière itérative,
IMPACT raffine son modèle au fur et à mesure de sa construction, seulement
lorsque nécessaire. Pour ce faire, il déroule la relation de transition d'un
programme. L'arbre ainsi obtenu est ensuite exploré. Lorsqu'un état d'erreur
est atteint, les états du chemin vers cette erreur sont annotés par des invariants
prouvant que le chemin est impossible dans le programme d'origine (si de tels
invariants n'existent pas, une erreur est reportée). Le cœur de l'algorithme
IMPACT consiste à utiliser ces invariants pour éviter d'explorer des branches
entières de l'arbre. Si deux nœuds \(A\) et \(B\) partagent la même location et
que l'invariant de \(B\) est plus fort que celui de \(A\) (l'invariant de \(B\)
implique l'invariant de \(A\)), alors il
est inutile d'explorer les fils de \(B\) : une erreur accessible à partir de
\(B\) est accessible à partir de \(A\) aussi.

\subsubsection{Gestion de la concurrence}

Les techniques d'abstraction par prédicat reposent sur le fait que le problème
d'accessibilité dans un programme booléen séquentiel est décidable. On peut donc
déterminer si une trace menant à une erreur existe dans le modèle abstrait.
Cependant, le problème d'accessibilité dans un programme booléen concurrent
n'est pas décidable. C'est une grande difficulté pour les méthodes
d'abstraction par prédicats, qui reposent sur la terminaison et la rapidité de
l'analyse du programme booléen. C'est plus vrai encore pour l'algorithme \ac{CEGAR},
qui effectue plusieurs vérifications successives de ce programme.

Deux alternatives existent pour intégrer la concurrence dans les techniques
d'abstraction par prédicat :

\begin{enumerate}
\def\labelenumi{\arabic{enumi})}
\item
  Considérer les entrelacements du programme lors de la vérification du
  programme booléen. Pour pallier le problème de terminaison, il est
  possible de construire une sur approximation du programme booléen.
  Cette approximation permet d'assurer la terminaison du programme
  booléen, mais elle peut générer des faux positifs. Il reste possible
  de détecter ces faux positifs dans la partie \emph{Simulation} de
  l'algorithme \ac{CEGAR}\cite{predicate_abstraction_over_approximation}.
  Une autre solution est de limiter la profondeur d'exploration et le
  nombre de changements de contexte. Cependant, cette approche rend
  nécessairement la vérification incomplète.
\item
  Utiliser un raisonnement de type
  \emph{rely-garantee}\cite{thread_modular_abstraction} : les
  threads sont examinés un par un, de manière indépendante, et une approximation
  de l'effet des autres threads est construite pour examiner les différentes
  traces possibles.
\end{enumerate}

\subsubsection{Outils}

Impara\cite{Impara} adapte l'algorithme \emph{IMPACT}\cite{IMPACT} et le combine
à des techniques de réduction d'ordre partiel afin de l'étendre à des programmes
multi thread. Il réduit ainsi l'explosion combinatoire présente dans l'algorithme
IMPACT : dérouler naïvement la relation de transition d'un modèle concurrent,
comme le fait une extension directe de l'algorithme IMPACT, revient à
énumérer un nombre exponentiel d'entrelacements.

La plupart des model-checkers utilisant la méthode \ac{CEGAR} basent leurs procédures
de décision sur des prouveurs limités à l'arithmétique linéaire sur des nombres
réels uniquement. Ils ne peuvent alors pas raisonner sur des tableaux de bits.
Satabs\cite{Satabs}\cite{clarkesatabs} implémente ses procédures de décision à
l'aide d'un solveur SAT. Il parvient ainsi à manipuler des tableaux de bits, et
à représenter des structures plus complexes du langage C. Il gagne en précision
sur l'arithmétique des pointeurs en particulier. Satabs est ainsi capable de
vérifier un certain nombre de propriétés built-in (validité des pointeurs,
erreurs arithmétiques, accès hors des bornes d'un tableau), en plus de
propriétés spécifiées par des assertions.

Threader\cite{Threader}\cite{Threader_theory} se base aussi sur la méthode
\ac{CEGAR}. Cependant, il utilise des techniques basées sur des raisonnements de type
\emph{Rely-guarantee} afin de rechercher une preuve modulaire du programme.
Threader gagne ainsi en performance lorsqu'une preuve modulaire existe, mais
il peut être plus lent qu'une méthode classique dans les autres cas.

SKINK\cite{SKINK} permet vérifier des propriétés exprimées par des assertions à
partir de la représentation intermédiaire de LLVM. SKINK se base sur une
approche de type CEGAR, mais il raffine itérativement une abstraction de
l'ensemble des traces d'exécution au lieu de travailler sur une abstraction des
états. Les interpolants renvoyés par les solveurs SAT sont utilisés pour
construire un automate qui vient restreindre le modèle. SKINK prends en charge
la concurrence en construisant le produit entre les automates représentant
chaque threads. Des méthodes d'ordre partiel sont utilisées pour limiter
l'explosion combinatoire.

CPAchecker\cite{CPAChecker} est un framework qui a pris la suite de l'outil
BLAST \cite{BLAST}. Il permet une analyse configurable travers des CPAs
(\emph{Configurable program analysis}). Un CPA définit un domaine abstrait
(BDD, analyse de valeurs, analyse d'intervalles\dots). CPAchecker est capable
de mener une analyse d'accessibilité sur une combinaison arbitraire de CPAs. La
concurrence est prise en charge à l'aide d'un CPA qui définit une exploration
explicite des entrelacements\cite{CPAChecker_multithread}. De manière similaire
à CIVL, CPAchecker vise à réduire les efforts de développement nécessaires pour
tester de nouvelles approches pour les méthodes basées sur l'abstraction par
prédicat. CPAchecker permet de construire une spécification sous la forme d'un
automate, à l'aide d'un formalisme similaire à celui utilisé par BLAST.

Les techniques d'abstraction par prédicat sont principalement tournées vers les
propriétés d'accessibilité spécifiées par des assertions. Parmi les outils
supportant le C multi thread, tous prennent en charge les assertions. Cependant, seul
Satabs est orienté vers la vérification de propriétés built-in et aucun ne
permet de vérifier des propriétés \ac{LTL}.

De manière générale, les techniques d'abstraction par prédicat sont très
efficaces dans le cas du model-checking de logiciels séquentiels, car elles
supportent bien l'explosion combinatoire liée aux données. Cependant, elles ont
plus de difficultés à traiter des structures de données complexes (tableaux et
allocations dans le tas). La vérification de programmes concurrents constitue
aussi une difficulté majeure.

\subsection{Model-checking borné}

Le model-checking borné, ou \ac{BMC}, est l'une des
techniques les plus utilisées dans l'industrie des semi-conducteurs. Elle a été
adaptée dans le cas du model-checking logiciel. Le model-checking borné se base
sur les avancées des solveurs SAT et SMT pour effectuer les tâches de
vérification.

Au lieu d'explorer entièrement un modèle, les algorithmes de model-checking
bornés explorent uniquement des préfixes finis des exécutions possibles du
modèle. Une profondeur maximale d'exploration \texttt{k} est fixée.
Les \texttt{k} premiers pas de chaque exécution du système sont alors
encodée dans une formule de la logique propositionnelle.
On construit ensuite la conjonction entre cette formule et la négation d'une
formule représentant la spécification du programme, et on transmet le résultat
à un solveur SAT ou SMT. Si la formule est satisfiable, il existe une
exécution valide ne respectant pas la spécification (puisqu’elle satisfait la
négation de la spécification). Une erreur est donc reportée, la valuation qui a
satisfait la formule représente le contre-exemple.

\paragraph{Forme SSA}
Afin d'encoder les exécutions d'un programme dans une
formule, on met tout d'abord ce programme dans la forme \ac{SSA}.
Elle consiste à transformer le programme de telle sorte que chaque
variable ne soit assignée qu'une seule fois. Pour ce faire, les variables sont
dupliquées, une nouvelle copie étant utilisée à chaque assignation. Les
structures de contrôle sont remplacées par des expressions conditionnelles une
fois que les différents branchements se rejoignent. Les fonctions sont inlinées
--- leur corps est inséré directement à l'emplacement de l'appel --- et les
boucles sont déroulées un nombre de fois limité par la profondeur d'exploration,
en une cascade de blocs \texttt{if}.

Le passage en forme \ac{SSA} est illustré par l'exemple présenté dans les
listings \ref{lst::ssa_init} et \ref{lst::ssa_end}.

\noindent\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, caption=Code initial, frame=tlrb, label=lst::ssa_init]
int a = 0, b = 1, c;
a = a + b;
if (a > 0)
    c = 2;
else
    c = 3;
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, caption=Forme SSA,frame=tlrb, label=lst::ssa_end]
int a_0 = 0;
int b_0 = 1;
int a_1 = a_0 + b_0;
int c_0 = 2;
int c_1 = 3;
int c_2 = a_1 > 0 ? c_0 : c_1;
\end{lstlisting}
\end{minipage}

\paragraph{Dépliage de la relation de transition}
Dans le cadre du \ac{BMC}, le programme est vu comme une relation de transition
\(R\). Étant donnés deux états \(s\) et \(q\) du programme, \(R(s, q)\) s'évalue
à vrai si et seulement s’il existe une transition dans le programme permettant
de passer de l'état \(s\) à l'état \(q\). On peut alors établir la formule
représentant les \(k\) premiers pas d'une exécution par :

\[
F = I(s_0) \land \bigwedge_{i\in \{1..k\}} R(s_{i-1}, s_i)
\]

Le solveur va tenter de résoudre la formule en trouvant une suite d'états
\(s_i\) qui la satisfait. Cette suite représente alors une exécution possible
dans le programme : \(I(s_0)\) impose que l'exécution commence dans un état
initial, et \(\bigwedge_{i\in \{1..k\}} R(s_{i-1}, s_i)\) impose que les
transitions entre deux états successifs de la trace soient valides.

Partant de la forme \ac{SSA}, la relation de transition se déplie facilement
en construisant la conjonction des instructions. Les variables de la forme \ac{SSA}
peuvent directement être considérées comme des variables logiques. La principale
difficulté consiste à établir une théorie pour représenter les
instructions, en particulier les utilisations dynamiques de la mémoire.

Dans notre exemple, la relation de transition se déplierait en :

\begin{multline}
  \underbrace{a_0 = 0 \land b_0 = 1}_\text{État initial} \land
  \underbrace{a_1 = a_0 + b_0}_\text{Instruction 1} \land
  \underbrace{c_0 = 2 \land c_1 = 3}_\text{Branches du tests} \\
  \land
  \underbrace{(a_1 > 0 \implies c_2 = c_0)
    \land (\lnot a_1 > 0 \implies c_2 = c1)
  }_\text{Fusion des branches}
\end{multline}


Afin de vérifier une propriété \(\Phi\) du programme, on construit la
conjonction entre la formule représentant les exécutions du système et la
négation de la propriété.

\[
F' = \lnot \Phi \land I(s_0) \land \bigwedge_{i\in \{1..k\}} R(s_{i-1}, s_i)
\]

Un modèle de cette formule représente donc les \(k\) premiers pas d'une
exécution valide, et qui ne respecte pas la propriété \(\Phi\). Il s'agit donc
d'une exécution contenant une erreur.

Le \ac{BMC} explore un système sur une profondeur bornée, il est donc nécessairement
incomplet. Il permet de trouver des erreurs, ou de prouver des propriétés
d'accessibilité, mais il ne peut prouver des propriétés de sûreté ou trouver des
erreurs à des propriétés de vivacité : une erreur ou l'évènement attendu
pourraient être présents à une profondeur plus importante que la profondeur
maximale d'exploration.

Lorsque le modèle contient un nombre d'états finis, il est possible de rendre le
\ac{BMC} complet : il suffit de fixer une profondeur maximale d'exploration
suffisamment grande pour que toutes les traces du programme n'affichent plus de
nouveaux comportements une fois cette profondeur atteinte. Cette profondeur est appelée le seuil de
complétion (\emph{completeness threshold}). Calculer la valeur exacte du seuil de
complétion est un problème difficile. On utilise donc des sur approximations.
Cependant, l'exploration d'un système jusqu'au seuil de complétion est souvent
trop coûteuse en temps et en mémoire pour être réalisable. Le \ac{BMC} est donc
souvent utilisé pour détecter des erreurs dans un système plutôt que pour
prouver leur absence, en effectuant plusieurs explorations avec une profondeur
maximale croissante.

\paragraph{Support du multi threading}

Plusieurs approches ont été développées pour prendre étendre le \ac{BMC} à des
logiciels multi thread\cite{ESBMC_multithread}.

Deux techniques sont principalement utilisées.
La première consiste à encoder tout les entrelacements possibles entre les threads
du programme dans la relation de transition, et donc dans la formule de la
logique propositionnelle fournie à un SAT-solveur ou un SMT-solveur. Cette
technique permet au solveur d'optimiser sa preuve en utilisant les similarités
entre différents entrelacements. Cependant, les formules générées peuvent être
extrêmement grandes et dépasser les capacités des solveurs.

La seconde approche se base sur l'exploration explicite des entrelacements du
programme : une formule est passée au solveur pour chaque entrelacement, le
procédé étant interrompu dès qu'une erreur est détectée. Les formules générées
sont ainsi plus petites et plus simples à résoudre pour les solveurs, cependant,
un nombre exponentiel d'appels au solveur peut être nécessaire, avec des
formules parfois très semblables.

Le nombre de changements de contexte autorisés dans une exécution est
généralement borné de manière indépendante par rapport à la profondeur
d'exploration. On évite ainsi d'explorer un nombre trop élevé d'entrelacements.
Cette seconde borne repose sur l'observation empirique : la plupart des erreurs
dues au parallélisme sont peu \emph{profondes}, elles peuvent être atteintes en
un nombre réduit de changements de contexte.

Le model-checking borné est la méthode la plus efficace pour trouver des
erreurs peu profondes. Elle supporte bien le multi threading. Cependant,
cette méthode est peu efficace pour prouver l'absence d'erreur et ne
peut généralement valider un programme que si sa profondeur est faible.
Elle est particulièrement sensible aux boucles dont le nombre
d'itérations n'est pas borné.

\subsubsection{Outils}

CBMC\cite{CBMC} est le premier model-checker logiciel à avoir utilisé le
model-checking borné. Il est orienté vers les applications embarquées, et permet
de vérifier un programme par rapport à différents modèles d'exécution. Il se
base sur des SAT-solveurs afin de vérifier les conditions de vérification qu'il
génère. CBMC remplace les opérateurs arithmétiques par la description de
circuits équivalents afin de construire une formule logique
(\emph{bit-flattening}). CBMC supporte les programmes multi thread en encodant
symboliquement les entrelacements dans la formule passée au model-checker. Comme
la majorité des model-checkers, CBMC supporte la consistance séquentielle (i.e.
un ordre total entre les instructions est considéré). Cependant, CBMC est aussi
capable de traiter des modèles mémoires faibles (i.e. un ordre partiel entre les
instructions est considéré). En effet, les multiprocesseurs modernes ne
respectent pas la consistance séquentielle : d'autres comportements peuvent
apparaître, liés à la propagation des valeurs à travers les niveaux de cache.

ESBMC\cite{ESBMC} a été conçu en se basant sur CBMC, dont il reprend le
frontend. ESBMC utilise un solveur SMT (SAT Modulo Theory) au lieu d'un solveur
SAT pour vérifier les formules générées et utilise des théories différentes de
celles utilisées par CBMC afin de créer ces formules. ESBMC supporte les
programmes multi thread en énumérant explicitement tous les entrelacements
possibles du programme, et en effectuant une exploration symbolique sur chacun
d'entre eux. ESBMC améliore le support des boucles par l'utilisation de preuves
par induction\cite{ESBMC_k_induction}. Les boucles sont déroulées sur un nombre
\(k\) d'itérations. Si cela ne suffit pas à trouver un contre-exemple, ESBMC va
tenter d'établir un invariant en montrant qu'il est maintenu tout au long de la
boucle par une preuve par induction.

SMACK\cite{SMACK} permet de traduire un programme en C vers le langage de
modélisation Boogie. Il utilise pour cela la représentation
intermédiaire LLVM-IR et implémente des simplifications du code source pour
réduire le modèle. Le modèle en Boogie est ensuite vérifié à l'aide d'un
model-checker utilisé en backend. Par défaut, Coral est utilisé. Il s'agit d'un
model-checker borné se basant sur des solveurs SMT pour les programmes en
Boogie, supportant la concurrence. Ceci permet à SMACK de tirer parti de
backends éprouvé et des performances des solveurs. SMACK reste cependant
modulaire, il peut ainsi utiliser d'autres algorithmes que du BMC pour le
backend. SMACK est capable de vérifier des spécifications sous forme d'assertions
uniquement.

\subsection{Séquentialisation}

Les techniques de model-checking logiciel pour des programmes séquentiels ont
largement progressé au niveau de leurs performances et de leur précision.
Cependant, les model-checkers restent bien plus limités dans le cas de
programmes concurrents. La séquentialisation réduit le problème de la
vérification d'un programme multi thread à celui de la vérification d'un
programme séquentiel pour tirer partit des performances des outils dans ce cas.

La séquentialisation consiste à traduire un programme concurrent en un programme
séquentiel non déterministe équivalent. Le non-déterminisme lié au contrôle (les
différents entrelacements) est remplacé par un non-déterminisme lié aux données,
ce qui permet de mieux le gérer. Les techniques de séquentialisation ne
s'appliquent donc qu'à un programme multi thread, il est nécessaire de les
combiner avec un outil de model-checking adapté au cas séquentiel pour réaliser
les tâches de vérification.

La séquentialisation permet d'attaquer deux problèmes simultanément : améliorer
la prise en charge de la concurrence en se ramenant au cas séquentiel, et
proposer une interface de gestion de la concurrence compatible avec plusieurs
model-checkers, sans que ceux-ci n'aient à modifier leurs algorithmes.

Nous allons énumérer les idées clefs des algorithmes de séquentialisation, tout
en les illustrant par l'exemple de la transformation réalisée par
Lazy-CSeq\cite{LazyCSeq}.

Partons d'un programme concurrent très simple (nous nous inspirons ici
de l'exemple présenté dans \cite{LazyCSeq}, auquel on peut se
référer pour plus de détails) :

\begin{lstlisting}[language=C, frame=single]
int y = 0;
void* T0(void *d) {
  int x;
  x = y;
  y = x + 1;
}
void* T1(void *d) {
  y = 3;
}
int main() {
  pthread_t t0, t1;
  pthread_create(t0, NULL, T0, NULL);
  pthread_create(t1, NULL, T1, NULL);
}
\end{lstlisting}

Les idées clefs de la séquentialisation sont les suivantes :

\begin{enumerate}
\def\labelenumi{\arabic{enumi})}
\item
  Remplacer les structures concurrentes par des structures séquentielles
  (un thread est remplacé par une fonction\dots)
\item
  Instrumenter le code afin de simuler les changements de contexte.
\item
  Ajouter un ordonnanceur non-déterministe. Il dirige l'exécution et
  permet de générer tous les entrelacements (généralement de type
  circulaire) du programme.
\item
  Recourir à un model-checker pour explorer le résultat.
\end{enumerate}

Dans notre exemple, le premier point consiste à changer la fonction
\texttt{main}, qui représente le thread principal, en une fonction
séparée \texttt{main\_thread}. Les autres threads sont déjà
représentés par une unique fonction, il n'est donc pas utile de les
modifier (si deux threads exécutaient la même fonction, il serait
nécessaire de la dupliquer). La seconde étape est réalisée en
introduisant un saut conditionnel avant chaque instruction du programme,
à travers la macro \texttt{J}. Cette macro permet d'interrompre et de
reprendre l'exécution d'une fonction à partir d'une instruction donnée,
en sautant les instructions qui précèdent ou suivent. La variable
\texttt{cs} contient à chaque instant le numéro du label
correspondant à la prochaine interruption, et le tableau \texttt{pc}
contient le numéro du label de la dernière instruction atteinte lors de
l'exécution précédente. Pour conserver les valeurs des variables locales
pendant les interruptions, ces dernières sont rendues statiques. Enfin,
la fonction \texttt{main} contient l'ordonnanceur. Il va simuler
\texttt{k} passes d'un ordonnancement de type round-robin, en
choisissant de manière non déterministe le nombre d'instructions à
exécuter dans chaque thread avant de changer de contexte.

On obtient alors le code séquentialisé du listing \ref{lst:code_seq}.
Des structures de contrôle supplémentaires permettent de représenter la
synchronisation des threads.

\begin{lstlisting}[language=C, label=lst:code_seq, frame=single,
  caption=Code séquentialisé, float=*]
int cs,ct,pc[T],size[T]={2,4,7};
#define J(A,B) if(pc[ct]>A||A>=cs) goto _##B;
int y=0;
void T0(void *arg) {
          static int x;
_0:J(0,1) x = y;
_1:J(1,2) y = x + 1;
_2: ;
}
void T1(void *arg) {
_3:J(3,4) y = 3;
_4: ;
}
int main_thread() {
          static pthread_t t0,t1;
_5:J(5,6) pthread_create(&t0,NULL,T0,0,1);
_6:J(6,7) pthread_create(&t1,NULL,T1,0,2);
_7: ;
}
int main() {
  int K = 10; // Check over 10 rounds
  int r;
  for(r=1; r<=K; r++) {
    cs=pc[0] + nondet_uint();
    assume(cs<=size[0]);
    main_thread();
    pc[0]=cs;
    cs=pc[1] + nondet_uint();
    assume(cs<=size[1]);
    T1();
    pc[1]=cs;
    cs=pc[2] + nondet_uint();
    assume(cs<=size[2]);
    T1();
    pc[2]=cs;
  }
}
\end{lstlisting}

La séquentialisation ne préserve pas nécessairement toutes les
propriétés du code, selon les transformations effectuées. Les propriétés
d'accessibilité sont généralement préservées, cependant la plupart des
approches déplient les boucles et bornent la profondeur d'exploration et
le nombre de changements de contexte possibles.

\subsubsection{Outils}

CSeq\cite{CSeq} suit le schéma de séquentialisation de Lal/Reps. Ce dernier
consiste à considérer \(K\) copies de la mémoire partagée, pour \(K\) phases
d'un ordonnancement \emph{round-robin}. La fonction représentant chaque thread
va mettre à jour la i\textsuperscript{ème} copie jusqu'au i\textsuperscript{ème}
changement de contexte, avant de la passer au thread suivant. Enfin, toutes les
exécutions incohérentes (lorsque l'état de la mémoire à la fin d'un cycle ne
correspond pas à l'état deviné au début du cycle suivant) sont supprimées. CSeq
utilise des model-checkers bornés pour mener la vérification. Il est compatible
avec CBMC, ESBMC et LLBMC.

Lazy-CSeq\cite{LazyCSeq} se base sur le framework mis en place par CSeq mais
prend une approche paresseuse (\emph{lazy}). Il ajoute des instructions de
contrôle aux fonctions représentant les threads, ce qui permet d'interrompre ou
de reprendre l'exécution d'une fonction chaque fois qu'un changement de contexte
peut avoir lieu. L'ordre d'exécution des instructions dans un entrelacement est
ainsi préservé, ce qui permet de réduire considérablement l'utilisation du
non-déterminisme. Lazy-CSeq est compatible avec CBMC, ESBMC et LLBMC.

Mu-CSeq\cite{MuCSeq} se base sur le concept de \emph{memory
unwinding} (déroulement de la mémoire, MU). Un MU consiste en une
séquence d'écriture dans la mémoire partagée du programme. Mu-CSeq
choisit un MU de manière non déterministe et le confronte à une
simulation du programme afin de vérifier si les écritures correspondent.
Si c'est le cas, une exécution valide a été détectée. Cette approche
permet d'éviter d'explorer des entrelacements équivalents, seul l'entrelacement
des écritures étant pris en compte. Mu-CSeq utilise CBMC comme backend.

Unbounded-Lazy-CSeq\cite{ULCSeq} se base sur l'algorithme utilisé
par Lazy-CSeq, mais permet de ne pas limiter le nombre de changements de
contexte. Il est aussi capable de traiter des programmes non bornés.
Pour cela, UL-CSeq conserve les boucles mais se base sur
CPAChecker\cite{CPAChecker} en backend et non sur des model-checkers bornés.

De manière générale, les outils de séquentialisation ont obtenu
d'excellentes performances ces dernières années. Lazy-CSeq a obtenu la
médaille d'or de la catégorie \emph{concurrence} lors des éditions 2014
et 2015 de la SVCOMP et une médaille d'argent pour les éditions 2016 et
2017, tandis que Mu-CSeq a obtenu la médaille d'or lors de l'édition
2016 et la médaille d'argent lors des éditions 2014 et 2015
\cite{svcomp_2016_result, svcomp_2015_result,
svcomp_2014_result, svcomp_2017_result}.

\subsection{Bilan}

Différents outils et techniques de model-checking ont été développés pour
tenter de résoudre le problème principal du model-checking : l'explosion
combinatoire. Ces techniques ont différents points forts et défauts, qui
dépendent des propriétés types à vérifier, de la structure du modèle (boucles,
non-déterminisme sur les données ou  le contrôle...) et du résultat attendu
(détection d'erreurs, preuve de correction...).

Afin de gagner en performances, les différents outils implémentent des
optimisations et des techniques de réduction qui provoquent en général une
certaine perte de précision. La plupart des outils restreignent ainsi le type de
propriétés et de spécification qu'ils supportent afin de gagner en performances.
La figure \ref{tab:prop_type_table}, en annexe, récapitule les types de
propriétés qu'il est possible de vérifier avec chaque outil (selon les articles
que nous avons passés en revue). On remarque en particulier que si la plupart
des outils supportent une spécification à l'aide d'assertions, le support pour
\ac{LTL} est bien plus réduit.

La gestion de la concurrence reste encore un problème ouvert.
Elle est actuellement prise en charge par différents mécanismes : les
différents entrelacements peuvent être intégrés directement dans le modèle, ils
peuvent aussi être énumérés explicitement. Une autre approche est de mener une
preuve modulaire, en examinant chaque thread individuellement et en simulant ses
interactions avec le reste du système. Enfin, les techniques de
séquentialisation permettent de ramener le non-déterminisme dû aux
entrelacements à du non-déterminisme dû aux données que les model-checkers
savent mieux traiter.

Par la suite, nous allons utiliser des model-checkers en tant que backend
afin de vérifier du code instrumenté. L'objectif sera alors de considérer le
model-checker comme une boîte noire, dont il est inutile de connaître le
fonctionnement interne. Connaître les techniques utilisées restera cependant
utile pour comprendre les résultats et les performances obtenus.