Memory Models: Enhancing Semantics for Programs with Data Races

Slide Note

This content delves into the importance of establishing stronger memory models to provide better semantics for programs experiencing data races. It highlights the challenges faced due to weak semantics in programming languages like C++ and Java, emphasizing the need for improved memory models to address issues such as null pointer exceptions and data dependence. The discussion explores concepts like Legato, bounded region serializability, weak semantics, and the significance of defining reasonable semantics for programs with data races. Additionally, it addresses the runtime cost versus strength trade-off in end-to-end memory models.

wmcde Follow

Uploaded on Oct 10, 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.

E N D

Presentation Transcript

Legato: Bounded Region Serializability Using Commodity HardwareTransactional Memory Aritra Aritra Sengupta Sengupta Man Cao Michael D. Bond and Milind Kulkarni 1

Programming Language Semantics? Data Races C++ no guarantee of semantics catch-fire semantics Java provides weak semantics 2

Weak Semantics Data data = null; boolean done= false; T2 T2 T1 T1 data = new Data(); done = true; if (done) data.foo(); 3

Weak Semantics Data data = null; boolean done= false; T2 T2 T1 T1 data = new Data(); done = true; if (done) data.foo(); Null Pointer Exception 4

Weak Semantics Data data = null; boolean done= false; T2 T2 T1 T1 data = new Data(); done = true; if (done) data.foo(); Null Pointer Exception No data dependence: Reordering effect 5

Need for Stronger Memory Models The inability to define reasonable semantics for programs with data races is not just a theoretical shortcoming, but a fundamental hole in the foundation of our languages and systems Give better semantics to programs with data races Stronger memory models Adve and Boehm, CACM, 2010 6

End-to-End Memory Models: Run-time cost vs Strength (Unbounded) (Unbounded) Synchronization Synchronization- -free Region Serializability Region Serializability free Run-time cost Bounded Region Bounded Region Serializability Serializability SC SC DRF0 (C++/Java) DRF0 (C++/Java) Strength 7

End-to-End Memory Models: Run-time cost vs Strength (Unbounded) (Unbounded) Synchronization Synchronization- -free Region Serializability Region Serializability free Run-time cost Dynamically Bounded Dynamically Bounded Region Serializability via Region Serializability via EnfoRSer EnfoRSer1 SC SC DRF0 (C++/Java) DRF0 (C++/Java) Strength 1. Sengupta et al. Hybrid Static-Dynamic Analysis for Statically Bounded Region Serializability. ASPLOS, 2015. 8

Dynamically Bounded Region Serializability (DBRS) acq(lock) methodCall() rel(lock) 9

Dynamically Bounded Region Serializability SC+Atomicity of bounded regions1 Eliminates SC violation Eliminates some atomicity violations DRF0 DRF0 Infinite loop Infinite loop Null pointer Null pointer exception exception Corrupt output Corrupt output Infinite Infinite loop Infinite loop Infinite loop Infinite loop Infinite loop Infinite loop Infinite loop Fails validation Fails validation SC SC Correct Correct Correct Correct DBRS DBRS Correct Correct Correct Correct hsqldb6 hsqldb6 sunflow9 sunflow9 jbb2000 jbb2000 jbb2000 jbb2000 sor sor lufact lufact moldyn moldyn raytracer raytracer Corrupt output Corrupt output Correct Correct Correct Correct Correct Correct Correct Correct Fails validation Fails validation Correct Correct Correct Correct Correct Correct Correct Correct Correct Correct Correct Correct loop 1. Sengupta et al. Hybrid Static-Dynamic Analysis for Statically Bounded Region Serializability. ASPLOS, 2015. 10

EnfoRSer Benchmarks: DaCapo 2006, 2009 and SPECjbb benchmarks 400 350 % Overhead over unmodified JVM % Overhead over unmodified JVM 300 Intel Xeon with TSX. A 14-core processor 250 200 150 100 50 0 1. Sengupta et al. Hybrid Static-Dynamic Analysis for Statically Bounded Region Serializability. ASPLOS, 2015. 11

End-to-End Memory Models: Run-time cost vs Strength (Unbounded) (Unbounded) Synchronization Synchronization- -free Region Serializability Region Serializability free Run-time cost Dynamically Bounded Dynamically Bounded Region Serializability via Region Serializability via EnfoRSer EnfoRSer SC SC This work: HTM-based dynamically bounded region serializability DRF0 (C++/Java) DRF0 (C++/Java) Strength 12

Outline Challenges Na ve implementation with hardware transactional memory Limitations of using HTM for DBRS Approach Overcoming limitations Our approach to DBRS enforcement: Legato Legato Evaluation 13

Enforcing DBRS with Commodity Hardware Transactional Memory (HTM) Transaction start Transaction End

Enforcing DBRS with Commodity Hardware Transactional Memory (HTM) Transaction Start Transaction End Transaction Start Transaction End

Enforcing DBRS with Commodity Hardware Transactional Memory (HTM) Transaction Start Transaction End Transaction Start Transaction End

EnfoRSer HTM: 1 DBR per-trans 400 350 % Overhead over unmodified JVM % Overhead over unmodified JVM 300 250 200 175 150 100 40 50 0 17

EnfoRSer HTM: 1 DBR per-trans 400 High cost of TSX instructions Start/End three atomic operations!2 350 % Overhead over unmodified JVM % Overhead over unmodified JVM 300 250 200 175 150 100 40 50 0 18 2. Yoo et al. Performance Evaluation of Intel TSX for High-Performance Computing, SC 2013

Legato: Key Idea Merge several regions into a single transaction: amortize the cost of starting and stopping a transaction 19

Legato: Key Idea Transaction Start Transaction End Transaction Start Transaction End 20

Legato: Key Idea Transaction Start Transaction Merge 21

Legato: Key Idea Transaction Merge Transaction Start Transaction Merge 22

Legato: Key Idea Transaction End Transaction Start Transaction Merge Transaction Merge 23

Challenges Conflicts Conflicts abort transactions: wasted work Capacity Capacity aborts: larger transactions have larger footprint unknown unknown a priori a priori HTM HTM- -unfriendly operations unfriendly operations: hardware interrupts, page faults etc. larger footprint, 24

Per-transaction cost vs Abort cost Transaction Abort Transaction Merge Transaction Start Transaction Merge

Per-transaction cost vs Abort cost Transient cause: conflicts, hardware interrupts => Retry transaction Capacity abort: end before culprit region => Start new transaction Transaction Abort Transaction Merge Transaction Start Transaction Merge

Per-transaction cost vs Abort cost Transaction Abort Transaction Merge Transaction Start Transaction Merge

Per-transaction cost vs Abort cost Transient cause: conflicts, hardware interrupts => Retry transaction Capacity abort: end before culprit region => Start new transaction Transaction End Transaction Merge Transaction Start Transaction Merge

Per-transaction cost vs Abort cost Transient cause: conflicts, hardware interrupts => Retry transaction Capacity abort: end before culprit region => Start new transaction Transaction Start Transaction End

Per-transaction cost vs Abort cost Transient cause: conflicts, hardware interrupts => Retry transaction Unknown abort location Capacity abort: end before culprit region => Start new transaction Transaction Abort

Per-transaction cost vs Abort cost Transient cause: conflicts, hardware interrupts => Retry transaction Capacity abort: end before culprit region => Start new transaction Transaction End

Per-transaction cost vs Abort cost Transient cause: conflicts, hardware interrupts => Retry transaction Capacity abort: end before culprit region => Start new transaction Minimal Learning Transaction End Future transaction behavior unknown

Legato: Our Approach Decide on a merge target: use history history of previous transaction 1. Temporary target . Temporary target changes rapidly: rapidly: capture transient effects 2. Setpoint Setpoint or steady state program phases steady state target changes slowly slowly: capture 33

Curr Curr Target: 8 Target: 8 Setpoint Setpoint: 8 Merging Algorithm : 8 34

Curr Curr Target: 8 Target: 8 Setpoint Setpoint: 8 Merging Algorithm: Initial Phase : 8 Transaction Start 35

Curr Curr Target: 8 Target: 8 Setpoint Setpoint: 8 Merging Algorithm: Initial Phase : 8 Transaction Merge 36

Curr Curr Target: 8 Target: 8 Setpoint Setpoint: 8 Merging Algorithm: Initial Phase : 8 Transaction Merge 37

Merging Algorithm: Recover from Transient Error Curr Curr Target: Target: 8/2 = 4 Setpoint Setpoint: 8 : 8 8/2 = 4 Rapid action: Rapid action: 38

Merging Algorithm: Recover from Transient Error Curr Curr Target: 4 Target: 4 Setpoint Setpoint: 8 : 8 Transaction Start 39

Merging Algorithm: Recover from Transient Error Curr Curr Target: 4 Target: 4 Setpoint Setpoint: 8 : 8 Transaction Merge 40

Merging Algorithm: Recover from Transient Error Curr Curr Target: Target: 4/2 = 2 Setpoint Setpoint: 8 : 8 4/2 = 2 41

Merging Algorithm: Recover from Transient Error Curr Curr Target: 2 Target: 2 Setpoint Setpoint: 8 : 8 Transaction Start 42

Merging Algorithm: Recover from Transient Error Curr Curr Target: Target: 2 2 Setpoint Setpoint: 8 : 8 No Action: No Action: Skeptical Skeptical Transaction End 43

Merging Algorithm: Build up to Setpoint Curr Curr Target: Target: 2*2 = 4 Setpoint Setpoint: 8 : 8 2*2 = 4 Transaction End 44

Merging Algorithm: Build up to Setpoint Curr Curr Target: Target: 4*2 = 8 Setpoint Setpoint: 8 : 8 4*2 = 8 Aggressive Aggressive Transaction End 45

Merging Algorithm: Change of Program Phase Curr Curr Target: Target: 9 9 Setpoint Setpoint: : 8 + 1 = 9 8 + 1 = 9 Transaction End 46

Merging Algorithm: Change of Program Phase Curr Curr Target: Target: 9 9 Setpoint Setpoint: : 8 + 1 = 9 8 + 1 = 9 Transaction End Enter a Enter a low => => more aggressive merging low- -conflict program phase conflict program phase 47