Memory Model Safety of Programs Research

Explore the challenges and vulnerabilities in memory models of programs, emphasizing the importance of maintaining strict locking discipline for performance-critical code. The research discusses issues with relaxed memory models on multicore machines and provides examples of memory model vulnerabilities in C# and C code. It also delves into the concept of memory model safety and the goal of efficiently verifying it for programs.

• Memory Model Safety
• Program Vulnerabilities
• Multicore Machines
• Memory Model Verification
• Memory Model Research

juju_206 Follow

Uploaded on Oct 08, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Memory Model Safety of Programs Sebastian Burckhardt Madanlal Musuvathi Microsoft Research EC^2, July 7, 2008

2. Motivation: Memory Model Vulnerabilities Programmers do not always follow strict locking discipline in performance-critical code Ad-hoc synchronization with normal loads and stores or interlocked operations is faster Such code can break on relaxed memory models Most multicore machines are not sequentially consistent Both compilers and actual hardware can contribute to effect (we focus on hardware effects here) Vulnerabilities are hard to find, reproduce, and analyze May require specific hardware configuration and schedule 2

3. C# Example (found in production-level code) volatile bool isIdling; volatile bool hasWork; //Consumer thread void BlockOnIdle(){ lock (condVariable){ isIdling = true; if (!hasWork) Monitor.Wait(condVariable); isIdling = false; } } //Producer thread void NotifyPotentialWork(){ hasWork = true; if (isIdling) lock (condVariable) { Monitor.Pulse(condVariable); } } 3

4. Example: Store Buffer Vulnerability Key pieces of code on previous slide: volatile int ii = 0; volatile int hw = 0; Consumer Producer Store ii, 1 Store ii, 1 Load hw, 0 Store hw, 1 Load ii, 1 0 On x86, hardware may perform store late Bug: Producer thread does not notice waiting Consumer, does not send signal 4

5. Abstract View of Memory Models Given a program P, a memory model Y defines the subset TP,Y T of traces corresponding to some (partial or complete) execution of P on Y. T TP, SC TP, Y SC (sequential consistency) Is strongest memory model More executions may be possible on a relaxed memory model Y 5 5

6. Memory Model Safety Observation: Programmer writes code for SC Resorts to {fences, volatiles, interlocked operations} to maintain SC behavior where needed If program P exhibits non-SC behavior, it is most likely a bug Definition: A program P is Y-safe if TP,SC = TP,Y 6

7. Goal & Position Goal: Find efficient methods to verify / falsify memory model safety of programs. Position: Memory models should be formulated in a manner that facilitates this goal. It helps if a memory model Y guarantees that data-race-free programs are Y-safe (but what about racy ones?) guarantees borderline executions (to be defined next). 7

8. Borderline Executions Def.: A borderline execution for P, Y is an execution in TP,SC with a successor in TP,Y - TP,SC TP,SC TP,Y Successor traces are traces with one more instruction. 8

9. Example: TSO Borderline Execution TP, SC 1.1 Store ii, 1 2.1 Store hw, 1 TP, TSO 1.2 Load hw, 0 1.1 Store ii, 1 2.1 Store hw, 1 1.2 Load hw, 0 2.2 Load ii, 1 1.1 Store ii, 1 2.1 Store hw, 1 1.2 Load hw, 0 2.2 Load ii, 0 Successor traces are traces with one more instruction. 9

10. Borderline Executions Def.: A borderline execution for P, Y is an execution in TP,SC with a successor in TP,Y - TP,SC TP,SC TP,Y Def.: A memory model Y guarantees borderline executions if the following property is true: A program P is Y-safe if and only if it has no borderline executions. 10

11. Borderline Executions Def.: A borderline execution for P, Y is an execution in TP,SC with a successor in TP,Y - TP,SC We can verify / falsify this as a safety property of sequentially consistent executions! TP,SC TP,Y Def.: A memory model Y guarantees borderline executions if the following property is true: A program P is Y-safe if and only if it has no borderline executions. 11

12. When does a Memory Model Guarantee Borderline Executions? Simplest case: If each trace TP,Y has a predecessor in TP,Y , we can use simple induction (because empty trace is in TP,SC ). TP,Y TP,SC This is true for TSO, and we show in [CAV08] paper how to exploit this to build a borderline monitor. 12

13. How May a Memory Model Fail to Guarantee Borderline Executions? Sometimes, traces have no predecessors (i.e. we can not take away any one instruction). // Thread 1 if (y = 1) if (x = 1) x = 1; y = 1; // Thread 2 Example program: some memory models may allow this circular trace: Load y, 1 Load x, 1 Store x, 1 Store y, 1 13

14. Conclusions / Future Work With increasing use of multicores and little programmer regard for race-freedom, we expect more programs to exhibit failures caused by the memory model. Borderline executions provide a practical way to verify / falsify memory model safety for a general class of memory models Future work: how to deal with Memory models without borderline executions Memory models defined by compiler optimizations 14