Foundations of Software Technology
Research team
Eneia Nicolae Todoran, Paulina Mitrea, Cornelia Melenti, Iulia Costin
Research fields
- Programming Languages Design and Semantics
- Continuation Semantics for Concurrency
- Type Systems and Software Engineering
- Global Computing Models and Technologies
Recent research projects
“Continuations and monads for parallel and distributed computing”, bilateral Greek-Romanian research collaboration; Contract C 18313; (2003-2005)
K. Pusztai Romanian project manager, E.N. Todoran, C. Ivan.
“Semantic techniques in concurrent systems development”, national research grant funded by CNCSIS A-932; (2005-2007).
E. N. Todoran project manager, P. Mitrea, C. Melenti, D. Mitrea.
In this project we introduced a methodology for concurrent languages development based on denotational semantics. We showed that, by using the continuation semantics for concurrency (CSC) technique (recently introduced by us), denotational semantics can be used not only for formal specification and design but also as a general method for building compositional prototypes of concurrent programming languages. From a software engineering perspective, the methodology is based on a combination of exploratory prototyping and formal methods.
When CSC is used in the semantic design, the nondeterministic behavior can be modeled in at least two ways: by using a monad parameterized by an oracle (based on a random number generator) to produce incrementally a single possible trace of execution, or by using a classic power domain monad to compute all possible execution traces for a given program (as in classic denotational semantics). The
program behavior monad establishes a simple relationship between a specification and a corresponding prototype. In the CSC approach all control concepts (including parallel composition and process synchronization) are encapsulated in continuations, and only the final yield of the denotational mapping distinguishes between a specification and a corresponding prototype.
We developed mathematical prototypes designed with CSC continuations and specific semantic domains for synchronous communication and concurrency. The immediate implementation of such a semantic prototype in an appropriate functional language is a compositional interpreter for the concurrent language under study. By using the functional programming language Haskell, we developed semantic interpreters designed with CSC for various concurrent control concepts, including distributed object oriented programming, and higher order communication.
The CSC technique provides excellent flexibility in the compositional design of concurrent programming languages. To the best of our knowledge, denotational semantics has never been used systematically for concurrent languages prototyping, and all our attempts to get a general solution to this problem by using only classic compositional techniques have failed.
“GlobalComp: Models, semantics, logics and technologies for global computing”, national research grant funded by ANCS, CNMP-PC, no. 11-052/2007; (2007-2010).
E.N. Todoran project coordinator, P. Mitrea, M. Ivan, R. Potolea, V. Dadarlat, A. Rarau, I. Costin, D. Mitrea, C. Melenti, C. Ivan.
The GlobalComp project involves four academic partners - The Technical University of Cluj-Napoca (project coordinator), “Babes-Bolyai” University of Cluj-Napoca, The University of Bucharest and A. I. Cuza University of Iasi - and one partner from industry - Siemens PSE.
A global computing (GC) system is a programmable infrastructure distributed at worldwide scale and available globally. GC distinguishes from traditional distributed computing in terms of scalability, connectivity, heterogeneity and autonomy. Within the framework of this project we will study systems compatible with the notion of GC. The most prominent example is that of the Web space; the growing complexity of the entire collection of Internet services brings the need for a change in the view of the Web space as just a database. In the emerging GC vision, the Web should become a programmable space. An important research theme of this project will be the study of GC from the perspective of the Peer-to-Peer (P2P) paradigm.
We intend to study and elaborate new formal models (that enable formal reasoning) and technologies for a number of GC key issues: distributed networks with dynamic topologies, data and code mobility, security, coordination and control. We will perform experiments on P2P architectures, and develop prototype implementations for various GC concepts, models and calculi. For the theoretical aspects of our research we will use our previous experience with process algebras, membrane systems, spatio-temporal logics, continuations, type systems, etc. At The Technical University of Cluj-Napoca we will mainly focus on the use of type systems and the continuation semantics for concurrency (CSC) technique (recently introduced by us). In particular, our aim is to collect sufficient evidence that the (dynamic) topology of a GC system can be represented in a natural manner as a CSC structured continuation.
Publications
E. N. Todoran. Software prototyping and formal specification. Mediamira, Cluj-Napoca, 2006 (in Romanian).
E. Todoran, F. M. Boian, C. Melenti, N. Papaspyrou, “Continuations for remote object control”. Studia Universitatis Babes-Bolyai Informatica, vol. L, no. 1, 2005, pp. 21-37.
E. Todoran, P. Mitrea, N. Papaspyrou: “Comparative Semantics for the Basic Andorra Model”, Automation Computers Applied Mathematics, Scientific Journal (ACAM), vol. 14, nr.1, 2005, pp. 27-43.
E. Todoran, N. Papaspyrou, K. Pusztai. “Denotational prototype semantics for a simple CSP-like language”. in Proceeding of the IEEE 8th International Conference on Intelligent Engineering Systems (INES 2004), 2004, pp. 319-324.
E. Todoran, K.Pusztai, P. Mitrea, N. Papaspyrou: “Comparative semantics for the Basic Andorra Model”, Automation Computers Applied Mathematics. Scientific Journal (ACAM), vol.13, no. 1, 2004.
E. N. Todoran, N. Papaspyrou, F. Boian, C. Ivan. “Continuation semantics for concurrency and concurrent languages prototyping”. Scientific Annals of A.I. Cuza University, vol. 15, 2004, pp. 22-37.
Research description
Continuations and monads for parallel and distributed computing
The collaboration with the Greek partner (professor dr. M. Skordalakis and dr. N. Papaspyrou) began during the visit of professor dr. K. Pusztai and dr. E. N. Todoran at The National Technical University of Athens in 1999, within the framework of a Tempus PHARE project. During that visit it became obvious that the two groups have common research interests in the domain of formal description techniques.
We considered two of our previous achievements: a resumption monad transformer (designed by N. Papaspyrou) and its application in the semantics of concurrency, and the continuation semantics for concurrency (CSC) technique (introduced by E. N. Todoran in 2000). The CSC technique can be used to model both sequential and parallel composition in interleaving semantics, as well as various mechanisms for synchronous and asynchronous communication. We decided to investigate the possibility to combine our previous ideas in order to develop a new approach to communication and concurrency based on the concepts of continuation (to improve the flexibility) and monad (to improve the modularity of the semantic descriptions). The main achievements of this project can be summarized as follows.
We showed that the CSC technique gives the language designer the ability to establish a simple relation between a general notion of structured continuation and the control concepts of the concurrent language under study. We proposed carefully designed continuation structures for various concepts of communication and concurrency, including: parallel composition, process creation, synchronous CSP-like communication, ADA-like rendez-vous, distributed objects and remote object (process) control. We introduced the ps-tree, a specific continuation structure for the control flow semantics of concurrent languages inspired from the notion of a cactus stack.
The simple and abstract way in which we defined the control flow semantics of concurrent languages was mainly due to the use of monads, which provide a unified way of presenting the semantics of fundamentally different (concurrent) languages. In our work, the semantic models are parameterized by a monad whose role is to abstract the behavior of elementary actions and the semantic interpreters. An important characteristic of the semantic models designed with continuations and monads is that they produce exactly the desired observables assembled in linear models, rather than complex branching structures, without having to incorporate communication attempts and silent steps, as in classic resumption-based models.
The CSC technique provides excellent flexibility in the denotational (compositional) modeling of concurrent control concepts. By using this technique, we were able to design denotational models for the following advanced control concepts that have never been modeled compositionally without CSC: remote object (process) destruction and cloning, and nondeterministic promotion in Andorra-like languages.