Une étude des futurs de première classe (spécification, formalisation et preuves formelles)

Futures enable an efficient and easy to use programming paradigm for distributed applications. A future is a placeholder for result of concurrent execution. Futures can be first class objects; first class futures may be safely transmitted between the communicating processes. Consequently, futures spread everywhere. When the result of a concurrent execution is available, it is communicated to all processes which received the future. In this thesis, we study the mechanisms for transmitting the results of first class futures; the future update strategies. We provide a detailed semi-formal specification of three main future update strategies adapted from ASP-calculus; we then use this specification for a real implementation. We study the efficiency of the three update strategies through experiments. Ensuring correctness of distributed protocols, like future update strategies is a challenging task. To show that our specification is correct, we formalise it together with a component model. Components abstract away the program structure and the details of the business logic ; this paradigm thus facilitates reasoning on the protocol. We formalise in Isabelle/HOL, a component model comprising notions of hierarchical components, asynchronous communications, and futures. We present the basic constructs and corresponding lemmas related to structure of components, and formal operational semantics of our components in presence of a future update strategy; proofs showing correctness of future updates are presented. Our work can be considered as a formalisation of ProActive/GCM, and shows the correctness of the middleware implementation.Les futurs fournissent une modèle de programmation efficace pour le développement des applications distribuées. Un futur est une objet temporaire qui représente le résultat d une exécution concurrente. Les futurs peuvent être des objet de première classe , et ainsi être transmis en toute sécurité entre les processus communicants. En conséquence, les futures se propagent partout dans le système. Lorsque le résultat d une exécution simultanée est disponible, il est communiqué à tous les processus qui ont reçu le futur. Nous étudions les mécanismes de transmission des résultats des futurs; les "stratégies pour mise à jour des futurs". Nous fournissons une spécification semi-formelle détaillée, de trois principales stratégies. Nous utilisons ensuite cette spécification pour une véritable implémentation et nous étudions l efficacité des trois stratégies. C est une tâche difficile d assurer la correction des protocoles distribués. Pour montrer que notre spécification est correcte, nous la formalisons avec un modèle de composants. Les composants abstraient la structure du programme ; ce paradigme facilite donc le raisonnement sur le protocole. Nous formalisons dans Isabelle/HOL un modèle de composants comprenant des notions de composants hiérarchiques, les communications asynchrones, et les futurs. Nous présentons les constructions de base et des lemmes liés à la structure des composants. Nous présentons une sémantique formelle des nos composants en présence d une stratégie de mise à jour de futurs ; Les preuves montrant la correction de notre stratégie sont présentées. Notre travail peut être considéré comme une formalisation de ProActive / GCM.NICE-BU Sciences (060882101) / SudocSudocFranceF