Research
Relaxed Memory Semantics
Modern processors and compilers reorder memory operations for performance, breaking the intuition of a single, sequentially consistent memory. My work verifies concurrent algorithms against the weak memory models that result, establishing that they remain correct under the relaxed orderings these models permit.