Linéarisabilité

Pour un autre texte important sur la conception d'objets concurrents, voir A Methodology for Implementing Highly Concurrent Data Objects par Maurice P. Herlihy en 1991

En 1987, Maurice P. Herlihy et Jeannette M. Wing ont publié un article célèbre nommé Linearizability: A Correctness Condition for Concurrent Objects. Leur texte procède selon le raisonnement suivant :

Un calcul concurrent est linéarisable s'il est équivalent, dans un sens précis, à un calcul séquentiel. Les opérations concurrentes semblent prendre effet instantanément, et les opérations séquentielles semblent se faire dans l'ordre prévu par le code source.

La linéarisabilité d'un calcul dans son ensemble requiert la linéarisabilité des calculs sur chacun de ses objets concurrents, ce qui fait de cette caractéristique une propriété locale, et facilite le raisonnement : il est plus simple de vérifier la linéarisabilité de chaque objet sur une base individuelle que d'essayer de la vérifier sur un système complexe fait d'une multitude d'objets concurrents.

Autre caractéristique appréciable de la linéarisabilité : elle est foncièrement non-bloquante, ce qui accroît la concurrence et se prête à une application dans un contexte de systèmes en temps réel.

Une conséquence d'un système linéarisable est qu'a posteriori, il est possible de regarder l'histoire de l'exécution du système et d'en tirer une image cohérente pour tous les threads qui y ont participé. Cette histoire se lit sur l'ordonnancement des écritures sur les états partagés : si le système est linéarisable, alors les threads reconnaîtront une séquence commune pour ces écritures (sauf si deux écritures se sont produites en même temps et ne définissent pas une séquence d'événements).

Notez que dans l'article original, les événements étaient définis comme des appels de fonctions et des retours de fonctions. Une histoire séquentielle était faite d'un enchaînement d'appels et de retours de fonctions; une histoire non séquentielle était dite concurrente. Une sous-histoire de l'histoire d'un processus est un ordonnancement irréflexif d'événements.

Propriétés de la linéarisabilité

L'article définit ainsi les propriétés de la linéarisabilité :

La linéarisabilité mène aussi naturellement à une forme de sérialisabilité, dont l'une des conséquences est l'avènement de mémoire transactionnelle.

Vérifier qu'une opération est linéarisable

Puisqu'un système est linéarisable si ses objets concurrents le sont, le raisonnement se porte naturellement sur les objets et leur construction. L'article propose une démarche abstraite en ce sens, ce qui est raisonnable sur le plan de la démonstration mathématique, mais concrètement l'idée est de vérifier le respect de cette propriété de chaque objet concurrent, tout simplement.

La linéarisabilité est implicite sur les atomiques; le recours à des atomiques est d'ailleurs en partie une conséquence de la définition de la linéarisabilité.

La linéarisabilité sera aussi implicite sur un objet correctement synchronisé (p. ex. : les zones de transit), dans la mesure où les méthodes des objets en question complètent leur exécution dans un nombre d'étapes / dans un temps maximal connu a priori..


Valid XHTML 1.0 Transitional

CSS Valide !