[TYPES/announce] Habil. Thesis: Language Design for Atomicity, Declarative Synchronization, and Dynamic Update

[Pawel.T.Wojciechowski]

Dear TYPES readers,

I would like to announce the forthcoming Habilitation Thesis:

   Language Design for Atomicity, Declarative Synchronization,
   and Dynamic Update in Communicating Systems.

   Pawel T. Wojciechowski

available from http://www.cs.put.poznan.pl/pawelw/book/.
The manuscript is currently under review. The abstract is below.

Comments and feedback would be very welcome.

Pawel

ABSTRACT

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 in 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 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.

Then, we describe two different approaches to declarative synchronization:
the calculus of concurrency combinators, with type-based verification of
combinator satisfiability, and a constraint language for the role-based
synchronization model.

Next, we describe a model of dynamic protocol update, and two example
switching algorithms. Finally, we design the class-based object calculus
of dynamic rebinding.

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.