[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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.