Weak consistency semantics:
Weak consistency semantics
Weak memory models

On library correctness under weak memory consistency
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, Viktor Vafeiadis.
Proc. ACM Program. Lang. 3, POPL, Article 68 (January 2019)
[Paper]
[@ACM]
[More...]

Bridging the gap between programming languages and hardware weak memory models.
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis.
Proc. ACM Program. Lang. 3, POPL, Article 69 (January 2019)
[Paper]
[@ACM]
[@arXiv]
[More...]
 Grounding thinair reads with event structures.
Soham Chakraborty, Viktor Vafeiadis.
Proc. ACM Program. Lang. 3, POPL, Article 70 (January 2019)
[Paper]
[@ACM]
[More...]
 Promising compilation to ARMv8 POP.
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis.
In ECOOP 2017, pp. 22:122:28 (June 2017)
[Paper]
[@LIPIcs]
 Repairing sequential consistency in C/C++11.
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, ChungKil Hur, Derek Dreyer.
In PLDI 2017, pp. 618632. ACM (June 2017)
Distinguished paper award at PLDI'17
[Paper]
[@ACM]
[More...]
 Formalizing the concurrency semantics of an LLVM fragment.
Soham Chakraborty, Viktor Vafeiadis.
In CGO 2017, pp. 100110. ACM (February 2017)
[Paper]
[@ACM]
[More...]

A promising semantics for relaxedmemory concurrency.
Jeehoon Kang, ChungKil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer.
In POPL 2017, pp. 175189. ACM (January 2017)
[Paper]
[@ACM]
[More...]
 Explaining relaxed memory models with program transformations.
Ori Lahav, Viktor Vafeiadis.
In FM 2016. LNCS 9995, pp. 479495. Springer (November 2016)
[Paper]
[@Springer]
[More...]

Validating optimizations of concurrent C/C++ programs.
Soham Chakraborty, Viktor Vafeiadis.
In CGO 2016, pp. 216226. ACM (March 2016)
[Paper]
[@ACM]
[More...]

Taming releaseacquire consistency.
Ori Lahav, Nick Giannarakis, Viktor Vafeiadis.
In POPL 2016, pp. 649662. ACM (January 2016)
[Paper]
[@ACM]
[More...]

Common compiler optimisations are invalid in the C11 memory model and what we can do about it.
Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli.
In POPL 2015, pp. 209220. ACM (January 2015)
[Paper]
[@ACM]
[More...]
Transactional and persistence semantics
 Persistency semantics of the Intelx86 architecture.
Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis.
Proc. ACM Program. Lang. 4, POPL, Article 11 (January 2020)
[Paper]
[@ACM]
[More...]
 Weak persistency semantics from the ground up: Formalising the persistency semantics of ARMv8 and transactional models.
Azalea Raad, John Wickerson, Viktor Vafeiadis.
Proc. ACM Program. Lang. 3, OOPSLA, Article 137 (October 2019)
[Paper]
[@ACM]
[More...]
 On the semantics of snapshot isolation.
Azalea Raad, Ori Lahav, Viktor Vafeiadis.
In VMCAI 2019 (January 2019)
[@arXiv]
[@Springer]
 Persistence semantics for weak memory: Integrating epoch persistency with the TSO memory model.
Azalea Raad, Viktor Vafeiadis.
Proc. ACM Program. Lang. 2, OOPSLA, Article 137 (November 2018)
[Paper]
[@ACM]
[More...]
 On parallel snapshot isolation and release/acquire consistency.
Azalea Raad, Ori Lahav, Viktor Vafeiadis.
In ESOP 2018. LNCS 10801, pp. 940967. Springer (April 2018)
[Paper]
[@Springer]
[More...]
Verification under weak memory consistency
Program logics
 A separation logic for a promising semantics.
Kasper Svendsen, Jean PichonPharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis.
In ESOP 2018. LNCS 10801, pp. 357384. Springer (April 2018)
[Paper]
[@Springer]
[Technical appendix]
[More...]
 Program verification under weak memory consistency using separation logic.
Viktor Vafeiadis.
In CAV (1) 2017. LNCS 10426, pp. 3046. Springer (July 2017)
[Paper]
[@Springer]
 Strong logic for weak memory: Reasoning about releaseacquire consistency in Iris.
JanOliver Kaiser, HoangHai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis.
In ECOOP 2017, pp. 17:117:29 (June 2017)
Best paper award at ECOOP'17
[Paper]
[@LIPIcs]
[More...]
 Tackling reallife relaxed concurrency with FSL++.
Marko Doko, Viktor Vafeiadis.
In ESOP 2017. LNCS 10201, pp. 448475. Springer (April 2017)
[Paper]
[@Springer]
[More...]
 Reasoning about fences and relaxed atomics.
Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira.
In PDP 2016, pp. 520527. IEEE (February 2016)
[Paper]
[@IEEE]
 A program logic for C11 memory fences.
Marko Doko, Viktor Vafeiadis.
In VMCAI 2016, LNCS 9583, pp. 413430. Springer (January 2016)
[Paper]
[@Springer]
[More...]
 OwickiGries reasoning for weak memory models.
Ori Lahav, Viktor Vafeiadis.
In ICALP 2015, Track B. LNCS 9135, pp. 311323. Springer (July 2015)
[Paper]
[@Springer]
[More...]
 Verifying readcopyupdate in a logic for weak memory.
Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis.
In PLDI 2015, pp. 110120, ACM (June 2015)
[Paper]
[@ACM]
[More...]
 Formal reasoning about the C11 weak memory model.
Viktor Vafeiadis.
In CPP 2015, pp. 12. ACM (January 2015)
[Paper]
[@ACM]
[Slides]

GPS: Navigating weak memory with ghosts, protocols, and separation.
Aaron Turon, Viktor Vafeiadis, Derek Dreyer.
In OOPSLA 2014, pp. 691707. ACM (October 2014)
[Paper]
[@ACM]
[More...]
 Relaxed separation logic: A program logic for C11 concurrency.
Viktor Vafeiadis, Chinmay Narayan.
In OOPSLA 2013, pp. 867884. ACM (October 2013)
[Paper]
[@ACM]
[More...]
Automated verification
 HMC: Model checking for hardware memory models.
Michalis Kokologiannakis, Viktor Vafeiadis.
In ASPLOS 2020 (March 2020)
[Paper]

Effective lock handling in stateless model checking.
Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis.
Proc. ACM Program. Lang. 3, OOPSLA, Article 173 (October 2019)
[Paper]
[@ACM]
[More...]
 Model checking for weakly consistent libraries.
Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis.
In PLDI 2019 (June 2019)
[Paper]
[@ACM]
[More...]

Effective stateless model checking for C/C++ concurrency.
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis.
Proc. ACM Program. Lang. 2, POPL, Article 17 (January 2018)
[Paper]
[@ACM]
[More...]
Verification under Sequential consistency
Program logics
 Concurrent separation logic and operational semantics.
Viktor Vafeiadis.
In MFPS 2011. ENTCS 276, pp. 335351. Elsevier (September 2011)
[Paper]
[@Elsevier]
[More...]
 Separation logic in the presence of garbage collection.
ChungKil Hur, Derek Dreyer, Viktor Vafeiadis.
In LICS 2011, pp. 247256. IEEE (June 2011)
[Paper]
[@IEEE]
[Technical appendix]
 Concurrent abstract predicates.
Thomas DinsdaleYoung, Mike Dodds, Philippa Gardner, Matthew Parkinson, Viktor Vafeiadis.
In ECOOP 2010. LNCS 6183, pp. 504528. Springer (June 2010)
[Paper]
[@Springer]
[Technical report]
 RGSep action inference.
Viktor Vafeiadis.
In VMCAI 2010. LNCS 5944, pp. 345361. Springer (January 2010)
[Paper]
[@Springer]
[Tool (Cave)]
 Structuring the verification of heapmanipulating programs.
Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.
In POPL 2010, pp. 261273. ACM (January 2010)
[Paper]
[@ACM]
[Proof scripts]
 Denyguarantee reasoning.
Mike Dodds, Xinyu Feng, Matthew Parkinson, Viktor Vafeiadis.
In ESOP 2009. LNCS 5502, pp. 363377. Springer (March 2009)
[Paper]
[@Springer]
[Technical report]
 A marriage of rely/guarantee and separation logic.
Viktor Vafeiadis, Matthew Parkinson.
In CONCUR 2007. LNCS 4703, pp. 256271. Springer (September 2007)
[Paper]
[@Springer]
[Technical report]
[More...]
 Proving correctness of highlyconcurrent linearisable objects.
Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro.
In PPoPP 2006, pp. 129136. ACM (March 2006)
[Paper]
[@ACM]
[Technical report]
Automated verification
 Rely/guarantee reasoning for asynchronous programs.
Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis.
In CONCUR 2015, pp. 483496 (September 2015)
[Paper]
[@LIPIcs]
 Asynchronous liquid separation types.
Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis.
In ECOOP 2015, pp. 396420 (July 2015)
[Paper]
[@LIPIcs]
[More...]
 Aspectoriented linearizability proofs.
Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.
Logical Methods in Computer Science 11(1:20) (March 2015)
[@LMCS]
 Proving lockfreedom easily and automatically.
Xiao Jia, Wei Li, Viktor Vafeiadis.
In CPP 2015, pp. 119127. ACM (January 2015)
[Paper]
[@ACM]
[More...]
 Aspectoriented linearizability proofs.
Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.
In CONCUR 2013. LNCS 8052, pp. 242256. Springer (August 2013)
[Paper]
[@Springer]
 Automatically proving linearizability.
Viktor Vafeiadis.
In CAV 2010. LNCS 6174, pp. 450464. Springer (July 2010)
[Paper]
[@Springer]
[Technical report]
[Tool (Cave)]
 Biabductive resource invariant synthesis.
Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis.
In APLAS 2009. LNCS 5904, pp. 259274. Springer (December 2009)
[Paper]
[@Springer]
 Proving that nonblocking algorithms don't block.
Alexey Gotsman, Byron Cook, Matthew Parkinson, Viktor Vafeiadis.
In POPL 2009, pp. 1628. ACM (January 2009)
[Paper]
[@ACM]
 Shapevalue abstraction for verifying linearizability.
Viktor Vafeiadis.
In VMCAI 2009. LNCS 5403, pp. 335348. Springer (January 2009)
[Paper]
[@Springer]
[Tool (Cave)]
 Modular safety checking for finegrained concurrency.
Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis.
In SAS 2007. LNCS 4634, pp. 233238. Springer (August 2007)
[Paper]
[@Springer]
[Tool (SmallfootRG)]
Verified compilation
For sequential programs

Lightweight verification of separate compilation.
Jeehoon Kang, Yoonseung Kim, ChungKil Hur, Derek Dreyer, Viktor Vafeiadis.
In POPL 2016, pp. 178190. ACM (January 2016)
[Paper]
[@ACM]
[More...]
 Pilsner: A compositionally verified compiler for a higherorder imperative language.
Georg Neis, ChungKil Hur, JanOliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis.
In ICFP 2015, pp. 166178 (September 2015)
[Paper]
[More...]

A formal C memory model supporting integerpointer casts.
Jeehoon Kang, ChungKil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis.
In PLDI 2015, pp. 326335. ACM (June 2015)
[Paper]
[@ACM]
[More...]
 The marriage of bisimulations and Kripke logical relations.
ChungKil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis.
In POPL 2012, pp. 5972. ACM (January 2012)
[Paper]
[@ACM]
[More...]
 A logical step forward in parametric bisimulations.
ChungKil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
Technical report MPISWS2014003 (January 2014)
[Paper]
[Project page with Coq scripts]
 The transitive composability of relation transition systems.
ChungKil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
Technical report MPISWS2012002 (April 2012)
[Paper]
[Coq scripts]
For concurrent programs
 CompCertTSO: A verified compiler for relaxedmemory concurrency.
Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.
J. ACM. 60(3):22 (June 2013)
[Paper]
[@ACM]
[More...]
 Verifying fence elimination optimisations.
Viktor Vafeiadis, Francesco Zappa Nardelli.
In SAS 2011. LNCS 6887, pp. 146162. Springer (September 2011)
[Paper]
[@Springer]
[More...]
 Relaxedmemory concurrency and verified compilation.
Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.
In POPL 2011, pp. 4354. ACM (January 2011)
[Paper]
[@ACM]
[More...]
Other
Interactive theorem proving (Coq)
 Mtac: A monad for typed tactic programming in Coq.
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
J. Functional Programming 25 (August 2015)
[Paper]
[@CUP]
[More...]
 Mtac: A monad for typed tactic programming in Coq.
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
In ICFP 2013, pp. 87100. ACM (September 2013)
[Paper]
[@ACM]
[Implementation (Mtac)]
 Adjustable references.
Viktor Vafeiadis.
In ITP 2013. LNCS 7998, pp. 328337. Springer (July 2013)
[Paper]
[@Springer]
[More...]
 The power of parameterization in coinductive proof.
ChungKil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
In POPL 2013, pp. 193206. ACM (January 2013)
[Paper]
[@ACM]
[Coq library (Paco)]
Miscellaneous
 GeoReplication: Fast If Possible, Consistent If Necessary.
Valter Balegas, Cheng Li, Mahsa Najafzadeh, Daniel Porto, Allen Clement, Sérgio Duarte, Carla Ferreira, Johannes Gehrke, João Leitão, Nuno M. Preguiça, Rodrigo Rodrigues, Marc Shapiro, Viktor Vafeiadis.
IEEE Data Engineering Bulletin 39(1): 8192 (March 2016)
[@IEEE]
 Modular verification of concurrencyaware linearizability.
Nir Hemed, Noam Rinetzky, Viktor Vafeiadis.
In DISC 2015, pp. 371387 (October 2015)
[Paper]
[@Springer]
 Automating the choices of consistency levels in replicated systems.
Cheng Li, João Leitão, Allen Clement, Nuno Preguiça, Rodrigo Rodrigues, Viktor Vafeiadis
In USENIX ATC 2014, pp. 281292. USENIX (June 2014)
[Paper]
[@USENIX]
 A programming language approach to fault tolerance for forkjoin parallelism.
Mustafa Zengin, Viktor Vafeiadis.
In TASE 2013, pp. 105112. IEEE (July 2013)
[Paper]
[@IEEE]
[More...]
 Finding heapbounds for hardware synthesis.
Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiri Simsa, Satnam Singh, Viktor Vafeiadis.
In FMCAD 2009, pp. 205212. IEEE (November 2009)
[Paper]
[@IEEE]
 Acute: Highlevel programming language design for distributed computation.
Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair AllenWilliams, Pierre Habouzit, Viktor Vafeiadis.
J. Functional Programming 17(45): 547612 (2007)
[Paper]
[@CUP]
[More...]
 Acute: Highlevel programming language design for distributed computation.
Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair AllenWilliams, Pierre Habouzit, Viktor Vafeiadis.
In ICFP 2005, pp. 1526. ACM (September 2005)
[Paper]
[@ACM]
[More...]