Fender: Programming with Relaxed Memory Models

To improve performance, virtually all modern processors (e.g. Power, SPARC, Intel, ARM) support relaxed memory models. Unfortunately, programming these relaxed models is difficult and error-prone, yet highly desirable. In this project, we develop powerful automated synthesis and verification techniques which ensure that modern chips are exploited correctly and efficiently. The techniques are based on model checking, abstract interpretation and dynamic analysis.

Project: practicalsynthesis.github.io/

Publications

2018

Automatic Verification of RMA Programs via Abstraction Extrapolation

Cedric Baumann, Andrei Marian Dan, Yuri Meshman, Torsten Hoefler, Martin Vechev

VMCAI 2018

Slides
Paper

2016

Modeling and Analysis of Remote Memory Access Programming

Andrei Dan, Patrick Lam, Torsten Hoefler, Martin Vechev

ACM OOPSLA 2016

Talk
Paper

2015

Effective Abstractions for Verification under Relaxed Memory Models

Andrei Dan, Yuri Meshman, Martin Vechev, Eran Yahav

VMCAI 2015

Slides
Paper

2014

Synthesis of Memory Fences via Refinement Propagation

Yuri Meshman, Andrei Dan, Martin Vechev, Eran Yahav

SAS 2014

Slides
Paper

2013

Predicate Abstraction for Relaxed Memory Models

Andrei Dan, Yuri Meshman, Martin Vechev, Eran Yahav

Static Analysis Symposium (SAS) 2013

Slides
Paper

2012

Dynamic Synthesis for Relaxed Memory Models

Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin Vechev, Eran Yahav

ACM PLDI 2012

Paper

2011

Partial-Coherence Abstractions for Relaxed Memory Models

Michael Kuperstein, Martin Vechev and Eran Yahav

ACM PLDI 2011

Slides
Paper

2010

Automatic Inference of Memory Fences

Michael Kuperstein, Martin Vechev and Eran Yahav

Formal Methods in Computer Aided Design (FMCAD) 2010

Slides
Paper