L’objectif de cet article est de donner un retour d’expérience de la preuve B pour la détection du risque de fuite mémoire dans le code généré à partir d’un modèle B.

La fuite mémoire désigne une situation dans laquelle des emplacements de mémoire vive, alloués d’une manière dynamique, ne sont jamais libérés pendant ou à la fin d’une exécution d’une application. En conséquence, ces emplacements mémoire ne sont plus accessibles d’une manière correcte et au fûr et à mesure, la mémoire sera saturée. La saturation de la mémoire peut causer l’arrêt de l’exécution des applications ou forcer le redémarrage de l’ordinateur.

La gestion de la mémoire dans le modèle S2OPC¶

Besoin d’un mécanisme spécifique¶

La méthode B ne se dispose pas de mécanisme pour effectuer les opérations d’allocation / de libération de mémoire. Ainsi les fonctions utilisant ces opérations sont implémentées en code d’un langage de programmation en dehors d’un modèle B. La liaison entre ce code et le modèle B se réalise par les composants spécifiques : des machines de base. Nous devons avoir un mécanisme spécifique pour garantir l’absence de fuite mémoire dans le code généré à partir d’un modèle B.

Note : Dans l’architecture d’un modèle B, un module développé posséde des machines abstraites (.mch), des éventuels raffinements (.ref) et des implantations (.imp). Les implantations sont traduites automatiquement en code d’un langage de programmation. Un module de base ne possède pas d’implantation: le code associé à un module de base ne s’obtient pas par une traduction (B -> C / Ada), mais par un codage manuel (cf. Manuel de Référence du Lanagage B).

Principe¶

Variable de contrôle : Une des manières simples pour modéliser le contrôle de la libération de mémoire allouée est d’utiliser une variable de contrôle, dénotée is_allocated. Le lien avec la mémoire allouée, modélisée par nb_elements par souci de simplification, est le suivant :

A l’initialisation : is_allocated = FALSE & nb_elements = 0
Lorsque la mémoire est allouée avec réussite : is_allocated = TRUE & nb_elements > 0
Lorsque la mémoire est libérée, is_allocated = FALSE & nb_elements = 0

La figure suivante illustre une implémentation de ce principe.

Propriétés à considérer : L’absence de fuite mémoire est garantie par les propriétés is_allocated = FALSE et is_allocated = FALSE => nb_elements = 0. Autrement-dit, à partir d’un certain niveau dans l’architecture IMPORTS d’un modèle B, la propriété is_allocated = FALSE doit être vérifiée. Ce qui veut dire qu’avant ou après chaque appel d’opération de ce niveau, aucune mémoire n’est allouée (ou toute mémoire allouée a été libérée).

Ces propriétés peuvent s’exprimer sous forme d’invariant d’un composant B et/ou de pré-condition / post-condition des opérations.

Dans tous les cas, une démonstration de la correction des opérations au travers de l’activité de preuve permet la détection de la non-libération de mémoires qui ne sont plus utilisées.

Activité de preuve¶

Cette activité consiste en la démonstration des PO (Proof Obligation / Obligation de preuve). Une PO est une formule mathématique de la forme Hypothèses => But. Les PO sont générées par le générateur de PO suivant les principes définis dans le document Obligations de preuve - Manuel de référence. De plus, le moteur de preuve interactif classifie les PO générées dans certaines catégories, par exemple :

Check preconditions of called operation, or While loop construction, or Assert predicates
Check operation refinement
Check that the invariant (inv) is preserved by the operation - ref 4.4, 5.5
etc.

Autrement-dit, plusieurs catégories de PO peuvent être générées vis-à-vis de nos propriétés garantissant l’absence de fuite mémoire.

Un exemple de modélisation et preuve dans service_set_view ¶

PO non-prouvables¶

Dans l’activité de preuve du service_set_view, nous nous amenions à démontrer une PO de l’opération locale treat_browse_request_BrowseValue_1 du composant service_set_view_i. Le but de la PO est le suivant :

    "`Check preconditions of called operation, or While loop construction, or Assert predicates'"
=>
    isBrowseResultAllocated$1 = FALSE

Le but de la PO paraît très simple : il ne contient pas de fermeture réflexive d’une relation, de restriction / soustraction sur le codomaine, de quantificateur universel / existentiel, etc. Le seul souci : impossible de le prouver !

Contexte de la PO ¶

La figure ci-dessus présente le lien IMPORTS des composants et le graphe d’appels des opérations liées à la PO :

treat_browse_request_BrowseValues contient une boucle dans laquelle treat_browse_request_BrowseValue_1 est appelée.
getall_and_move_browse_result est appelée seulement si compute_browse_result renvoie e_sc_ok ou e_sc_bad_no_continuation_points.
L’allocation de mémoire est réalisée par l’opération alloc_browse_result et caractérisée par le statut isBrowseResultAllocated et la mémoire allouée max_nb_references. Une des précondition de l’opération alloc_browse_result est isBrowseResultAllocated = FALSE.
La libération de mémoire est réalisée par getall_and_move_browse_result ou clear_browse_result. La différence entre ces deux opérations est que la première renvoie aussi le résultat de Browse.
Il n’y avait pas de propriété isBrowseResultAllocated = FALSE dans l’invariant du module service_set_view

Ce contexte amène à la situation dans laquelle alloc_browse_result est appelée alors que sa précondition isBrowseResultAllocated = FALSE n’est pas vérifiée (car à l’entrée de la boucle, nous n’avons pas la condition isBrowseResultAllocated = FALSE, et durant la boucle getall_and_move_browse_result n’est pas appelée systématiquement). Ainsi la PO est non-prouvable.

Note : Dans le graphe d’appel d’opérations, il n’y a pas de flèche reliant une opération promue avec son origine qui se trouve au niveau inférieur du lien IMPORTS : du point de vu de code généré, ces opérations sont identiques. Par exemple, pour l’opération compute_browse_result qui est promue du module browse_treatment au module translate_browse_path_result, le code généré est le suivant :

#define translate_browse_path_result__compute_browse_result browse_treatment__compute_browse_result

Analyses¶

La PO permet de détecter le code amenant aux risques de fuite mémoire qui n’a pas été détectée par les tests fonctionnels.
La bonne spécification de la machine de base browse_treatment_result_bs nous permet de détecter le problème de fuite mémoire lors de l’activité de preuve :
- Dans les post-conditions des opérations alloc_browse_result, getall_and_move_browse_result et clear_browse_result (cf. l’exemple ci-dessous sur clear_browse_result), les conditions liées aux variables isBrowseResultAllocated et max_nb_references sont bien modélisées : nous avons la propriété isBrowseResultAllocated = FALSE => max_nb_references = 0 vérifiée d’une manière implicite.
```
d_init_out ==
    d_variables_out
    :(
    // ...
    max_nb_references                = 0
    )
d_init_out_status ==
    isBrowseResultAllocated := FALSE

clear_browse_result =
BEGIN
    d_init_out ||
    d_init_out_status
END
```
- La pré-condition isBrowseResultAllocated = FALSE de l’opération alloc_browse_result modélise d’une manière implicite le besoin d’avoir la propriété isBrowseResultAllocated = FALSE vérifiée au niveau du module service_set_view.
```
p_alloc_bres <-- alloc_browse_result(p_maxResultRefs) =
PRE
    isBrowseResultAllocated = FALSE         &
    // ...
THEN
    CHOICE
        /* Out of memory */
        p_alloc_bres := FALSE
    OR
        p_alloc_bres := TRUE ||
        d_variables_out,
        d_variables_out_status
        :(  // ...
            isBrowseResultAllocated            = TRUE             &
            max_nb_references                  = p_maxResultRefs  &
            // ...
```
En effet, cette pré-condition doit être vérifiée lorsque alloc_browse_result est appelée dans treat_browse_request_BrowseValue_1, et elle se propage jusqu’au treat_browse_request du module service_set_view.
L’implantation en langage de programmation de la machine de base, browse_treatment_result_bs.c, est conforme à la spécification de la machine de base.
Pour rendre la PO prouvable, la correction à apporter consiste en :
- une libération de mémoire dans les cas où compute_browse_result renvoie un code différent de e_sc_ok et de e_sc_bad_no_continuation_points. Cela permet de prouver la PO durant la boucle au sein de treat_browse_request_BrowseValues.
- un ajout du prédicat isBrowseResultAllocated = FALSE dans l’invariant du module service_set_view. Cela permet de prouver la PO à l’entrée de la boucle. Cet ajout est justifié par le fait qu’à la fin de traitement du service treat_browse_result (comme tous les autres services view), la mémoire allouée pendant ce service doit être libérée.

Conclusion¶

Les implantations des opérations dans le modèle B sont traduites en code exécutable. Ce dernier peut être testé pour détecter des erreurs fonctionnelles. En revanche, les spécifications abstraites des opérations et les invariants permettent de modéliser aussi des aspects non fonctionnels dont l’absence de fuite mémoire fait partie. L’activité de preuve est un moyen efficace pour la détection de problèmes liés à ces aspects.