Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada

Asynchronous message passing concurrency with higher level concurrency constructs including activities, asynchronous method invocations and future return values is gaining increased popularity, as an alternative to shared memory concurrency with lower level threads and locks. However, similar to data races in shared memory concurrency, message races in asynchronous message passing concurrency can make a program incorrect and cause bugs that are hard to find and fix. This paper presents order types, a novel type system for static reasoning about message races in asynchronous message passing concurrency. Order types are local, causal and polymorphic types with the following features. First, order types encode both communication and flow behaviors and their happens-before relations. Second, order types are designed for an imperative calculus with concurrent activities, asynchronous method invocations, future return values, wait- by-necessity synchronizations on futures, first-class activities and futures, recursion and dynamic creation of activities. Third, order types are polymorphic and introduce universally qualified type variables to encode unknown values of variables. Fourth, the order type of a module can be inferred modularly using only its implementation and independent of implementations of other modules in the program. Order types complement previous work on static reasoning about races in asynchronous message passing concurrency.

Mon 23 Oct

Displayed time zone: Tijuana, Baja California change

10:30 - 12:00
Session 1: Verification and Language ModelsAGERE at Prince of Wales
Chair(s): Joeri De Koster Vrije Universiteit Brussel, Belgium
10:30
30m
Talk
Sparrow - A DSL for Coordinating Large Groups of Heterogeneous Actors
AGERE
Humberto Rodriguez Avila Vrije Universiteit Brussel, Joeri De Koster Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel
File Attached
11:00
30m
Talk
Tree Topologies for Causal Message Delivery
AGERE
Sebastian Blessing Imperial College London, Sylvan Clebsch Imperial College London, Sophia Drossopoulou
11:30
30m
Talk
Order Types: Static Reasoning about Message Races in Asynchronous Message Passing Concurrency
AGERE
Mehdi Bagherzadeh Oakland University, Hridesh Rajan Iowa State University
File Attached