Formal Semantics for Expressing Optimism: The Meaning of HOPE~*

摘要

Optimism is a powerful technique for increasing concurrency. A program can increase concurrency by making an optimistic assumption about its future state, and verifying the assumption in parallel with computations based on the optimistic assumption. the use of optimism has been restricted to specialized systems due to the difficulty of writing and understanding optimistic programs. In this paper, we define optimism as any computation that uses rollback. We present a formal semantics for expressing optimism by defining operations for concurrent programs to specify which optimistic computations to roll back, while automating the dependency tracking. We prove that these semantics guarantee some intuitiviely desirable behaviors. Finally, we describe our programming language implementation based on the semantics.