A formal definition of the Eiffel// semantics
has been defined in the structural operational style
of Natural Semantics.
Using the
Centaur system, this semantics permits to generate an
interactive environment for parallel object-oriented programming
and visualization. We provide features such as graphical
representation of objects, visualization of closure and semantic
rules, and animation tools to show the concurrent activities of
objects.
The interest of this approach is to formally introduce parallelism
within the framework of the Eiffel language, and more generally
in object-oriented programming, leading towards
formal transformations and parallelization for object-oriented
languages.
The Eiffel// language (pronounce Eiffel Parallel) defines
an extension of Eiffel which permits reusability and flexibility
in parallel programming.
The Eiffel// language belongs to the category of asynchronous languages
with asynchronous communications. The main objective of this language
is to help the writing of parallel programs thanks to
the following features:
The Eiffel// model uses the following principles:
As an illustration, the following Figure presents an Eiffel// system.
It provides
a parallel version of the sequential class binary_tree, which
describes the management
of a sorted binary tree with two routines insert and search:
each node of the tree has two children ( left
and right), an information ( info) and an associated
key ( key); keys of the left (resp. right) subtree of a node are smaller
(resp. greater) than the key of this node.
To parallelize the binary tree we define the p_binary_tree class.
It inherits from the process class and the binary_tree class;
no other programming is necessary;
Polymorphism between processes (p_bt) and objects
(bt) makes it possible to reuse existing sequential code
(here build_binary_tree for instance).
In that example, the default fifo behavior and the wait-by-necessity
ensure that all insertions are handled in a correct order,
and before the search; the parallel system preserves the semantics
of the sequential one.
We adopt a structural operational semantics for both the
Eiffel language itself, and the concurrent primitives.
More specifically, we use the Natural Semantics
within the Centaur system, and the Typol formalism
which provides us with executable specifications.
This operational semantics simulates parallelism with a non-deterministic
interleaving of (activities of) concurrent objects.
The semantics of inheritance and dynamic binding is
expressed in Natural Semantics (120 rules)
Although, the modules describing the actual execution of statements
(loops, feature calls, assignments, ...)
are expressed in Structural Operational Semantics (200 rules).
We need to define some structures which describe the global
configuration of a system. During execution, an Eiffel// system is composed
of objects. Each object in the system has a configuration (attribute values,
activity, pending requests); the collection of all object configurations
is the configuration of the system. For modeling objects (with their activity)
during execution, we need a structure (based on an abstract syntax).
We also need a structure to store the futures and their values.
We then describe the operational semantics of the language
in terms of a transition system, modeling possible transitions (global actions)
from one configuration to another.
We present rules describing global actions of a
system; these global actions are expressed in terms of local actions
on objects or interactions between objects.
Here are examples of rules expressing global actions:
We present a graphical environment for parallel
object-oriented programming. It provides visual tools to
develop and debug object-oriented programs as well as parallel or concurrent
systems. This environment was derived from a structural operational semantics
of Eiffel//.
The visualization is not obtained from code
instrumentation but automatically, using the semantic description.
The graphical environment focuses on objects and their interactions
(object topology, attribute values, concurrent activities, subsystems,
synchronizations),
provides a set of primitives for controlling and probing
the execution (granularity of interleaving, step-by-step execution,
control over the interleaving), and detects deadlock configurations when they
occur.
Due to non-determinism of concurrency, it is crucial to provide the user
with the possibility to investigate the interleaving space
of all possible executions.
The outcome of such an approach is twofold: (i) a pedagogic environment
to demonstrate concepts of object-oriented programming, actor computation,
and formal semantics; (ii) a step towards environments for the formal study of
parallel object-oriented programming.
Here are examples of typical sessions:
