Low-level Concurrent Programming . - Michael J. Sullivan

Low-level Concurrent Programming Using theRelaxed Memory CalculusMichael J. SullivanCMU-CS-17-126November 2017School of Computer ScienceCarnegie Mellon UniversityPittsburgh, PA 15213Thesis Committee:Karl Crary, ChairKayvon FatahalianTodd MowryPaul McKenney, IBMSubmitted in partial fulfillment of the requirementsfor the degree of Doctor of Philosophy.Copyright c 2017 Michael J. SullivanThis research was sponsored in part by the Carnegie Mellon University Presidential Fellowship. The views andconclusions contained in this document are those of the author and should not be interpreted as representing theofficial policies, either expressed or implied, of any sponsoring institution, the U.S. government or any other entity.

Keywords: programming languages, compilers, concurrency, memory models, relaxedmemory

AbstractThe Relaxed Memory Calculus (RMC) is a novel approach for portable lowlevel concurrent programming in the presence of the the relaxed memory behaviorcaused by modern hardware architectures and optimizing compilers. RMC takes adeclarative approach to programming with relaxed memory: programmers explicitlyspecify constraints on execution order and on the visibility of writes. This differsfrom other low-level programming language memory models, which—when theyexist—are usually based on ordering annotations attached to synchronization operations and/or explicit memory barriers.In this thesis, we argue that this declarative approach based on explicitprogrammer-specified constraints is a practical approach for implementing low-levelconcurrent algorithms. To this end, we present RMC-C , an extension of C withRMC constraints, and rmc-compiler, an LLVM based compiler for it.

We live on a placid island of ignorance in the midst of black seas of infinity,and it was not meant that we should voyage far.— “The Call of Cthulhu”, H.P. LovecraftAnd all I ask is a tall ship and a star to steer her by;— “Sea Fever”, John Masefieldiv

AcknowledgmentsIt’s difficult to overstate how much thanks is owed to my parents, Jack and Mary Sullivan.They’ve provided nearly three decades of consistent encouragement, support (emotional, moral,logistical, financial, and more), and advice (“Put ‘write thesis proposal’ on your To-Do List, thenwrite the proposal and cross it off!”). I know I wasn’t the easiest kid to raise, but they managedto mostly salvage the situation. Thank you—I wouldn’t be here without you.Thanks to my brother, Joey, who my interactions with over the years have shaped me in moreways than I understand. And I’m very grateful that—at this point in our lives—most of thoseinteractions are now positive.Immeasurable thanks to my advisor, Karl Crary, without whom this never would have happened. Karl is an incredible researcher and it was a pleasure to spend the last six years collaborating with him. Karl also—when I asked him about the CMU 5th Year Masters—was the oneto convince me to apply to Ph.D. programs instead. Whether that is quite worth a “thanks” is ahard question to answer with anything approaching certainty, but I believe it is.I also owe a great debt to Dave Eckhardt. Operating Systems Design and Implementation(15-410) is the best class that I have ever taken and I haven’t been able to get it out of my head.The work I did over seven semesters as one of Dave’s TAs for 410—teaching students aboutconcurrency, operating systems, and, most of all, giving thoughtful and detailed feedback aboutsoftware architecture and design—is the work I am most proud of, and I am supremely thankfulfor being able to be a part of it. While much of my work is likely to take me far afield, I try tocarry a little of the kernel hacker ethic in my heart wherever I go. On top of that, Dave has been aconsistent source of advice, support, and guidance without which I’d never have made it throughgrad school.I owe much to a long string of excellent teachers I had in the Mequon-Thiensville School District, beginning with my third-grade teacher Mrs. Movall, who—in response to me asking if therewas a less tedious way to draw some particular shape in LOGO—arranged for a math teacher tocome over from the high school to teach me about the wonders of variables, if statements, andGOTOs. I owe a particularly large debt to Robin Schlei, who provided years of support, and toKathleen Connelly, who first put me in touch with Mark Stehlik. Thank you!On that note, thanks to Mark Stehlik, who was as good an undergraduate advisor as could beasked for, even if he wouldn’t let me count HOT Compilation as an “applications” class. Andthanks to all the great teachers I had at CMU, especially Bob Harper, who kindled an interest inprogramming languages.Grad school was a long and sometimes painful road, and I’d have never made it throughwithout my hobbies. Chief among them, my regular tabletop role-playing game group, who sacrificed countless Saturday nights to join me in liberating Polonia, exploring the Ironian Wastesfor the Ambrosia Trading Company, and conclusively demonstrating, via their work for the Kromian Mages Guild, that not all wizards are subtle: Rhett Lauffenburger (Roger Kazynski), GabeRouth (Hrothgar Boarbuggerer né Hrunting), Ben Blum (Yolanda Swaggins-Moonflute), MattMaurer (Jack Silver), Michael Arntzenius (Jakub the Half-Giant), and Will Hagen (Daema). AGM couldn’t ask for a better group of players. I’d also like to thank my other major escape: theEVE Online alliance Of Sound Mind, and especially the CEOs who have built SOUND into sucha great group to fly with—XavierVE, June Ting, Ronnie Cordova, and Jacob Matthew Jansen.v

Fly safe!The SCS Musical provided another consistently valuable form of stress in my life, and I’dlike to thank everybody involved in helping to revive it and keep it running. I had allowed myselfto forget about the giant technical-theatre-shaped hole in my heart, and I don’t think I’ll be ableto again.Thanks to the old gang from Homestead—Becki Johnson, Gina Buzzanca, and Michael andAndrew Bartlein. Though we’ve been scattered far and wide from our parents’ basements inWisconsin—and though the Bartleins are rubbish at keeping in touch—you’ve remained some ofmy truest friends.A lot of people provided—in their own ways—important emotional support at different pointsin the process. I owe particular thanks to Jack Ferris, Joshua Keller, Margaret Meyerhofer,Amanda Watson, and Sarah Schultz.Salil Joshi and Joe Tassarotti contributed in important ways to the design of RMC and itscompiler. Ben Segall, Paul Dagnelie, and Rick Benua provided helpful suggestions about benchmarking woes. Paul and Rick also provided useful comments on the draft. Matt Maurer providedsome much needed statistical help. I’d like to thank Shaked Flur et al. for providing me with theARMv8 version of the ppcmem tool, which proved invaluable for exploring the possible behaviors of ARMv8s.A heartfelt thanks to everyone on my committee. Paul McKenney provided early and interesting feedback on this document (and a quote from “Sea Fever”), Kayvon Fatahalian gaveexcellent advice on what he saw as the key arguments of my work, and Todd Mowry helped meunderstand the computer architect’s view of the world a little better.I’ve had a lot of fantastic colleagues during the decade I spent at CMU, both as an undergradand as a grad student. I learned more about computer science and about programming languagesin conversation with my colleagues than I have from any books or papers. Thanks to JoshuaWise, Jacob Potter, Ben Blum, Ben Segall, Glenn Willen, Nathaniel Wesley Filardo, MatthewWright, Elly Fong-Jones, Philip Gianfortoni, Car Bauer, Laura Abbott, Chris Lu, Eric Faust,Andrew Drake, Amanda Watson, Robert Marsh, Jack Ferris, Joshua Keller, Joshua Watzman,Cassandra Sparks, Ryan Pearl, Kelly Hope Harrington, Margaret Meyerhofer, Rick Benua, PaulDagnelie, Michael Arntzenius, Carlo Anguili, Matthew Maurer, Joe Tassarotti, Rob Simmons,Chris Martens, Nico Feltman, Favonia, Danny Gratzer, Stefan Mueller, Anna Gommerstadt, andmany many others.Thanks also to all the wonderful colleagues I had working at Mozilla and Facebook on theRust and Hack programming languages.The most stressful and miserable part of my grad school process was the semester I spentpreparing my thesis proposal. I was nearly burnt out after it and I don’t think I could have kepton going without the ten weeks I spent “Working From Tahoe” (WFT) from The Fairway Housein Lake Tahoe. Thanks to Vail Resorts and everybody who split the ski cabin with me for makingit possible—especially to Jack Ferris and Kelly Hope Harrington for bullying me into it. Andthanks to the Northstar Ski Patrol, the paramedics of the Truckee Fire Protection District, andthe staff at the Tahoe Forest Hospital and the University of Pittsburgh Medical Center for all theexcellent care I received after I skied into a tree.Thanks to Aaron Rodgers and Mike McCarthy, but not to Dom Capers. Go Pack Go!NVIDIA Corporation donated a Jetson TK1 development kit which was used for testingvi

and benchmarking. The IBM Power Systems Academic Initiative team provided access to aPOWER8 machine which was used for testing and benchmarking.To all of the undoubtedly countless people who I really really ought to have thanked here butwho slipped my mind: I’m sorry, and thank you!And last, but certainly not least, I’d like to extend a heartfelt thanks to Phil, Madz, Manny,and all the rest of the gang down at Emarhavil Heavy Industries. Emarhavil Heavy Industries—where there’s always something big just over the horizon.vii

viii

Contents12Introduction1.1 Sequential Consistency . . . . . . . . .1.2 Paradise Lost . . . . . . . . . . . . . .1.2.1 Hardware architecture problems1.2.2 Compiler problems . . . . . . .1.3 Language Memory Models . . . . . . .1.3.1 Java . . . . . . . . . . . . . . .1.3.2 C 11 . . . . . . . . . . . . .1.4 A new approach . . . . . . . . . . . . .The Relaxed Memory Calculus2.1 A Tour of RMC . . . . . . . . . . . . . . . . . . . . . . . .2.1.1 Basics . . . . . . . . . . . . . . . . . . . . . . . . .2.1.2 Concrete syntax: tagging . . . . . . . . . . . . . . .2.1.3 Pre and post edges . . . . . . . . . . . . . . . . . .2.1.4 Transitivity . . . . . . . . . . . . . . . . . . . . . .2.1.5 Pushes . . . . . . . . . . . . . . . . . . . . . . . .2.2 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.2.1 Ring buffers . . . . . . . . . . . . . . . . . . . . . .2.2.2 Using data dependency . . . . . . . . . . . . . . . .2.3 Advanced Features . . . . . . . . . . . . . . . . . . . . . .2.3.1 Non-atomic locations and data races . . . . . . . . .2.3.2 Sequentially consistent locations . . . . . . . . . . .2.3.3 Give and take - fine-grained cross function edges . .2.3.4 LPRE and LPOST - Pre and Post edges to other actions2.4 Model Details . . . . . . . . . . . . . . . . . . . . . . . . .2.4.1 Execution Model . . . . . . . . . . . . . . . . . . .2.4.2 Memory system model . . . . . . . . . . . . . . . .2.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . .2.5.1 Execution vs. visibility . . . . . . . . . . . . . . . .2.5.2 Recursion . . . . . . . . . . . . . . . . . . . . . . 526