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

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.