‹Programming› 2018
Mon 9 - Thu 12 April 2018 Nice, France
Thu 12 Apr 2018 14:30 - 15:00 at Baie des Anges A + B - Session 5

Context. TypeState-Oriented Programming (TSOP) is a paradigm intended to help developers in the implementation and use of mutable objects whose public interface depends on their private state. Under this paradigm, well-typed programs are guaranteed to conform with the protocol of the objects they use.

Inquiry. Previous works have investigated TSOP for both sequential and concurrent objects. However, an important difference between the two settings still remains. In a sequential setting, a well-typed program either progresses indefinitely or terminates eventually. In a concurrent setting, protocol conformance is no longer enough to avoid deadlocks, a situation in which the execution of the program halts because two or more objects are involved in mutual dependencies that prevent any further progress.

Approach. In this work, we put forward a refinement of TSOP for concurrent objects guaranteeing that well-typed programs not only conform with the protocol of the objects they use, but are also deadlock free. The key ingredients of the type system are behavioral types, used to specify and enforce object protocols, and dependency relations, used to represent abstract descriptions of the dependencies between objects and detect circularities that might cause deadlocks.

Knowledge. The proposed approach stands out for two features. First, the approach is fully compositional and therefore scalable: the objects of a large program can be type checked in isolation; deadlock freedom of an object composition solely depends on the types of the objects being composed; any modification/refactoring of an object that does not affect its public interface does not affect other objects either. Second, we provide the first deadlock analysis technique for join patterns, a concurrency abstraction with which programmers can express complex synchronizations in a succint and declarative form.

Grounding. We detail the proposed typing discipline for a core programming language blending concurrent objects, asynchronous message passing and join patterns. We prove that the type system is sound and give non-trivial examples of programs that can be successfully analyzed. A Haskell implementation of the type system that demonstrates the feasibility of the approach is publicly available.

Importance. The static analysis technique described in this work can be used to certify programs written in a core language for concurrent TSOP with proven correctness guarantees. This is an essential first step towards the application and integration of the technique in a real-world developer toolchain, making programming of such systems more productive and less frustrating.

Wed 11 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:45 - 15:00
Lisp, Jazz, Aikido – Three Expressions of a Single Essence
Research Papers
Didier Verna EPITA / LRDE
Link to publication DOI
Live Multi-language Development and Runtime Environments
Research Papers
Fabio Niephaus Hasso Plattner Institute, University of Potsdam, Tim Felgentreff Oracle Labs, Potsdam, Tobias Pape HPI, Germany, Robert Hirschfeld HPI, University of Potsdam, Marcel Taeumel Hasso Plattner Institute
Link to publication DOI

Thu 12 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change