Kala: An Efficient and Scalable Time Travel Infrastructure for Concurrent Systems Suresh Jagananthan
The notion of time travel, the ability of an implementation to revert a concurrent computation to an alternative feasible global state is investigated. Recent work on software transactions or speculative execution provide a constrained form of time-travel: when a transaction aborts due to a serializability violation, the transaction's effects are reverted. Similarly, the effects of a speculative thread can be undone if data dependency violations are detected. However, the policies that dictate when a transaction or a speculative action must abort, and where computation resumes, are very rigid, are not specified by the programmer, and often over-constrained.
The broader ramifications of time travel and revocation on programming language design and specification, compiler analysis, and runtime implementation is the focus of this research. Effective support for time travel can enable a number of new programming abstractions for concurrent programming. This research entails the development of abstractions that revert computation based on programmer-specified invariants, specification techniques that define relations among program states used to guide revocation strategies, static analyses that identify equivalences among states, and compiler and runtime structures to enable efficient reversion of control and state.
