Yet Another Reo Semantics: Reasoning about Speculative Execution

Speculative execution is a well-known technique that allows for the optimization of concurrent systems. In this talk, we explore an extension to Reo that allows reasoning about speculations, and introduce a semantics based on a logical framework with data types and data streams. Our semantics has the capability to detect and handle inconsistencies, which is important for speculative execution: if a branch prediction was mistaken, an inconsistency is forced that could be resolved by backtracking and reversing computation based on a false speculation. We base our work on a novel typed language for compositions and components. Along the way, we introduce new primitives, alongside traditional Reo primitives: consensus, prophecy, and forcing. We explore the properties of independence, progress, linearity, and causality, arguing why they are fundamental to understand speculative executions.

hosted by