TY - GEN
T1 - RCML
T2 - 15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014
AU - Sivaramakrishnan, K. C.
AU - Ziarek, Lukasz
AU - Jagannathan, Suresh
PY - 2014
Y1 - 2014
N2 - A functional programming discipline, combined with abstractions like Concurrent ML (CML)'s first-class synchronous events, offers an attractive programming model for concurrency. In high-latency distributed environments, like the cloud, however, the high communication latencies incurred by synchronous communication can compromise performance. While switching to an explicitly asynchronous communication model may reclaim some of these costs, program structure and understanding also becomes more complex. To ease the challenge of migrating concurrent applications to distributed cloud environments, we have built an extension of the MultiMLton compiler and runtime that implements CML communication asynchronously, but guarantees that the resulting execution is faithful to the synchronous semantics of CML. 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 on the Amazon EC2 cloud infrastructure demonstrate the utility of our approach.
AB - A functional programming discipline, combined with abstractions like Concurrent ML (CML)'s first-class synchronous events, offers an attractive programming model for concurrency. In high-latency distributed environments, like the cloud, however, the high communication latencies incurred by synchronous communication can compromise performance. While switching to an explicitly asynchronous communication model may reclaim some of these costs, program structure and understanding also becomes more complex. To ease the challenge of migrating concurrent applications to distributed cloud environments, we have built an extension of the MultiMLton compiler and runtime that implements CML communication asynchronously, but guarantees that the resulting execution is faithful to the synchronous semantics of CML. 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 on the Amazon EC2 cloud infrastructure demonstrate the utility of our approach.
KW - Axiomatic Semantics
KW - Cloud Computing
KW - Message-passing
KW - Speculative Execution
UR - https://www.scopus.com/pages/publications/84893480524
U2 - 10.1007/978-3-319-04132-2_1
DO - 10.1007/978-3-319-04132-2_1
M3 - Conference contribution
AN - SCOPUS:84893480524
SN - 9783319041315
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 16
BT - Practical Aspects of Declarative Languages - 16th International Symposium, PADL 2014, Proceedings
Y2 - 20 January 2014 through 21 January 2014
ER -