LTL appliquée au mapreduce

Hadoop

Le second environnement MapReduce que nous allons décrire est Hadoop5, un environnement Java libre qui a été créé par la Apache Foundation dans le but de simplifier la création d’applications distribuées et scalables. Ce dernier permet donc de traiter un grand ensemble de données en utilisant la logique du parallélisme. L’environnement permet d’utiliser des milliers de noeuds et des pétaoctets de données. Ces dernières sont sauvegardées dans des fichiers dans une partition de type HDFS (Hadoop Distributed FileSystem). C’est un système de fichier qui est portable, extensible et qui a été inspiré par le GoogleFS. Le HDFS est écrit en Java et son but ultime est de sauvegarder de très gros volumes de données sur un grand nombre de machines avec des disques durs banalisés. Le système de fichier permet l’abstraction de l’architecture physique de stockage. Cela permet donc de manipuler les données comme il s’agissait d’un seul et unique périphérique de stockage. Il est important de savoir qu’il existe une autre façon de stocker les données dans l’environnement Hadoop. L’application HBase permet de créer une base de données distribuée à travers les noeuds de stockage. Cette dernière est orientée sur le principe de colonnes, c’est-à-dire que l’ensemble des données d’une colonne est stocké sur le même noeud.
L’environnement permet de travailler avec un cluster de noeud de deux types, soit les noeuds maîtres (master) et travailleurs (worker). Les noeuds maîtres ont pour tâche de s’occuper de gérer le stockage des données et de coordonner l’exécution des différentes instances de mapper et de reducer. Ce sont eux qui savent où se situent les blocs de données à travers des périphériques de stockage. De plus, ce sont eux qui s’occupent de l’exécution de la tâche à travers le cluster. À tout moment, un seul des noeuds maîtres est responsable de l’exécution des tâches. Si jamais celui-ci rencontre un problème, le noeud maître de secours reprend l’exécution de la tâche à l’endroit où l’ancien noeud maître était rendu. Ceci est possible puisqu’il existe un mécanisme permettant de savoir en tout temps où est rendue l’exécution du noeud maître principal pour tous les noeuds de secours. Les noeuds maîtres exécutent le traitement sous le format d’une tâche sous le principe MapReduce. Les noeuds travailleurs eux permettent de stocker les données et effectue le traitement voulu sur ces dernières. Par la suite, quand ils ont terminé leurs tâches, ils attendent le traitement suivant déterminé par le noeud maître.

Sans oublier, qu’il est important de noter que dans l’environnement Hadoop

MapReduce, ils nous étaient impossibles d’effectuer un enchaînement de phase Mapper et Reducer dans une même tâche. Donc, pour émuler le multi-générations dans Hadoop, nous avons dû créer un code dynamique permettant de lancer plusieurs tâches une à la suite de l’autre. De plus, cela implique que nous devons avoir une phase d’InputReader et d’OutputWriter pour chaque tâche, ce qui signifie une perte de temps à chaque génération.

WordCount de mode Hadoop

À titre d’exemple, voici comment le code de l’exemple « word count », décrit précédemment dans le chapitre, ce traduit en code Java utilisant l’environnement Hadoop MapReduce.

Mr Sim VS Hadoop

Nous pouvons remarquer qu’il y a quelques éléments qui diffèrent entre les différents outils qui permettent de travailler avec le paradigme MapReduce. Toutefois, nous allons effectuer une comparaison entre Mr Sim et Hadoop pour les points suivants :
 Mr Sim est un outil mono-thread, c’est-à-dire que l’exécution totale de la tâche se fait dans un thread. Donc cela implique alors que l’exécution de la tâche, ainsi que les phases MapReduce, se font une à la suite de l’autre et ce dans l’ordre nécessaire au bon fonctionnement de la tâche. On peut également en conclure que Mr Sim est mono-machine et séquentiel. De plus, un autre fait qui appuie cet énoncé est que Mr Sim est déployable sur une machine, puisqu’il utilise l’outil de développement Java local de la machine. Si on effectue la comparaison directement avec Hadoop,
on peut s’apercevoir qu’ils sont totalement différents. La raison est que Hadoop permet l’utilisation d’un environnement distribué. C’est-à-dire de pouvoir utiliser plusieurs unités de traitement qui sont déployées dans un regroupement de machines, c’est-à-dire un cluster, pour exécuter la tâche. De plus, rien n’empêche d’utiliser plusieurs threads par machine pour effectuer un traitement spécifique en parallèle.
 Maintenant au niveau du stockage des données, Mr Sim est totalement dépendant du système de fichier de la machine hôte. De plus, c’est ce dernier qui s’occupe de stocker et de rendre accessible le fichier dans lequel les données sont contenues. Mr Sim ne fait que lire les informations ou en écrire. Ce fait est totalement faux pour Hadoop, car ce dernier utilise son propre système de fichier, soit le HDFS. De plus, la gestion des fichiers est laissée au noeud maître et c’est ce dernier qui s’occupe de savoir où se trouvent les données dans l’ensemble des partitions HDFS que contient son cluster.
 Mr Sim permet d’utiliser l’héritage lors du transfert de données entre les différentes phases. Pour lui, une instance d’une classe K’ qui hérite de K est compatible avec le Mapper ou Reducer pour l’objet K. Ce qui n’est pas le cas dans l’environnement Hadoop. Pour ce dernier, une instance d’une classe K’ n’est pas strictement égale à K, donc le Mapper ou Reducer associé à K est invalide pour cette instance. Donc, pour palier au problème, si l’utilisation de plus d’un type d’objet est nécessaire dans les différentes phases, il faut utiliser un objet conteneur qui permet de représenter tous les instances qui héritent de K.
 Le principe d’avoir une tâche multi-générations est possible dans Mr Sim, il suffit de chaîner les Mappers de la génération X aux Reducers de la génération X-1.
Toutefois, les derniers Reducers sont liés au OutputWriter pour pouvoir interpréter les résultats du traitement de la tâche. Dans un environnement Hadoop, il est impossible d’effectuer un tel enchaînement. Il faut en tout temps avoir la séquence normale, soit l’InputReader, Mapper, Reducer et OutputWriter, pour effectuer le traitement d’une tâche. Donc, le traitement multi-générations est émulé par le processus principal de la tâche. Celui-ci doit déterminer s’il est nécessaire de lancer une prochaine génération, donner comme fichier d’entrée de la prochaine génération le fichier sortant de la dernière génération et lancer la tâche. C’est également le processus principal qui doit déterminer quand faire interagir le bon InputReader ou OutputWriter, s’il en existe plus d’une version.
En somme, nous avons décrit les différences majeures entre les deux environnements MapReduce. De plus, c’est sans compter les différences de déclarations des environnements pour créer un objet pour pouvoir lancer la tâche, ainsi que les différences au niveau des ressources disponibles des environnements.

LTL APPLIQUÉE AU MAPREDUCE

Comme nous avons pu le voir dans la section précédente, il est possible d’utiliser le parallélisme pour décomposer un problème pour qu’il puisse être résolu dans un environnement au moyen du paradigme MapReduce. Toutefois, le problème que nous voulons étudier, soit l’analyse de traces avec la LTL, est resté sans solution jusqu’à tout récemment. En 2009, les chercheurs Kuhtz et Finkbeiner ont démontré que la validation de formules LTL sur des traces appartient à la classe de complexité AC1 (logDCFL) [3]. Leur résultat permet alors d’en déduire que le processus peut être divisé de façon efficace par l’évaluation des blocs entiers d’événements en parallèle. Leur façon de travailler est différente et est accessible au parallélisme, puisque leur technique dépend de la longueur de la trace. De plus, il est important de savoir que leur méthode ne traverse pas les événements de la trace les uns à la suite des autres. Toutefois, lors de l’évaluation du déroulement, ce dernier ne peut être effectué en parallèle. Il faut tout d’abord créer à l’avance un certain type de circuit booléen. Cependant, ce dernier dépend de la longueur de la trace à évaluer. En outre, la démonstration formelle du résultat montre qu’un nombre déterminé de portes de ce circuit peuvent être sollicités en parallèle à chaque étape du processus, cependant l’algorithme lui-même nécessite un accès global et partagé à la trace entière pour chacun des processus parallèles. Malheureusement, cette idée ne se prête pas directement à un environnement de traitement distribué et parallèle.
Nous allons mettre cette approche de côté et nous allons en étudier une autre. Dans cette section, nous présentons un algorithme qui effectue la validation d’une formule LTL sur une trace en utilisant le principe de MapReduce. L’algorithme effectue le travail d’analyse en itérant la formule LTL sur les données. Lors de la première itération, tous les états qui satisfont les variables propositionnelles, contenu dans la formule à vérifier, sont identifiés. Dans l’itération suivante, les résultats déterminés précédemment sont utilisés pour évaluer toutes les sous-formules qui utilisent directement une de ces variables.
Autrement dit, à la fin de l’itération i du processus, les événements où toutes les sousformules de profondeur i respectent la propriété sont connus. Il s’ensuit que, pour évaluer une formule LTL de profondeur n, l’algorithme aura besoin d’exactement de n cycles MapReduce. Chaque cycle MapReduce agit dans les faits comme une forme de testeur temporel [17] en testant une trace constituée d’évaluations de testeurs de niveau inférieur.
Cependant, cela ne signifie pas que la trace doit être lue autant de fois. Dans les faits, la trace de départ est lue uniquement une fois dans son entièreté, lors de la première itération de la procédure. Par la suite, c’est seulement le numéro de référence séquentiel à chaque événements qui doit être transféré entre les mappers et les reducers. Le contenu de la trace originale ne sera plus jamais consulté lors des traitements.
Le système est décrit en fournissant les détails de chacun des composants du principe de MapReduce décrite dans la Figure 1. Nous supposons que chacune des instances du principe (InputReader, Mapper, Reducer et OutputWriter) sont paramétrées par la formule à vérifier et la longueur de la trace ℓ.

Format de la trace et l’InputReader

La phase de l’InputReader est responsable de traiter les parties de la trace et la génération du premier ensemble de tuples clé-valeurs à partir de ces derniers. Nous assumons que chacun des événements est séquentiellement numéroté ou que sa position à l’intérieur de la trace peut être facilement déterminée. Pour un événement e, nous allons y référer en utilisant son numéro séquentiel noté #(e). L’algorithme de la phase InputReader, qui est représenté dans la figure 7a, parcourt chaque événement de la partie de la trace qui lui est confiée et évalue sur chaque événement chacune des variables propositionnelles présentes dans φ, la formule LTL à évaluer. Pour chaque variable propositionnelle a et chaque événement e pour lequel cette variable s’évalue à vrai, l’algorithme émet un tuple <a, (i,0)> ou la variable i représente le numéro séquentiel de l’événement au sein de la trace. On note par atom(φ) l’ensemble de toutes les variables propositionnelles présentes dans φ.
Il est important de remarquer que le traitement initial ne nécessite pas que la trace se situe sur un seul et unique noeud. Chaque noeud contient un fragment de la trace et les événements de ce dernier ne sont pas nécessairement successifs. Il suffit que chacun des événements puisse être remis à sa place séquentielle au sein de l’ensemble de la trace; le nombre de noeuds hôtes qui contient un sous-ensemble de la trace peut être variable. Ceci est particulièrement utile si l’ensemble des événements et leur stockage est fait de façon distribuée.

Mapper

La phase Mapper a comme format d’entrée des tuples qui ont la forme < ψ,(n,i)>, ces derniers ont pour source la phase InputReader décrite ci-dessus, ou alors les résultats d’un cycle MapReduce précédent. Chacun de ses tuples se lit comme suit : « le processus est à l’itération i et la sous-formule ψ est vraie pour l’événement n ». On peut voir, en particulier, la façon dont les tuples retournés par l’InputReader expriment ce fait pour les termes de base de la formule à vérifier.
Le pseudo-code du Mapper, que l’on retrouve dans la figure 7b, est responsable de transformer les résultats obtenus pour certaines formules ψ, afin d’obtenir ceux d’une formule ψ’ dont ψ est une sous-formule directe (celles-ci sont obtenues en utilisant la fonction superformulæ (φ, ψ)). Par exemple, si les événements où p est vraie sont connus, alors ces résultats peuvent être utilisés pour déterminer les événements où F p est vraie. À cette fin, les Mappers prennent chacun des tuple <ψ,(n,i)> et émettront en sortie un tuple de la forme <ψ’,(ψ,n,i+1)>, où ψ est une sous-formule de ψ’. Ce dernier se lit comme suit : « le processus est à l’itération i + 1, la sous-formule ψ est vrai dans l’événement n et ce résultat est nécessaire pour évaluer ψ’ ».

Reducer

Les mappers sont surtout utilisés pour préparer les résultats de la dernière itération pour être utilisés pour l’itération en cours. En revanche, chaque instance de reducer effectue l’évaluation réelle d’une couche de plus de la formule temporelle linéaire à vérifier. Après l’étape de shuffling, chaque instance individuelle de reducer reçoit tous les tuples de la forme <ψ’,( ψ,n,i)> pour une formule ψ’, où ψ est une sous-formule directe de ψ’. Par conséquent, le reducer donne toutes les informations sur chacun des numéros d’événements qui respectent ψ’ et est en charge de traiter les états où ψ est respecté selon ses informations. Cette tâche peut être décomposée en fonction de l’opérateur principal de ψ’.
L’algorithme pour chaque reducer est représenté à la figure 8.
Lorsque la formule de haut niveau à évaluer est X ψ, les événements qui satisfont la formule sont ceux qui précèdent immédiatement un événement qui respecte ψ. Donc, le reducer parcourt l’ensemble des tuples d’entrée <X ψ, (ψ,n,i)> et produit pour chacun un tuple de sortie <X ψ, (n-1,i)>.
Lorsque la formule de haut niveau à évaluer est F ψ, les événements qui satisfont la formule sont ceux qui dans le futur respecteront ψ. Le reducer correspondant est celui qui parcourt les tuples d’entrée et calcule le plus grand numéro d’événement c pour lequel ψ est respecté. Tous les événements précédents c respectent F ψ. Conséquemment, le format que le reducer génère comme tuple de sortie est <F ψ,(k,i)>, pour tout k ϵ [0,c].
Le reducer pour ¬ ψ parcourt tous les tuples et garde dans un tableau booléen si ei |= ψ pour chaque événement i de la trace. Par la suite, il émet un tuple <¬ψ, (k,i)>, pour tous les numéros d’événement k qui n’ont pas été vu dans les tuples d’entrée. Le reducer pour G ψ effectue le traitement dans le sens inverse. Premièrement, il parcourt tous les tuples de la même façon. Si nous définissons c comme l’indice du dernier événement pour lequel ψ n’est pas respecté, le reducer émettra des tuples de sortie de format <Gψ,(k,i)>, pour k ϵ [ c+1, ℓ ]. Cela correspond alors à tous les événements pour lesquels G ψ est respecté.
Le traitement des opérateurs binaires ∨ et ∧ est un peu plus délicat. Des soins particuliers doivent leurs êtres apportés pour maintenir les tuples dont les résultats seront utilisés dans la dernière itération. Prenons le cas de la formule (F p) ∧ q. Les états où les termes clos (feuilles) p et q sont respectés seront traités par l’InputReader à l’itération 0.
Cependant, bien que q soit une sous-formule directe de (F p) ∧ q, il faut attendre jusqu’à l’itération 2 pour pouvoir la combiner à F p, évaluée à l’itération 1. Plus précisément, un tuple <ψ * ψ’, (ψ, n,i)> peut être évaluée uniquement à l’itération δ(ψ * ψ’) ; dans tous les itérations précédentes, les tuples <ψ,(n,i)> doivent être remis en circulation. La première condition de l’algorithme des deux reducers prend soin de cette situation. Il est important de savoir que la fonction delta δ, permet de calculer la profondeur de la propriété demandée. Exemple : La formule δ(G((¬{p0/0}) ∨ (X{p1/0}))) est de profondeur 4.
Dans le cas contraire, lorsque la formule de niveau supérieur à évaluer est ψ ∨ ψ’, le format des tuples de sortie est < ψ ∨ ψ’, (n,i)> chaque fois que le reducer lit des tuples d’entrée < ψ ∨ ψ’, (ψ ,n,i)> ou < ψ ∨ ψ’, (ψ’ ,n,i)>. Lorsque la formule de niveau supérieure est ψ ∧ ψ’, le reducer doit mémoriser les numéros d’événements n pour les tuples lus et tels que < ψ ∧ ψ’, ( ψ ,n,i)> et < ψ ∧ ψ’, (ψ’ ,n,i)>, et émettra des tuples de format < ψ ∧ ψ’, (n,i)> dès qu’il aura vu les deux.
Le dernier cas à considérer est une formule de forme ψ U ψ’. Le premier reducer parcourt parmi tous ses tuples d’entrées et mémorise le numéro de l’événement qui respecte ψ et ceux pour lesquels ψ’ est respecté. Il procède ensuite à rebours à partir du dernier événement de la trace et émet < ψ U ψ’, (n,i)> pour un certain état n si ψ’ respecte n ou si ψ respecte n et qu’il existe une suite ininterrompue d’états conduisant à un état pour lequel ψ’ est respecté. Cette dernière information est traitée via la variable booléenne b.
Comme on peut le voir, les tuples produits par chaque reducer ont la forme < ψ, (n,i)>, permettant de porter la même signification que ceux originalement produits par le InputReader, mais pour des formules de plus grande profondeur. Toutefois, le résultat d’un cycle MapReduce peut être réinjecté en entrée pour un nouveau cycle. Comme nous l’avons vue, cela prend exactement δ(φ) cycles complets pour évaluer une formule LTL φ.
Finalement, puisque l’événement 0 est un élément de l’ensemble de tuples, l’OutputWriter conclut que la formule est vraie pour la trace analysée. À partir de cet exemple simple, on peut voir comment de multiples InputReader peuvent traiter les différentes parties de la même trace de façon indépendante. Dans les faits, l’InputReader n’a
pas besoin que les parties de la trace soient composées d’événements consécutifs au sein de l’ensemble, en autant que chaque événement soit correctement numéroté selon sa position séquentielle au sein de la trace. De plus, un effet secondaire de la mise en place du problème dans le cadre du principe MapReduce, c’est que le nombre d’occurrences de Mapper parallèles qui peuvent être utilisés pour traiter un ensemble de tuples d’entrée à chaque cycle, est variable et non statique. Bref, le nombre d’occurrences varie selon les besoins de la tâche en cours, sans compter que jusqu’à un Reducer par clé (c’est-à-dire un par sous-formule) peut fonctionner en parallèle dans la phase Reducer d’un cycle.

LTL-Past

La LTL-Past, la logique temporelle linéaire du passé, est une dérivé de LTL que l’on utilise dans le traitement de l’algorithme en version Hadoop. La différence est que cette dernière prend également en considération les opérateurs de la logique du passé.
C’est-à-dire des opérateurs mettant en relation l’événement courant avec des événements antérieurs de la trace. On verra ici comment l’algorithme que nous avons développé peut être étendu à ces opérateurs.

Les ajouts

Pour permettre l’utilisation de la LTL-Past, nous avons ajoutés la logique de ses opérateurs au sein de l’algorithme décrit précédemment. Toutefois, cette ajout est prit en compte uniquement dans la version Hadoop de l’algorithme. Par la suite, nous avons dû ajouter de nouvelles procédures pour les rendre accessibles dans la phase Reducer.

Opérateur S

L’opérateur S signifie « since ». La formule φ S ψ est vraie si φ est vrai pour tous les événements précédents jusqu’à ce qu’un événement vérifie ψ. C’est-à-dire que dès que la propriété de gauche a été observée, elle doit l’être pour l’ensemble des événements avant l’événement courant jusqu’à ce que la propriété de droite le soit. L’opérateur S est l’inverse de l’opérateur U; ils ont une méthode de traitement semblable, mais un comportement différent à partir de l’événement courant.

Opérateur H

L’opérateur H signifie « historically», ce qui implique par exemple dans le cas de la formule H φ que φ est vrai dans tous les événements passés de la trace, à partir de l’événement en cours. C’est-à-dire que la propriété à observer a toujours été vraie dans le passé. L’opérateur H est l’opérateur inverse de l’opérateur G.

Opérateur O

L’opérateur O signifie « Once ». La formule O φ est vraie si φ est vrai dans un événement passé de la trace. Autrement dit, cela veut dire que la propriété sera respectée par un événement passé contenu dans la trace, à partir de l’événement courant. L’opérateur O est l’opérateur inverse de l’opérateur F.

Opérateur Y

Finalement, l’opérateur Y signifie « yesterday » et la formule est vrai chaque fois que φ est vrai dans l’événement précédent de la trace. Donc, cet opérateur permet d’établir une relation entre l’événement courant et le précédent. L’opérateur Y est l’opérateur inverse de l’opérateur X.

Les impacts

Suite à l’intégration des opérateurs de la LTL-Past, le plus gros impact est d’augmenter la possibilité de traitement et de rendre possible l’utilisation d’opérateur des deux types de la LTL ensemble. L’algorithme pour chaque reducer est représenté dans la figure 10.
Lorsque la formule de haut niveau à évaluer est Y ψ, les événements qui satisfont la formule sont ceux qui succèdent immédiatement un événement qui respecte ψ. Donc, le reducer parcourt l’ensemble des tuples d’entrée <Y ψ,(ψ,n,i)> et produit pour chacun un tuple de sortie <Y ψ,(n+1,i)>.
Le reducer pour H ψ parcourt tous les tuples et garde dans un tableau booléen si ei ne satisfait pas ψ pour chaque événement i de la trace. Si définissons c comme l’indice du dernier événement pour lequel ψ n’est pas respecté, le reducer émettra des tuples de sortie de format <H ψ,(k,i)>, pour k ϵ [ ℓ, c-1]. Cela correspond alors à tous les événements pour lesquels H ψ est respecté.
Lorsque la formule de haut niveau à évaluer est O ψ, les événements qui satisfont la formule sont ceux qui dans le passé respectent ψ. Le reducer correspondant est celui qui parcourt les tuples d’entrée et calcule le plus petit numéro d’événement c pour lequel ψ est respecté. Tous les événements qui succèdent c respectent O ψ. Conséquemment, le format que le reducer génère comme tuple de sorties est <Oψ,( k,i)>, pour tout k ϵ [c,0].
Le dernier cas à considérer est une formule de forme ψ S ψ’. Le premier reducer parcourt tous ses tuples d’entrées et mémorise le numéro de l’événement qui respecte ѱ et ceux pour lesquels ψ’ est respecté. Il procède ensuite dans l’ordre à partir du premier événement de la trace et émet < ψ S ψ’, (n,i)> pour un certain événement n si ψ’ respecte n ou si ψ respecte n et qu’il existe une suite ininterrompue d’événements conduisant à un événement pour lequel ψ’ est respecté. Cette dernière information est conservée via la variable booléenne b.
Comme on peut le constater, les tuples produits par les reducers de la LTL-Past ont la même forme que ceux produits par la LTL, soit < ψ, (n,i)>. Ceci leur permet d’être traités dans les mêmes phases et objets de l’algorithme LTLValidator. La LTL-Past permet d’écrire certaines formules plus facilement, cela raccourcit la notation. Il est important de noter que toutes formules écrites avec la LTL-Past peuvent être réécrites avec la LTL.
Cependant, pour garder le sens voulu, il faut utiliser un ensemble d’opérateurs et de propriétés pour représenter un opérateur de la LTL-Past.

IMPLÉMENTATION DANS MR. SIM

Dans ce chapitre, nous décrirons comment l’algorithme présenté au chapitre précédent peut être implémenté concrètement en utilisant la première des plateformes MapReduce présentée en début de mémoire, soit MrSim.

LTLValidator

LTLValidator est un outil et algorithme permettant l’analyse d’une formule LTL sur une trace XML au moyen de MrSim. Son but est de pouvoir déterminer si oui ou non une formule LTL donnée est respectée dans l’ensemble de la trace. Pour ce faire, l’outil utilise comme logique les pseudo-codes préalablement présentés au chapitre 4 pour implémenter les phases du paradigme MapReduce. Pour savoir comment utiliser l’outil LTLValidator, nous référons le lecteur à l’annexe 1 de ce présent document.

Formules LTL

Pour pouvoir utiliser une formule LTL, dans tout système, il faut avoir une structure d’objet permettant de l’écrire et de représenter l’ensemble de ses opérateurs. Dans cette section, nous allons aborder la façon de l’écrire en utilisant les différents niveaux d’objets contenus dans la figure 12.
Pour commencer, nous devons avoir une déclaration de type unique pour l’ensemble des opérateurs. Cela nous permettra d’avoir un seul Mapper et un seul Reducer, chacun acceptant des tuples de ce type général. C’est alors que la classe « Operator » prend tout son sens. Son but est de contenir l’ensemble des fonctionnalités communes à l’ensemble des opérateurs LTL ainsi que la déclaration des fonctions que l’ensemble doit initialiser.
Il est important de noter que la classe « Operator » est abstraite, ce qui veut dire qu’elle ne peut être instanciée. Toutefois, on peut s’apercevoir avec la LTL qu’il existe plus d’un type d’opérateur et que ceux-ci ont des attributs et des méthodes leur étant propres.
Donc, pour écrire une formule avec succès, il faut prendre en compte la nature des opérateurs. Pour ce faire, il faut définir, comme le montre le niveau deux de la figure, des classes qui sont des héritiers de la classe abstraite Operator.
Il y a tout d’abord la classe « BinaryOperator » qui représente tous les opérateurs binaires nécessitant un sous-opérateur à gauche et à droite. À l’intérieur de la classe, on retrouve ses deux objets sous les noms de m_left et m_right, sans compter la chaîne m_symbol permettant de contenir la string de l’opérateur ainsi qu’une valeur booléenne permettant de représenter si l’opérateur est commutatif. Cette classe possède également des fonctions lui étant propres, tels que des accesseurs spécialisés pour ses objets de type Operator.
Ensuite, il y a la classe « Atom » qui permet de représenter les variables propositionnelles. Autrement dit, cette classe contient les variables et valeurs à observer dans la trace. La classe «Atom» possède la chaîne m_symbol contenant le nom de l’opérateur, soit dans ce cas-ci la variable « / » suivi de sa valeur, ainsi que des fonctions lui étant propre pour traiter ses données. Il est important de noter que l’on aurait pu implémenter la classe «Atom», sans que celle-ci soit une héritière de la classe abstraite «Operator». Toutefois, cela aurait augmenté la complexité d’écriture des formules LTL. La raison est que les deux autres types d’opérateurs contiennent un ou des opérateurs comme objet et une chaîne de caractère. Alors, il aurait fallu que l’on permette également d’utiliser un objet de type «Atom» et que l’on le traite. Donc, cela aurait eu comme impact d’augmenter la complexité du code et du transfert des données entre les différentes phases de l’algorithme.
La classe « UnaryOperator » permet de représenter tous les opérateurs unaires, c’està- dire, qui ne possède qu’une seule sous-formule. Cette dernière est représentée par l’objet m_operand et la classe contient également la chaîne m_symbol permettant de contenir le nom de l’opérateur.
Les classes que l’on vient de voir nous permettent d’associer la nature des opérateurs et de mieux écrire des formules LTL, mais comment fait-on pour différencier les différents opérateurs ? C’est à ce moment que la nouvelle génération de classe, tel que présenté au niveau trois de la figure, permet de spécialiser le traitement de chaque opérateur. Pour les opérateurs qui héritent de la classe « BinaryOperator » et de la classe « UnaryOperator », la façon de faire ressortir leur caractère unique est pareille. Il faut tout simplement, définir le symbol qui les représente, créer des constructeurs qui permettent de bien initialiser l’objet qui les représente et de bien définir comment on effectue la comparaison de cet objet. Ensuite, dans le cas du type « Atom », la classe enfant à utiliser est « XpathAtom » et cette dernière contient un tableau de chaîne de caractères : son contenues est le nom de la variable et valeur.

LTLTuple

La classe LTLTuple permet de créer des tuples plus spécifiques au traitement LTL pour contenir les données. La classe Tuple est fournie par Mr Sim et elle permet de contenir une clé de type abstrait K et une valeur de type abstrait V. Cette classe fournit des accesseurs de valeurs et une méthode permettant d’avoir le tuple dans un format chaîne de caractères (string).
La classe LTLTuple permet d’orienter l’utilisation de Tuple selon la logique LTL.
Dans les faits, lors de la déclaration de la classe LTLTuple, la déclaration de la classe Tuple a une clé K et une valeur V de type bien précis. Dans le cas de la clé, le type spécifié est «Operator», ce qui permettra de pouvoir spécifier un objet opérateur servant à contenir la formule à appliquer sur les données. Pour les données, son type spécifié est de LTLTupleValue, qui à pour but de contenir l’ensemble des données à traiter. Dans ce casci, les données sont l’ensemble des possibilités de contenus que nous avons vus lors de la présentation des pseudo-codes du chapitre 4. Plus précisément : le numéro de l’événement, un opérateur et le numéro de l’itération.

Phase lecture

La phase de lecture des données est assurée par des instances de la classe InputFormat lors de la phase d’InputReader dans des environnements MapReduce distribués. Dans notre cas, la phase est effectuée par des instances de type parser XML qui ont pour tâche de traiter l’ensemble des éléments contenus dans la source de données. Il est important de noter que dans sa version de base de Mr Sim, le seul parser qui était disponible était de type DOM (Document Object Model). Le type DOM permet de parcourir et manipuler les objets XML sous forme d’arbre. Les objets sont alors tous contenus dans la mémoire vive de la machine. Par la suite, le parser SAX (Simple API for XML) a été ajouté pour pouvoir offrir la possibilité de traiter de plus grand ensemble de données. Le type SAX permet de parcourir les données dans le fichier sans les avoirs dans la mémoire vive de la machine et lorsque nécessaire, il est possibles de parcourir une partie du fichier et non sa totalité.
En premier lieu, le parser DOM lit l’entièreté des éléments à traiter, soit dans notre cas des événements contenus dans un document XML, et les sauvegarde en mémoire. Il est important de savoir que notre parser DOM est dit « intelligent », c’est-à-dire qu’il effectue un traitement en lien avec nos besoins au niveau de la LTL. Le parser émet seulement les paramètres des événements en lien avec la formule à évaluer.
Le fonctionnement du parser SAX est presque identique. La seule différence se situe au niveau de la lecture des données. Le parser SAX lit les événements un par un et les traites immédiatement après les avoir lues. Ce parser a été créé suite à l’apparition du fait que le parser DOM prenait tout l’espace mémoire et que le traitement aboutissait sur une erreur. Cela a donc permis de repousser la possibilité de lecture et de traitement de l’algorithme LTLValidator avec Mr Sim.

Mr Sim parallèle

L’outil Mr Sim a subi une modification importante au niveau des possibilités qu’il offre à l’utilisateur. Il est maintenant possible d’utiliser le parallélisme à l’intérieur de l’exécution de Mr Sim. Un flux de travail parallèle (ParallelWorkflow) à été ajouté à l’outil, permettant d’effectuer le traitement de l’algorithme en utilisant plus d’un Mapper ou Reducer en même temps. La façon de l’utiliser ressemble beaucoup au flux de travail séquentiel. La seule différence est qu’il utilise des objets de type «ResourceManager» lors de l’instanciation de l’objet.

Table des matières

RÉSUMÉ
REMERCIEMENTS
TABLE DES MATIÈRES
LISTE DES TABLEAUX
LISTE DES FIGURES
CHAPITRE 1 INTRODUCTION
CHAPITRE 2 REVUE DE LITTÉRATURE
2.2 La logique temporelle linéaire (LTL)
2.2.1 Trace d’événements
2.2.2 LTL
2.2.3 Opérateurs Temporels
2.2.3.1 Opérateur G
2.2.3.2 Opérateur F
2.2.3.3 Opérateur U
2.2.3.4 Opérateur X
2.2.4 Syntaxe et Sémantique formelle de la LTL
2.3 Les outils séquentiels
2.3.1 BeepBeep
2.3.2 Logscope
2.3.3 Maude
2.3.4 Monid
2.3.5 MonPoly
2.3.6 ProM
2.3.7 RuleR
2.3.8 Saxon
2.3.9 SEQ. OPEN
2.3.10 Résumé
CHAPITRE 3 MAPREDUCE
3.1 Description des composants de MapReduce
3.1.1 L’InputReader
3.1.2 Mapper
3.1.3 Shuffling
3.1.4 Reducer
3.1.5 OutputWriter
3.2 Exemple de tâche
3.2.1 Mapper
3.2.2 Reducer
3.2.3 Objet de la tâche
3.2.4 Exécution de la tâche
3.3 Environnements MapReduce
3.3.1 Mr Sim
3.3.1.1 WordCount de Mr. Sim
Figure 5 : Tâche Mr Sim WordCount
3.3.2 Hadoop
3.3.2.1 WordCount de mode Hadoop
3.3.3 Mr Sim VS Hadoop
CHAPITRE 4 LTL APPLIQUÉE AU MAPREDUCE
4.2. Format de la trace et l’InputReader
4.3 Mapper
4.4 Reducer
4.5 OutputWriter
4.6 Exemple
4.7 LTL-Past
4.7.1 Les ajouts
4.7.1.1 Opérateur S
4.7.1.2 Opérateur H
4.7.1.3 Opérateur O
4.7.1.4 Opérateur Y
4.7.2 Les impacts
CHAPITRE 5 IMPLÉMENTATION DANS MR. SIM
5.1 LTLValidator
5.1.1 Formules LTL
5.1.2 LTLTuple
5.1.3 Phase lecture
5.1.4 Mr Sim parallèle
5.2 Outils connexes
5.2.1 XMLTraceGenerator
5.2.2 TagCounter
5.2.3 JobLauncher
CHAPITRE 6 IMPLÉMENTATION DANS HADOOP
6.1 Environnement de développement
6.2 Structure XML
6.3 Format d’entrée de Hadoop
6.3.1 FileInputFormat
6.3.2 LTLInputFormat1Gen
6.3.3 LTLInputFormatXGen
6.4 Format des objets de transitions
6.4.1 Writable
6.4.2 WritableComparable
6.5 Format de sortie
6.5.1 LTLOutputFormatXGen
6.5.2 LTLOutputFormatLastGen
6.6 Instanciation de la tâche
6.6.1 L’objet jobConf
6.6.2 Les formats de sortie
CHAPITRE 7 CLUSTER HADOOP MAPREDUCE
7.2 L’univers VMware
7.2.1 Project Serengeti
7.2.2 VMware VSphere
7.2.3 VMware VCenter Server
7.2.4 Windows Server 2008
7.2.5 Le déploiement du cluster
7.3 L’univers Solaris
7.3.1 Oracle Solaris 11.1
7.3.2 Oracle VM VirtualBox
7.3.3 Observation sur le tutoriel
7.3.4 Exécution de tâche sur un cluster
CHAPITRE 8 TESTS DE PERFORMANCE ET COMPARAISONS
8.1 Environnement d’exécution
8.2 Les environnements de tests
8.2.1 Mr Sim
8.2.2 Hadoop
8.3 Formules LTL
8.4 Résultats
8.4.1 Nombre de tuples
8.4.2 Temps d’exécution
CONCLUSION
BIBLIOGRAPHIE
ANNEXE 1
ANNEXE 2
ANNEXE 3
ANNEXE 4
ANNEXE 5

Télécharger le rapport complet