HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Asynchronous Components with Futures: Semantics and Proofs in Isabelle/HOL

Ludovic Henrio 1 Muhammad Uzair Khan 1
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : Components provide an easy to use programming paradigm allowing for better re-usability of application code. In the context of distributed programming, autonomous hierarchical components provide a simple model for creating efficient applications. This paper presents a model for distributed components communicating asynchronously using futures – placeholders for results. Our components communicate via asynchronous requests and replies where the requests are enqueued at the target component, and the invoker receives a future. Then, future references can be dispersed among components. When the result is available for a future, it needs to be transmitted to all interested components, as determined by a future update strategy. We present formal semantics of our component model incorporating formalisation of one such future update strategy. Our model has been mechanically formalised in Isabelle/HOL, together with the proof of properties. This approach validates the actual implementation of the future update strategy itself.
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00462325
Contributor : Muhammad Uzair Khan Connect in order to contact the contributor
Submitted on : Friday, May 28, 2010 - 4:02:14 PM
Last modification on : Friday, February 4, 2022 - 3:11:36 AM
Long-term archiving on: : Friday, October 19, 2012 - 2:16:07 PM

File

FutureUpdateGCM.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00462325, version 1

Collections

Citation

Ludovic Henrio, Muhammad Uzair Khan. Asynchronous Components with Futures: Semantics and Proofs in Isabelle/HOL. 7th International Workshop on Formal Engineering approaches to Software Components and Architectures, Mar 2010, Paphos, Cyprus. pp.1-20. ⟨inria-00462325⟩

Share

Metrics

Record views

143

Files downloads

141