Isolates: Serializability Enforcement for Concurrent ML
Lukasz Ziarek, Armand Navabi, Suresh Jagannathan · Purdue e-Pubs (Purdue University System) · 2010
Abstract. There has been much recent interest in exploring higher-level concurrency control abstractions such as software transactional mem-ory (STM) to alleviate the complexity of reasoning about interactions among concurrent threads of control. Isolation and atomicity are the two critical properties provided by an STM that guarantee serializability of concurrent actions. Isolation ensures that transactions execute without interference from effects performed by other transactions, and atomicity guarantees that intermediate effects performed by a transaction are not seen by other concurrently executing transactions. While these properties have been primarily designed with shared mem-ory in mind, there has been recent work (5; 6) that explores how atom-icity could be leveraged to increase the expressivity of message-passing abstractions such as the first-class synchronous events found in Concur-rent ML (CML) (17). Notably, these proposals do not enforce isolation of concurrently executing events, and thus cannot be used to enforce transactional execution of CML programs. In this paper, we consider the introduction of a new event combinator that addresses this signifi-cant limitation. An isolate is a combinator that allows a complex event to execute in isolation with other concurrently executing events (including other isolates). By doing so, it enables the integration of a true transac-tional semantics into a CML-style concurrency model, enabling reasoning about CML programs in terms of serializable event orderings. Incorporat-ing isolation into CML poses a number of challenging problems, however, whose solutions form the focus of this paper. 1