Decades after Turing proposed his model of computation, we still lack suitable means to tackle the complexity of getting more than a few Turing Machines to interact with one another in a verifiably coherent manner. This dearth currently hampers software engineering in unleashing the full potential of multi-core platforms. The coordination language Reo, developed by the Foundations of Software Engineering group at CWI, offers a promising approach to overcome this obstacle by fulfilling the role of a domain specific language (DSL) for compositional specification of protocols.
To utilize massively concurrent multi-core platforms, modern software engineering must develop:
- New compositional programming language constructs and paradigms that allow software developers to explicitly express the concrete interaction protocols in their applications at a high-level of abstraction, shielding them from the low-level details of the concurrency involved, and its mapping onto a multi-core architecture.
- Compositional, scalable verification, analysis, and testing techniques for reasoning about correctness and quality of service properties based on formal methods.
- Efficient, dynamic scheduling, resource allocation, and reconfiguration techniques for utilizing processor cores, memory units, and communication bandwidth, to satisfy performance and predictability requirements.
Models of concurrency embedded in conventional general-purpose programming languages offer only low-level constructs (such as threads, semaphores, locks, etc.) for building interaction protocols to coordinate the concurrent execution of computing actions. Moreover, these languages do not structurally enforce modularization of protocols as a concern separate from computation code. Consequently, dispersing protocol code among computation code comprises a common methodology for specifying structured interaction among threads.
Figure 1: A Java implementation of a typical producer-consumer scenario
Figure 1, a Java implementation of a typical producer-consumer scenario, exemplifies this phenomenon: lines 4-6, 9-11, 20-22, and 27-29 implement the protocol. This methodology suffers from several shortcomings. For example, intertwining computation and protocol code makes protocols nebulous, latent, and intangible. It prevents different groups from working independently on computation and protocol code, and prevents reusing code in other applications. The negative impact of these shortcomings increases as programs grow larger and more complex.
Reo offers an alternative wherein programmers build protocols as concrete first-class constructs, by directly composing simpler (ultimately, primitive) protocols [1]. Reo [2], a visual programming language, has various formal semantics for describing the behaviour of Reo programs, called connectors, and tools for their verification and analysis [3]. These include both functional analysis (detecting deadlock, model-checking) and reasoning about non-functional properties (computing quality-of-service properties). Its declarative nature really distinguishes Reo from other models of concurrency. Using Reo, programmers specify what, when, and why interaction takes place; not how. Indeed, Reo does not feature primitive actions for sending or receiving data elements. Rather, Reo considers interaction protocols as constraints on such actions. In stark contrast to traditional models of concurrency, Reo's constraint-based notion of interaction has the advantage that to formulate (specify, verify, etc.) protocols, one does not need to even consider any of the alternative sequences of actions that give rise to them.
Using Reo, computational threads remain completely oblivious to protocols that compose them into, and coordinate their interactions within, a concurrent application: their code contains no concurrency primitive.
The sole means of communication for a computational thread consists of I/O actions that it performs on its own input/output ports.
To construct an application, one composes a set of such threads together with a protocol by identifying the input/output ports of the computational threads with the appropriate output/input nodes of a Reo connector that implements the protocol. A Reo compiler then generates the proper multi-threaded code for the application.
Figure 2 shows three examples of protocols expressed as Reo connectors: graphs of nodes and arcs, which we refer to as channels. Importantly, communicating parties remain oblivious to how a connector routes data: parties dispatching (fetching) data elements do not know where to (from) these elements go (come).
Figure 2: Example connectors
The connector on the left, called MergerWithBuffer, specifies the same protocol as the one embedded in Figure 1.
Untangled from each other into separate computation and protocol modules, we can study, analyse, and verify the properties of each, independently of the others. We can combine the very same pieces of code that implement a set of producers and consumers with any of the connectors in Figures 2 to obtain different applications that manifest different protocols. We can reuse the same protocols, i.e., the connectors in Figure 2, with very different computational threads in entirely different applications. Reo turns interaction protocols into tangible, explicit, first-class concepts. We can connect the nodes of various instances of these Reo connectors to each other, to obtain connectors that implement more complex protocols. This protocol-level compositionality, a key feature of Reo, supports compositional, scalable construction, verification, analysis, and testing of protocols. Availability of the protocol of an application as an explicit, concrete piece of code enables efficient, dynamic scheduling and resource management.
Our on-going work on generating efficient code from Reo specifications to run on multi-core platforms has shown promising results, revealed interesting challenges, and confirms that the principles of “separation of concerns” and “modularity” apply equally well in the design, construction, verification, analysis, testing, and reuse of scalable protocols.
Link:
http://reo.project.cwi.nl; http://www.cwi.nl/~farhad
References:
[1] Farhad Arbab (2011). Puff, The Magic Protocol. In: Formal Modeling: Actors, Open Systems, Biological Systems, LNCS 7000, pp. 169-206, doi:10.1007/978-3-642-24933-4 9.
[2] Farhad Arbab (2004). Reo: a channel-based coordination model for component composition. MSCS 14(3), pp. 329–366, doi:10.1017/S0960129504004153.
[3] Sung-Shik T.Q. Jongmans & Farhad Arbab (2012): Overview of Thirty Semantic
Formalisms for Reo. SACS 22(1), pp. 201–251, doi:10.7561/SACS.2012.1.201.
Please contact:
Farhad Arbab, Sung-Shik Jongmans
CWI, The Netherlands
Tel: +31 20 592 4056, +31 20 592 4241
E-mail:
{jcomments on}
