Order Types: Static Reasoning about Message Races in Asynchronous Message Passing Concurrency
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.
(AGERE!-2017-Slides-1-3.pdf) | 542KiB |
Mon 23 OctDisplayed 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 30mTalk | 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 30mTalk | Tree Topologies for Causal Message Delivery AGERE Sebastian Blessing Imperial College London, Sylvan Clebsch Imperial College London, Sophia Drossopoulou | ||
11:30 30mTalk | Order Types: Static Reasoning about Message Races in Asynchronous Message Passing Concurrency AGERE File Attached |