Nov 17, 2016

Eduard Kamburjan, Crystal Chang Din, and Tzu-Chun Chen

Session-Based Compositional Analysis for Actor-Based Languages Using Futures

This paper proposes a simple yet concise framework to statically verify communication correctness in a concurrency model using futures. We consider the concurrency model of the core ABS language, which supports actor-style asynchronous communication using futures and cooperative scheduling. We provide a type discipline based on session types, which gives a high-level abstraction for structured interactions. By using it we statically verify if the local implementations comply with the communication correctness. We extend core ABS with sessions and annotations to express scheduling policies based on required communication ordering. The annotation is statically checked against the session automata derived from the session types.

Eduard Kamburjan and Tzu-Chun Chen

Stateful Session Analysis for Actors with Futures

This paper presents a static analysis including a session-based type system using a Points-To analysis for verifying active object languages – object-oriented languages based on the actor paradigm with futures. We specify and verify not only interaction behaviors, but also constraints on object state and data expressed in a first-order formalization of heap memory. A Points-To analysis gives a lightweight analysis on dependency of constraints at different interactions, whose behaviors are checked by a session-based type system. Instead of specifying communication channels, we specify the interplay of futures and method calls on objects. We propose a session-based global specification and establish a local static verification framework to ensure the interacting objects will produce deadlock-free communication traces adhering to our specification.

Please reload


T: (+49) 06151-16-27813