Skip to main content
Open Access Publications from the University of California


UCLA Electronic Theses and Dissertations bannerUCLA

Prove Once, Run Efficiently Anywhere: Tools for Lock-free Concurrent Algorithms


The multi-core revolution has pushed programmers and algorithm designers to build algorithms that leverage concurrency. This notoriously difficult task is futher complicated by the existence of weak architecture and language memory models. The presence of many such memory models has traditionally forced correctness proofs for lock-free concurrent algorithms to be performed on a per-model basis, resulting in a significant duplication of effort. We demonstrate that the correctness of lock-free concurrent algorithms can be proved once for implementations that can be compiled to run correctly and efficiently on all mainstream memory models.

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View