Rx-CML: A Prescription for Safely Relaxing Synchrony


One way to ease the burden of concurrent programming is to have threads communicate synchronously via message-passing, making explicit the program points where data is transferred from one thread to another. In a language like Concurrent ML (CML), this philosophy leads to strong guarantees on the ordering and visibility of communicated data, simplifying program reasoning. The cost of synchrony comes with a high price in performance, however, particularly in distributed environments where communication latency is high. To ameliorate these costs, we might allow communication to be asynchronous, having senders buffer data without waiting for the availability of a matching receiver, thereby allowing execution of the sender's continuation to overlap data transmission. However, while the use of asynchrony can help reclaim performance, it also complicates program structure and understanding.

In this paper, we investigate an alternative semantics for CML that implements sends asynchronously, but \emph{guarantees} that the resulting execution nonetheless exhibits behavior observably equivalent to one in which all communication is performed synchronously. Our goal is to retain the expressivity and simplicity of CML's synchronous operations in writing concurrent programs and reasoning about them, but give implementations the flexibility to safely regain performance using asynchronous communication.

We formalize the conditions under which this equivalence holds, and present an implementation that builds a decentralized dependence graph whose structure can be used to check the integrity of an execution with respect to this equivalence. We integrate a notion of speculation to allow ill-formed executions to be rolled-back and re-executed, replacing offending asynchronous actions with safe synchronous ones. Several realistic case studies deployed in a cloud environment demonstrate the utility of our approach.


Code @ github, tech report