[ Po polsku ]
There is a growing interest in the design of new programming languages
that combine features such as concurrency (or parallelism) and
possibility of adding
new code during program execution. These features support multi-core
CPUs and dynamic software updating. Example applications are
distributed services that must run "non-stop", e.g.
financial trading, telephone switches, flight reservations, and air
traffic control. Stopping "non-stop" services results in loss of
revenue; it may also compromise safety. The service providers must be
therefore able to repair, update or extend their systems with minimal
service interruption. Dynamically updatable, distributed systems can be
implemented using popular programming languages, that allow software
components to be loaded and bound dynamically. However, in order to
facilitate programming, and be able to guarantee robustness, novel
programming abstractions are needed.
In this book, we design novel language constructs and runtime
algorithms for atomicity, declarative synchronization, and dynamic
protocol update. They can be used to build communicating systems
from modular protocols, that can be replaced dynamically.
-
Atomicity provides guarantees that
a set of operations executed in a network site (machine) can be
regarded as a single unit of computation, regardless of any other
operations occurring concurrently.
-
Declarative synchronization
is the mean to implement control of various concurrent actions or
events in the system, by defining a synchronization policy
(such as atomicity). The policy is defined using a set of rules,
separately from the code of components. This approach allows protocol
components to be reusable in different protocol stacks, and
facilitates dynamic replacement of protocol components.
-
Dynamic protocol update means transparent replacement of
protocols at runtime, so that the use of services implemented by
these protocols is not disrupted. Concurrent, dynamic replacement
of protocol components located on different network sites occurs
under control of switching algorithms.
The book has the following structure:
-
We begin by discussing
motivations and contributions. Then, we describe the versioning
algorithms for concurrency control in atomic tasks.
-
In the following chapter, we design the calculus of atomic tasks,
i.e. atomic, roll-back free transactions that may have I/O effects.
The calculus has a type system for static verification of data
required by dynamic versioning, which guarantees that the constructs
of the calculus are used correctly.
-
Then, we describe two different
approaches to declarative synchronization: (1) the calculus of
concurrency combinators, with type-based verification of combinator
satisfiability (which guarantees that the combinators are used
correctly), and (2) a constraint language for the role-based
synchronization.
-
Next, we describe a model of dynamic protocol update, and give two
example switching algorithms. Finally, we design the class-based
object calculus of dynamic rebinding, and use it to show
the application of synchronization mechanisms described in
this book (ie. atomic tasks and concurrency combinators) when
rebinding concurrent objects.
-
In the appendix, we have included proofs of type soundness for
the calculus of atomic tasks, including the proof of dynamic
correctness of an example versioning algorithm.
A preprint is available in
PDF and
Postscript.
Any comments are very welcome.
Pawel [dot] T [dot] Wojciechowski [at] put.poznan.pl
Last modified: Sat Apr 19 20:10:49 CEST 2008
