Speculative N-Way Barriers

damp09.pdf (with Lukasz Ziarek, Suresh Jagannathan, and Umut A. Acar; Accepted to DAMP'09.)
Speculative execution is an important technique that has historically been used to extract concurrency from sequential programs. While techniques to support speculation work well when computations perform relatively simple actions (e.g., reads and writes to known locations), understanding speculation for multi-threaded programs in which threads communicate through shared references is significantly more challenging, and is the focus of this paper.
We use as our reference point a simple higher-order concurrent language based on a synchronous join calculus. Our technique permits the body of a match expression to speculatively proceed before the match has been satisfied, and to have participating threads that would normally block on a pattern speculate past the pattern as well. Our solution formulates safety properties under which speculation is correct, and uses traces to validate these properties.
Formal semantics and proofs

The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.