7-Theme1.tex

\chapter{LTL AVEC SUPPORT DES POSITIONS ET DES VARIABLES LOCALES}\label{sec:Theme1}

\section{Limitations des méthodes de spécification actuelles}

À travers la revue de littérature, nous avons dégagé deux principales
limitations concernant les méthodes de spécification utilisées pour
model-checking de programmes concurrents.

La première limitation concerne les assertions. Les assertions sont le mécanisme
de spécification le plus utilisé dans le cadre du model-checking logiciel.
Cependant, les propriétés que l'on peut spécifier par des assertions sont
limitées à un sous-ensemble des propriétés de sûretés --- une assertion spécifie
qu'une certaine condition doit être vraie à une certaine position du code. Dans
le cas de programmes concurrents, ce type de propriétés est souvent insuffisant.

En effet, l'entrelacement entre les instructions d'un programme concurrent est
généralement complexe. Il est donc fréquent de vouloir vérifier des propriétés
portant sur l'ordre d'apparition de certains évènements au cours d'une exécution
du programme. Les assertions ne sont pas adaptées pour spécifier ce type de
propriétés.

\paragraph{Exemple}
L'absence de conditions de concurrence dans un programme est une propriété
généralement désirable. Elle fait partie de l'ensemble plus vaste des propriétés
d'exclusion mutuelle : il s'agit de vérifier que deux instructions accédant à
une même variable partagée ne peuvent être exécutées simultanément. Les listings
\ref{lst:data-race_t1} et \ref{lst:data-race_t2} présentent un cas très simple
de data-race.

\noindent\begin{minipage}{.45\textwidth}
  \begin{lstlisting}[language=C, frame=single, caption=Thread 1,
    label=lst:data-race_t1]
int p = 0;
void* thread1(void* d) {
  ...
  p += 1;
  ...
}
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Thread 2,
    label=lst:data-race_t2]

void* thread2(void* d) {
  ...
  p += 1;
  ...
}
\end{lstlisting}
\end{minipage}

Si les instructions \texttt{p += 1} des deux threads ont lieu simultanément, la
valeur finale de \texttt{p} est indéterminée.

Spécifier l'absence de data-races dans ce programme à l'aide d'assertions n'est
pas immédiat : les assertions ne permettent pas d'exprimer la notion de
simultanéité. Il est nécessaire d'introduire des variables supplémentaires, et
donc de modifier le système. La spécification la plus simple que nous avons pu
produire est présentée dans les listings \ref{lst:data-race_assert1} et
\ref{lst:data-race_assert2}\footnote{On remarque que cette spécification permet
  d'atteindre une race-condition sans violer les assertions. Ce n'est pas un
problème ici, car s’il est possible d'atteindre une race-condition, alors au
moins un entrelacement viole les assertions, un model-checker signalera donc
correctement l'erreur.}.

\noindent\begin{minipage}{.45\textwidth}
  \begin{lstlisting}[language=C, frame=single, caption=Thread 1,
    label=lst:data-race_assert1]
int p = 0;
int flag = 0;
void* thread1(void* d) {
  ...
  assert(!flag);
  flag = 1;
  p += 1;
  flag = 0;
  ...
}
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Thread 2,
    label=lst:data-race_assert2]


void* thread2(void* d) {
  ...
  assert(!flag);
  flag = 1;
  p += 1;
  flag = 0;
  ...
}
\end{lstlisting}
\end{minipage}

Cet exemple souligne le fait que, dans un programme concurrent, on
s'intéresse fréquemment au lien entre plusieurs \emph{assertions} plutôt qu'au
déclenchement d'une assertion simple. On aimerait pouvoir formuler des
propriétés telles que ``si deux assertions sont violées simultanément, une
erreur est présente'' ou ``si une assertion est violée, puis une seconde
assertion est violée, une erreur est présente''.

La seconde limitation concerne les spécifications utilisant \ac{LTL}.
Les model-checkers logiciels supportant \ac{LTL} restreignent généralement les
propositions atomiques à des fonctions booléennes portant sur la valeur des
variables globales du programme.
Si toutes les variables globale ont la même valeur dans deux états distincts du
programmes (qui diffèrent par leur position dans le code et leurs variables
locales), alors toutes les formules \ac{LTL} vont s'évaluer de la même manière
dans ces deux états : il n'est pas possible de les distinguer dans la
spécification, ce qui limite le type de propriétés qu'il est possible de spécifier.

En particulier, ces restrictions rendent impossible d'exprimer une assertion par
une formule \ac{LTL}. Alors que les logiques temporelles permettent d'exprimer
facilement des relations d'ordre entre différents évènements, \ac{LTL} n'est donc
pas une solution aux limitations rencontrées par les assertions.

\paragraph{Exemple}
Reprenons l'exemple précédent. La propriété d'exclusion mutuelle que l'on veut
spécifier peut s'écrire \(G \lnot (p_1 \land p_2)\) où \(p_1\) (respectivement
\(p_2\)) est la proposition atomique indiquant si le thread 1 (respectivement le
thread 2) est dans sa zone critique. Mais on ne peut pas exprimer \(p_1\) et \(p_2\)
directement, sans mentionner des positions du programme. Encore une fois, il est
nécessaire d'introduire des variables supplémentaires et de modifier le système.
Les listings \ref{lst:data-race_ltl1} et \ref{lst:data-race_ltl2} présentent une
solution, associée avec la spécification \(G \lnot (flag1 == 1 \land flag_2 ==
1)\).

\noindent\begin{minipage}{.45\textwidth}
  \begin{lstlisting}[language=C, frame=single, caption=Thread 1,
    label=lst:data-race_ltl1]
int p = 0;
int flag1 = 0;
void* thread1(void* d) {
  ...
  assert(!flag);
  flag1 = 1;
  p += 1;
  flag1 = 0;
  ...
}
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Thread 2,
    label=lst:data-race_ltl2]

int flag2 = 0;
void* thread2(void* d) {
  ...
  assert(!flag);
  flag2 = 1;
  p += 1;
  flag2 = 0;
  ...
}
\end{lstlisting}
\end{minipage}

Les deux mécanismes de spécification les plus utilisés par le model-checking
logiciel sont donc limités, sans être complémentaires. Certaines propriétés sont
alors complexes à spécifier. En pratique, le cas des data-races présenté en
exemple est suffisamment pour être implémenté en tant que propriété built-in,
mais ce n'est pas le cas pour d'autres propriétés (d'exclusion mutuelle ou non).

Dans ce chapitre, nous allons présenter un nouveau formalisme de spécification
permettant de remédier à ce problème. Il se base sur une restriction de \ac{LTL}
plus souple que celle utilisée classiquement par les model-checkers logiciels.
Nous introduisons le concept de \emph{zones de validités} afin de permettre
l'utilisation de variables locales et de positions dans les propositions
atomiques. Nous produisons ainsi un formalisme de spécification qui englobe les
assertions et les propositions LTL (telles que classiquement utilisées par les
model-checkers logiciel), tout en permettant de surmonter les limitations
rencontrées par les utilisations classiques de LTL : l'utilisation des variables
locales et des positions du code source dans la spécification.

Nous allons tout d'abord présenter les différents obstacles à résoudre afin
d'atteindre cet objectif. Nous présenterons ensuite les solutions (parfois partielles)
que nous apportons à ces problèmes, ainsi que le formalisme de spécification que
nous avons établi. Enfin, nous justifierons nos choix et nous les comparerons
aux autres travaux connexes.

\section{Comment spécifier les propriétés d'un code ?}

Différents problèmes doivent être surmontés afin de permettre l'utilisation de
variables locales et de positions dans une spécification.
Limiter \ac{LTL} à des propositions atomiques portant sur les variables globales
a permis d'éviter ces problèmes, qui sont spécifiquement liés aux variables
locales et aux positions.

\subsection{Désignation des variables d'un programme}

Pour utiliser une variable dans la spécification d'un programme, il est
nécessaire de la désigner de manière unique.
Le language C n'autorise qu'une seule variable globale portant un nom
donné dans un fichier\footnote{Les mots clefs \texttt{extern} et
\texttt{static} permettent de déclarer plusieurs variables globales
portant le même nom dans un programme}. Une variable globale peut donc être
identifiée de manière unique par son nom dans la plupart des cas (en ajoutant le
nom du fichier où elle est déclarée si nécessaire). Ce n'est pas
aussi simple lorsqu'on considère des variables locales : deux variables
locales portant le même nom peuvent cohabiter sans faire référence au
même emplacement mémoire.

Deux variables locales distinctes (ne faisant pas référence à la même
adresse mémoire), mais ayant le même nom peuvent survenir dans diverses situations,
parmi lesquelles :

\begin{itemize}
\item
  une variable \texttt{foo} est définie dans plusieurs contextes
  distincts (des fonctions différentes, des blocs différents d'une même
  fonction\ldots{}). La connaissance du contexte de la définition permet
  de les distinguer.
\item
  une fonction \texttt{bar} contenant une variable \texttt{foo}
  est appelée plusieurs fois séquentiellement dans le programme. La
  variable \texttt{foo} dépend alors de l'appel à la fonction
  \texttt{bar}.
\item
  la variable \texttt{foo} est définie dans des threads distincts.
  Dans ce cas, les deux instances de la variable peuvent exister
  simultanément. L'instance dépend du thread dans lequel elle est
  définie.
\item
  la variable \texttt{foo} est définie dans une fonction récursive
  \texttt{bar}. Dans ce cas, une nouvelle instance de \texttt{foo}
  est définie à chaque appel récursif de \texttt{bar}.
\end{itemize}

On peut répartir ces cas en deux catégories :

\begin{itemize}
\item
  les deux variables sont lexicalement distinctes, elles sont issues de
  deux définitions distinctes dans le code source. Dans ce cas, on peut
  différencier les variables en ajoutant des informations
  supplémentaires à leurs noms, pour identifier les contextes de
  déclaration de manière unique (fichier, fonction, bloc\ldots{}).
\item
  les deux variables sont lexicalement identiques, mais elles sont
  redéfinies. Ce cas est plus complexe : les appels de fonctions et les
  créations de threads peuvent être dynamiques et dépendre de l'exécution.
  Ils sont donc difficiles à identifier de manière statique, et il en va
  de même pour les variables locales associées.
\end{itemize}

\subsection{Portée des propositions atomiques}

Dans une formule LTL, une proposition atomique est intrinsèquement globale :
pour tout état \(s\) du programme, il peut être nécessaire de déterminer si
\(s\) est un modèle de la proposition atomique. Cela est généralement déterminé
selon la valeur prise par une expression booléenne dans l'état \(s\).
L'expression est évaluée en utilisant la valeur des variables dans l'état \(s\).

Cependant, si cette expression dépend de variables locales, elle ne peut être
évaluée que si toutes ces variables locales existent dans l'état \(s\). Une
proposition atomique n'est donc correctement définie que dans le domaine où sont
définies les variables locales dont elle dépend.

Pour obtenir une définition correcte d'une proposition atomique dépendant de
variables locales, il est donc nécessaire de prolonger sa définition à
l'ensemble des états.

\subsection{Désignation des positions d'un programme}

Tout comme pour les variables, il est nécessaire de désigner de manière unique
une position du code pour l'utiliser dans une spécification.

Il faut donc concevoir un moyen de désigner une position dans le code qui soit
à la fois pratique pour l'utilisateur et robuste par rapport aux modifications du
code.
Il est aussi nécessaire de tenir compte de la précision recherchée. Sur ce
point, nous nous limiterons à désigner une instruction. En effet, si l'on veut
désigner une expression au sein d'une instruction, il est toujours possible de
la transformer en une instruction indépendante.

Plusieurs options peuvent être envisagées pour résoudre ce problème :

\begin{itemize}
\item
  indiquer la position à l'aide du numéro de la ligne et du nom du fichier ;
\item
  placer des marqueurs dans le code ;
\end{itemize}

La première méthode souffre d'un inconvénient majeur : la spécification doit
être corrigée dès qu'une ligne est ajoutée ou enlevée dans le code. Nous avons
donc retenu la seconde option. Elle impose cependant de rajouter une
instrumentation dans le code, ce que nous désirons minimiser.

Une fois la manière de désigner une position établie, il faut déterminer comment
l'utiliser dans la spécification. Nous dirons par la suite qu'un programme a
atteint une position dans le code lorsqu’un des pointeurs d'instruction du
programme pointe sur l'instruction désignée par la position.

Il est cependant nécessaire de définir comment et dans quelle mesure une
position peut intervenir dans une proposition atomique. Nous avons
considéré les options suivantes :

\begin{enumerate}
\def\labelenumi{\arabic{enumi})}
\item
  une proposition atomique désigne une position ou une condition sur les
  variables du programme, de manière exclusive. On fait le lien entre les
  positions et les valeurs des variables du programme à l'aide des opérateurs de
  la logique des prédicats. Si \texttt{pos1} et \texttt{pos2} désignent
  deux positions du programme, alors on spécifie que la variable \texttt{x}
  est non nulle entre \texttt{pos1} et \texttt{pos2} par \(G
  (\{\text{pos1}\}\implies \{x \neq 0\} U \{\text{pos1}\})\).
\item
  une proposition atomique est constituée d'une condition sur les variables du
  programme et d'une condition sur les positions. En reprenant l'exemple
  précédent, on écrirait alors \(G \lnot p\), avec \(p\) la proposition atomique
  qui est vérifiée par tous les états ayant une position entre \texttt{pos1}
  et \texttt{pos2} et où \texttt{x} est nulle.
\item
  les positions viennent contraindre les opérateurs temporels. On pourrait
  envisager une approche semblable à la logique MTL\cite{mtl_definition}, où les
  opérateurs temporels sont restreints à des intervalles de temps, mais en
  appliquant la restriction à des positions du programme. On écrirait alors
  \(G_{[pos1, pos2]} \lnot \{ x \neq 0 \}\).
\end{enumerate}

Nous avons décidé de ne pas explorer l'option 3. En effet, elle demande de
modifier le comportement standard des opérateurs LTL et nous avons préféré
limiter nos modifications aux propositions atomiques seulement.

\section{Syntaxe et sémantique de la spécification proposée}

\subsection{Syntaxe}

Nous allons tout d'abord présenter la grammaire de la spécification que
nous avons finalement retenue, avant de justifier nos choix.

Notre spécification est composée de deux parties. D'une part, une formule LTL
classique. D'autre part, la définition des propositions atomiques utilisées
par la formule LTL.

La définition d'une proposition atomique est composée des éléments suivants :

\begin{itemize}
\item
  \textbf{un nom} : il permet de référer facilement à la proposition atomique.
\item
  \textbf{une zone de validité} : elle délimite un bloc d'instructions dans
  le code (au sens du langage C). Une zone de validité est délimitée par deux
  labels (placés dans le code par l'ingénieur réalisant la spécification).
  L'entrée et la sortie d'une zone de validité doivent être dans le même
  contexte et tout pointeur d'exécution atteignant le label de début doit
  atteindre le label de fin avant de sortir du contexte (i.e. un branchement ne
  doit pas permettre de sortir d'une zone de validité en évitant l'instruction
  portant le label de fin).
\item
  \textbf{une fonction d'évaluation} : il s'agit d'une fonction booléenne pure,
  écrite en C. Cette fonction est utilisée pour déterminer si un état
  dans la zone de validité vérifie la proposition atomique ou non.
\item
\textbf{une liste de paramètres} : ils désignent les variables qui seront
  passées en argument de la fonction d'évaluation lorsque celle-ci est évaluée.
  Une variable locale est préfixée par le nom de la fonction dans laquelle elle
  est définie. Tous les paramètres doivent être définis dans la zone de validité
  de la proposition atomique.
\item
  \textbf{une valeur par défaut} : lorsque la proposition atomique n'est pas dans
  sa zone de validité, elle s'évalue à sa valeur par défaut. Cette valeur par
  défaut permet de prolonger la définition de la proposition atomique en dehors
  de sa zone de validité.
\end{itemize}

Le tableau \ref{tab:spe_gram} résume la grammaire de notre spécification.

\begin{table}[ht]
\centering
\caption{Grammaire des propositions atomiques}
\label{tab:spe_gram}
\begin{tabular}[]{@{}rcl@{}}
\hline
<atomic-proposition>  & ::= & <proposition-id> <evaluation-function> <parameters>\\
                      &     &  <default> <validity-area>\\
<proposition-id>      & ::= & \emph{name of the proposition}\\
<evaluation-function> & ::= & \emph{C pure boolean function}\\
<parameters>          & ::= & <parameter> <parameters> \textbar{} \emph{nil}\\
<parameter>           & ::= & <global-parameter> \textbar{} <local-parameter>\\
<global-parameter>    & ::= & \emph{variable name}\\
<local-parameter>     & ::= & \emph{function name} :: \emph{variable name}\\
<default>             & ::= & \emph{boolean}\\
<validity-area>       & ::= & <label> <label>\\
<label>               & ::= & \emph{name of a C label}\\
\hline
\end{tabular}
\end{table}

La spécification est alors constituée d'une formule LTL portant sur des
propositions atomiques définies selon cette grammaire.

\subsection{Sémantique}

Les opérateurs de la logique classique et de la logique temporelle
suivent la sémantique usuelle de la logique propositionnelle et de LTL.

Les propositions atomiques s'évaluent selon la valeur des pointeurs
d'instruction du programme. On considère qu'un état \(p\) est dans la zone de
validité d'une proposition atomique lorsque, dans l'état \(p\), un pointeur
d'instruction du programme pointe sur une instruction comprise entre le label de
début de la zone de validité de la proposition et le label de fin. Cela signifie
que, quelque soit l'exécution menant à l'état \(p\), le pointeur d'exécution a
déjà atteint l'instruction désignée par le label de début, mais pas encore celle
désignée par le label de fin. Pour que la spécification soit valide, il est
nécessaire que, quelque soit l'exécution, si un pointeur d'instruction désigne
l'instruction marquée par un label de début, alors il atteigne celle marquée par
le label de fin avant de sortir du contexte courant.

On évalue alors la proposition atomique en un état \(p\) par :

\begin{itemize}
\item
  si l'état \(p\) n'est pas dans la zone de validité de la proposition
  atomique, alors la proposition atomique s'évalue à sa valeur par
  défaut.
\item
  si l'état \(p\) est dans la zone de validité de la proposition
  atomique, alors elle s'évalue à la valeur renvoyée par l'évaluation de
  sa fonction d'évaluation, avec comme paramètres la liste de variables
  de la proposition atomique, dans l'ordre.
\end{itemize}

\subsection{Exemple}

Nous avons choisi par la suite de représenter cette spécification en
JSON (JavaScript Object Notation)\cite{json}. Ce format est
relativement verbeux, mais présente l'avantage d'être facile à parser
tout en étant lisible pour l'être humain. Établir une syntaxe plus
concise pourrait représenter un développement futur.

Étant donné le code suivant, constitué de deux threads s'exécutant
simultanément (pour des raisons de concision, la fonction
\texttt{main} a été omise), nous allons spécifier le fait que la
variable \texttt{a} du premier thread n'est jamais nulle en même temps que
la variable \texttt{a} du second thread.

\noindent\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Thread 1]
void* thread1(void* d) {
  int a
b_p1:
  a = 0;
  a = 1;
e_p1:
  pthread_exit(NULL);
}
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Thread 2]
void* thread2(void* d) {
  int a;
b_p2:
  a = 1;
  a = a - 1;
e_p2:
  pthread_exit(NULL);
}
\end{lstlisting}
\end{minipage}

Il est nécessaire de rajouter des fonctions d'évaluation pour les
propositions atomiques :

\noindent\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Proposition atomique p1]
int f_ev_1(int x) {
    return x == 0;
}
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Proposition atomique p2]
int f_ev_2(int x) {
    return x == 0;
}
\end{lstlisting}
\end{minipage}

On obtient alors la spécification présentée dans le listing
\ref{lst:specifiation}.

\begin{figure}[ht]
\begin{lstlisting}[frame=single, caption=Spécification, label=lst:specifiation]
{ "ltl": "G(! (p1 && p2))",
  "pa": [
    {"name": "p1",
      "default": false,
      "expr": "f_ev_p1",
      "span": ["b_p1", "e_p1"],
      "params": ["thread1::a"]
    },
    { "name": "p2",
      "default": false,
      "expr": "f_ev_p2",
      "span": ["b_p2", "e_p2"],
      "params": ["thread2::a"]
    }
  ]
}
\end{lstlisting}
\end{figure}

Dans cet exemple, le code ne respecte pas la spécification. L'exécution
\(t1: a = 0 \rightarrow t2: a = 1 \rightarrow t2: a = a - 1\) permet
d'obtenir un état qui ne satisfait pas la propriété.

\section{Motivation de nos choix}

Nous allons maintenant expliquer comment et dans quelle mesure ce formalisme
de spécification permet de surmonter les obstacles détaillés précédemment.

\subsection{Identification des variables}

Nous avons choisi d'identifier une variable globale par son nom et une
variable locale par le nom de la fonction dans laquelle elle est définie
et le nom de la variable. Cela n'apporte qu'une solution partielle au problème
de l'identification des variables.

\paragraph{Cas de deux variables lexicalement distinctes}
Notre solution permet de distinguer des variables lexicalement distinctes tant
qu'elles ne sont pas définies dans une même fonction. Nous avons jugé que ce cas
est suffisamment peu fréquent pour ne pas le traiter. Nous laissons donc le soin
à l'utilisateur de renommer les variables concernées.

\paragraph{Cas de plusieurs instances d'une variable lexicalement identique}
Nous ne proposons pas de solution dans ce cas de manière générale. Cependant,
il existe des solutions pour quelques cas particuliers.

L'un des cas où identifier une variable dépend d'une notion dynamique a lieu
lorsqu’une même fonction est utilisée pour créer plusieurs threads. En effet,
les threads peuvent être créés de manière dynamique, leur nombre et leur ordre
de création peuvent donc dépendre de l'exécution. Cependant, il est fréquent de
créer les threads d'un programme de manière statique, en créant toujours le même
nombre de threads dans le même ordre (dans la fonction \texttt{main} par
exemple). Dans ce cas, il est possible d'identifier un thread par un indice
correspondant à l'ordre de création des threads. On pourra alors identifier de
manière unique une variable dans un thread uniquement en rajoutant un préfixe à
son nom, qui prendra alors la forme
\texttt{{thread\_id}::{fonction}::{variable}}\footnote{\label{fn:notimplemented}
Cette fonctionnalité n'est pas implémentée dans l'outil présenté dans le
Chapitre~\ref{sec:Theme2}.}.

Un autre cas est lié à l'identification d'une variable locale à une fonction
appelée plusieurs fois dans un programme. Une instance de la variable est créée
à chaque appel. Si les appels à la fonction sont séquentiels (il
existe donc plusieurs instances de la variable dans le programme, mais une seule
existe à chaque instant), considérer que ces différentes instances correspondent
à la même variable dans la spécification est généralement le comportement
attendu.

Cependant, lors d'appels récursifs ou concurrents, plusieurs instances de la
variable existent simultanément : pour évaluer une proposition atomique, il
faut alors décider quelle instance doit être utilisée. Dans ce cas, nous ne
proposons pas de solution. Il est cependant possible de reprendre l'approche de
Divine\cite{Divine_LTL}, en l'adaptant à notre système de valeurs par
défaut\textsuperscript{\ref{fn:notimplemented}}. Nous présentons cette approche
plus en détail dans la section~\ref{sec:related_work}.

\subsection{Identification des positions dans le code}

Identifier une position dans le code sans y placer un marqueur n'est pas une
solution viable : elle est trop sensible aux modifications du code, d'autant
plus que lors de la vérification d'un programme, on s'attend à plusieurs
itérations avec des modifications mineures du code, afin de corriger les erreurs
détectées.

Nous avons donc utilisé des marqueurs. Nous avons choisi des labels, puisqu'ils
permettent de désigner une instruction du code. Des alternatives auraient été
d'utiliser des commentaires ou des macros afin de marquer les instructions. Nous
avons préféré les labels pour des raisons d'implémentation, les commentaires
n'étant pas conservés par de nombreuses bibliothèques de transformation de code,
mais aussi en raison de leur signification : un label a pour rôle de désigner
une instruction.

Cependant, la précision d'une position à l'aide d'un marqueur reste de, au
mieux une instruction. On ne peut donc pas désigner une
position plus précisément, au niveau d'une expression par exemple. Nous avons
considéré que ce cas est suffisamment peu fréquent pour qu'il soit possible de
l'ignorer. Il reste de plus possible de décomposer une instruction afin d'en
désigner ses parties.

Nous avons choisi de former des intervalles de positions, car ils représentent un
bon compromis entre une énumération explicite et des constructions plus
complexes (union ou intersections d'intervalles\ldots{}). Dans les cas où une
zone de validité plus complexe est nécessaire, il est possible de la simuler en
utilisant plusieurs propositions atomiques et les opérateurs de la logique
classique pour les combiner.

\subsection{Définition des propositions atomiques}

Afin de définir correctement les propositions atomiques dans tous les
états du programme, nous avons choisi d'utiliser des valeurs par défaut
combinées à des zones de validité.

L'intérêt des zones de validité est double. L'utilisateur peut spécifier
manuellement quand une proposition doit utiliser sa fonction d'évaluation. Cela
permet en particulier d'attendre que les variables soient correctement
initialisées. Les zones de validité permettent aussi d'utiliser des positions
du code dans la spécification, et de lier directement ces positions à une
proposition sur les valeurs des variables du programme. Il n'est donc pas
nécessaire d'utiliser deux propositions atomiques \texttt{b} et \texttt{e} pour
définir le début et la fin d'un intervalle de position, une troisième
proposition atomique \texttt{p} pour spécifier une propriété sur les valeurs des
variables et enfin, d'utiliser une formule telle que \(G (b \implies (p U e))\)
pour spécifier que \texttt{p} doit être valide entre \texttt{b} et \texttt{e}.
\(G p\) est suffisant, la zone de validité étant incluse dans la proposition
atomique \texttt{p}. On obtient ainsi une formule LTL plus simple.

Nous avons choisi d'utiliser une valeur par défaut que l'utilisateur peut fixer,
plutôt qu'imposer une valeur par défaut. Il serait aussi possible d'imposer la
valeur par défaut (à \emph{faux} par exemple), on pourrait alors
reproduire les propositions atomiques ayant \emph{vrai} comme valeur par
défaut en utilisant une double négation. Par exemple, pour une proposition
atomique \(p\) ayant \(vrai\) comme valeur par défaut et \(f\) comme fonction
d'évaluation, et pour la formule \(G p\), on pourrait utiliser de manière
équivalente la proposition atomique \(q\), avec \(faux\) comme valeur par défaut
et \(\lnot f\) comme fonction d'évaluation. La formule LTL serait alors \(G
\lnot q\).

Cependant, il nous a semblé plus pratique et confortable de permettre à
l'utilisateur de fixer cette valeur de manière cohérente avec
l'utilisation de la proposition atomique. Ainsi, dans le
cas d'une propriété de sûreté \(G p\), il est plus naturel de fixer la
valeur par défaut de \(p\) à \emph{vrai} plutôt que considérer une
double négation.

\section{Expressivité de la spécification proposée}

Notre spécification est une restriction de \ac{LTL} plus faible que celle utilisée
par la plupart des model-checkers logiciels. Exprimer une formule \ac{LTL} ne
portant que sur des variables globales est donc très simple. Il suffit de
désigner le programme complet comme zone de validité pour toutes les
propositions atomiques. Le reste de la spécification est inchangé.

On vérifie ainsi que notre formalisme de spécification englobe bien les formules
\ac{LTL} classiquement utilisées par les model-checkers.

Notre spécification permet aussi de spécifier l'équivalent d'une assertion. En
effet, une assertion signifie : ``si un pointeur d'instruction du
programme pointe sur l'assertion et que l'état ne vérifie pas la
condition exprimée, alors il y a une erreur''.

On peut donc représenter cela par une propriété de sûreté. On exprime
une assertion par la formule \(G p\), avec \(p\) une proposition
atomique telle que :

\begin{itemize}
\item
  sa zone de validité correspond à l'emplacement de l'assertion dans le
  programme ;
\item
  sa fonction d'évaluation est la condition utilisée dans l'assertion,
  elle s'évalue donc à la valeur de cette expression dans la zone de
  validité ;
\item
  sa valeur par défaut est \emph{vrai}e, elle s'évalue donc à \emph{vrai}
  hors de la zone de validité.
\end{itemize}

Notre formalisme de spécification englobe donc bien les spécifications à l'aide
d'assertions et les formules \ac{LTL} classiquement supportée, tout en tirant
parti des forces de ces deux formalismes.

\section{Travaux similaires}\label{sec:related_work}

Des travaux portant sur la prise en charge des variables locales ont été réalisés,
autour du model-checker Divine\cite{Divine_3_0}. Ils sont présentés dans
\cite{Divine_LTL}.

Divine met en place un ensemble de macros permettant de définir les propositions
atomiques utilisées dans une formule LTL. Deux macros, \texttt{ap(proposition)}
et \texttt{ap\_set(proposition, value)} permettent respectivement de modifier
directement la valeur d'une proposition atomique passée en argument. La macro \texttt{ap}
met la proposition atomique à \emph{vrai} uniquement pendant l'exécution de
la macro, tandis que \texttt{ap\_set} change la valeur d'une proposition
atomique de manière durable, jusqu'à une prochaine modification.

Divine permet aussi de lier une proposition à une fonction d'évaluation à l'aide
de deux autres macros, \texttt{ap\_global(proposition, fonction, N, arg1, \dots,
  argN)} et\\
\texttt{ap\_local(proposition, fonction, N, arg1, \dots, argN)}.

La macro \texttt{ap\_global} doit être appelée dans l'espace global. Elle permet
de lier une proposition atomique à une fonction booléenne dont tous les
paramètres sont des variables globales.

La macro \texttt{ap\_local} lie une proposition atomique à une fonction dont
certains des paramètres peuvent être locaux. Les paramètres sont identifiés
dans le contexte d'appel selon la norme du C, et peuvent ensuite être masqués.
Le lien entre la fonction et la proposition atomique dure jusqu'à la sortie du
contexte (où les paramètres locaux sont détruits). Ensuite, la proposition
atomique prend la valeur par défaut \emph{faux}.

\paragraph{Exemple}
Reprenons l'exemple d'une data-race (Listing \ref{lst:data-race_t1}). Les
listings~\ref{lst:data-race_divine1} et \ref{lst:data-race_divine2} présentent
la spécification de l'absence de data-race dans le formalisme de Divine. La
formule \ac{LTL} correspondante est \(G(\lnot (P1 \land P2)))\).

\noindent\begin{minipage}{.45\textwidth}
  \begin{lstlisting}[language=C, frame=single, caption=Thread 1,
    label=lst:data-race_divine1]
void* thread1(void* d) {
  ...
  ap_set(P1, 1);
  p += 1;
  ap_set(P1, 0);
  ...
}
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[language=C, frame=single, caption=Thread 2,
    label=lst:data-race_divine2]
void* thread2(void* d) {
  ...
  ap_set(P2, 1);
  p += 1;
  ap_set(P2, 0);
  ...
}
\end{lstlisting}
\end{minipage}

\paragraph{Exemple}
Nous allons illustrer l'utilisation de \texttt{ap\_local} en spécifiant un
programme pour éviter une division par zéro. On considère pour cela la formule
\ac{LTL} \(G P\), avec \(P\) la proposition atomique indiquant que la variable
locale \(p\), dans le listing~\ref{lst:zdiv_divine} est non nulle. \(P\) est
définie à l'aide de la macro \texttt{ap\_local}.

\begin{figure}
\noindent\begin{minipage}[t]{.45\textwidth}
  \begin{lstlisting}[language=C, frame=single, caption=\texttt{ap\_local},
    label=lst:zdiv_divine]
int non_nul(int p) {
  return p != 0;
}
void* thread1(void* d) {
  int p;
  ap_local(P, non_nul, p);
  ...
  c = 1/p;
  ...
}
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}[t]{.45\textwidth}
\begin{lstlisting}[frame=single, language=C, caption=Fonction récursive,
  label=lst:divine-rec]
int p(int a) {
  return a == 8;
}
int count(int a) {
  ap_local(P, p, a);
  if (a < 10)
    return count(a + 1);
  return a;
}
int main() {
    count(6);
    return 0;
}
\end{lstlisting}
\end{minipage}
\end{figure}

L'usage de macro permet à Divine de mettre en place une spécification concise et
intuitive. La désignation des paramètres à passer aux fonctions d'évaluation, en
particulier, est à la fois moins verbeuse et plus précise --- elle permet de
designer une variable dont le nom est réutilisé dans la même fonction.

Divine est aussi confronté au problème posé par de multiples instances d'une
variable lexicalement identique. Divine choisi d'évaluer une proposition
atomique à vrai dès qu'il existe un contexte dans lequel elle s'évalue à vrai.
On considère donc la disjonction des valeurs prise par la proposition dans
l'ensemble des contextes actifs. Cette solution est justifiée par le fait qu'on
est généralement intéressé par l'instant où une proposition atomique ne prend
pas sa valeur par défaut (imposée à \emph{faux} par Divine).

\paragraph{Exemple}
Le code du listing~\ref{lst:divine-rec} présente une fonction récursive. Une
nouvelle instance de la variable \texttt{a} est donc déclarée à chaque appel
récursif, et les différentes instances existent simultanément.

Supposons que l'on veuille vérifier que la variable \texttt{a} ne vaut jamais 8
dans la fonction \texttt{count}. On cherche donc a vérifier formule \(G \lnot
P\). \(P\) est définie de sorte à être vrai si et seulement si \texttt{a} vaut
8. En déroulant les trois premiers appels, on obtient trois contextes, où
\texttt{a} vaut respectivement 6, 7 et 8. Pour \(a = 6\) et \(a = 7\), \(P\)
s'évalue à \(faux\). Pour \(a = 8\), \(P\) s'évalue à \(vrai\). On retient donc
cette valeur pour la proposition atomique. La formule est alors invalide, ce qui
permet de trouver une erreur.

Cette solution peut être adaptée dans le cas de notre formalisme de
spécification, en prenant la conjonction des valeurs si la valeur par défaut est
\emph{faux}, et la conjonction sinon.

Cependant, Divine ne propose pas l'équivalent d'un intervalle de validité.
Limiter la vérification d'une propriété à un intervalle de ligne dans le code
demande donc de définir des propositions atomiques supplémentaires, dont la
valeur est gérée par \texttt{ap} et \texttt{ap\_set}, et d'utiliser les
opérateurs \ac{LTL}. Cette approche produit des formules plus complexes, et donc
plus difficiles à vérifier.