The Java Memory Model

After many years, support for multithreading has been integrated into mainstream programming languages. Inclusion of this feature brings with it a need for a clear and direct explanation of how threads interact through memory. Programmers need to be told, simply and clearly, what might happen when their programs execute. Compiler writers need to be able to work their magic without interfering with the promises that are made to programmers. Java’s original threading specification, its memory model


1 Introduction
1.1 Why Solve This Problem?
1.2 Approach
1.3 Development
2 Building Blocks
2.1 Code is Reordered
2.2 Synchronization and Happens-Before
2.3 Atomicity
2.4 Visibility
2.5 Ordering
2.6 Discussion
3 In Which Some Motivations Are Given
3.1 Guarantees for Correctly Synchronized Programs
3.2 Simple Reordering
3.3 Transformations that Involve Dependencies
3.3.1 Reordering Not Visible to Current Thread
3.4 Synchronization
3.5 Additional Synchronization Issues
3.5.1 Optimizations Based on Happens-Before
3.5.2 Additional Guarantees for Volatiles
3.5.3 Optimizers Must Be Careful
3.6 Infinite Executions, Fairness and Observable Behavior
3.6.1 Control Dependence
4 Causality – Approaching a Java Memory Model
4.1 Sequential Consistency Memory Model
4.2 Happens-Before Memory Model
4.3 Causality
4.3.1 When Actions Can Occur
4.4 Some Things That Are Potentially Surprising about This Memory Model
4.4.1 Isolation
4.4.2 Thread Inlining
5 The Java Memory Model
5.1 Actions and Executions
5.2 Definitions
5.3 Well-Formed Executions
5.4 Causality Requirements for Executions
5.5 Observable Behavior and Nonterminating Executions
5.6 Formalizing Observable Behavior
5.7 Examples
5.7.1 Simple Reordering
5.7.2 Correctly Synchronized Programs
5.7.3 Observable Actions
6 Simulation and Verification
6.1 The Simulator
6.1.1 Simulating Causality
6.1.2 Simulator Performance
6.2 Proofs
6.2.1 Semantics Allows Reordering
6.2.2 Considerations for Programmers
7 Immutable Objects
7.1 Informal Semantics
7.1.1 Complications
7.2 Motivating Examples
7.2.1 A Simple Example
7.2.2 Informal Guarantees for Objects Reachable from Final Fields
7.2.3 Additional Freeze Passing
7.2.4 Reads and Writes of Final Fields in the Same Thread
7.2.5 Guarantees Made by Enclosing Objects
7.3 Full Semantics
7.4 Illustrative Test Cases and Behaviors of Final Field
7.5 Permissible Optimizations
7.5.1 Prohibited Reorderings
7.5.2 Enabled Reorderings
7.6 Implementation on Weak Memory Orders
7.6.1 Weak Processor Architectures
7.6.2 Distributed Shared Memory Based Systems
8 Related Work
8.1 Architectural Memory Models
8.2 Processor Memory Models
8.3 Programming Language Memory Models
8.3.1 Single-Threaded Languages
8.3.2 Multi-Threaded Languages
8.4 Final Fields
9 Future Work
9.1 Performance Testing and Optimization
9.2 Better Programming Model
9.3 Other Programming Languages
10 Conclusion
A Finalization
A.1 Implementing Finalization
A.2 Interaction with the Memory Model

Author: Manson, Jeremy

Source: University of Maryland

Download URL 2: Visit Now

Leave a Comment