Home     |     Publications/Talks     |     Formal proofs     |   Thesis

Abstract:-

      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 in a distributed programming library. 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. We present formal operational semantics of our components in presence of a future update strategy; proofs showing correctness of our future update strategy are presented. Our work can be considered as a formalisation of ProActive/GCM and shows the correctness of the middleware implementation.

Une étude des futurs de première classe: Spécification,
Formalisation, et Preuves Formelles

Abstract:-

     Les futurs fournissent une modèle de programmation efficace, et facile a utiliser pour le développement des application distribuées. Un futur est une ob jet temporaire qui représente le résultat d’une exécution concurrente, et donc simultanée. Les futurs peuvent être des ob jet 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ée à tous les processus qui ont reçu le futur. Dans cette thèse, nous étudions les mécanismes de transmission des résultats des futurs de première classe; les "stratégies pour mise à jour de futurs".

    Nous fournissons une spécifications semi-formelle détaillées, de trois principales stratégies pour mettre à jour les futurs. Ces stratégies sont adaptées à partir d’ ASP. Nous utilisons ensuite cette spécification pour une véritable implémentation dans une bibliothèque de programmation distribuée. Nous étudions l’efficacité des trois stratégies, grâce à des expérimentations. C’est une tâche difficile d’assurer la correction des protocoles distribués, comme les stratégies pour mise à jour des futurs. 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 et
montre que les principes selon lesquels est implémenté le middleware sont coprrects.




Download Manuscript