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 <>
Submitted on : Friday, May 28, 2010 - 4:02:14 PM
Last modification on : Monday, October 12, 2020 - 10:30:26 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

406

Files downloads

304