Muhammad Uzair Khan

Home     |     Publications/Talks     |     Formal proofs     |   Thesis

    I am a Ph.D student from Pakistan, in the OASIS team at Inria Sophia Antipolis.
    Supervised by:- Ludovic Henrio  and Denis Caromel.

 Research Unit
 Sophia Antipolis
 (+33)4 97 15 53 71
 Postal address
 2004, Route des Lucioles - BP93 06902 
 Sophia Antipolis Cedex - France

Research Area:

Keywords:  Distributed systems,  First class futures, Future update strategies, Components,  Formal methods

     Futures enable an efficient and easy to use programming paradigm for distributed applications.  In ProActive, an active object is analogous to a process, having its own thread and a message queue for storing incoming requests.  Futures, as used in ASP and ProActive, represent the result of an asynchronous invocation and can be safely transmitted between processes.  As references to futures disseminate, a strategy is necessary to propagate the computed result of each future to the processes that need it.

     Our work focuses on efficient transmission of future values. We study various strategies that may be used to update first class futures. An important aspect of the work is to present the contributions in a language independent manner so that they can be applied directly to various existing frameworks that support first class futures, for example Creol and AmbientTalk in addition to ProActive.

    Theoretical Aspect:-  We  focus on theoratical aspects such as formalization of future update strategies using Isabelle/HOL. For formalizing our strategies, we are extending a formalization of GCM model. GCM is a component model defined by the European Network of Excellence CoreGrid. It extends the Fractal component model, by addressing Grid computing: it supports deployment, scalability, autonomic behavior, and asynchronous communications.
    The formalization comprises notions of Components, futures and asynchronous communications. Components form the basic units of concurrency (actors) and are hierarchical. Communication takes place via asynchronous message exchanges. The model allows for first class futures that are used as placeholdersfor the results of asynchronous invocations. Components are loosely coupled and synchronization is achieved through wait by necessity. Using this formalization, We are interested in proving characteristics like  `all requested futures are eventually updated' and `All strategies are semantically equivalent'. This semantic equivalence is of particular interest as it allows for replacing one strategy by another without affecting the application.
      Implementation:-   In addition to this theoratical work,  we focus on implementing the various future update strategies in ProActive with the aim of evaluating the effciency of each strategy in a given configuration.