Transcript ppt - University of Utah School of Computing

Analyzing the CRF Java Memory Model
Yue Yang
Ganesh Gopalakrishnan
Gary Lindstrom
School of Computing
University of Utah
Outline
Java Memory Model (JMM) introduction
Why current JMM is broken
Overview of the CRF JMM
Our formal executable model
Analysis results
Introduction of JMM
 Language level support for multi-threading
 Need a memory model (thread semantics) to
specify how threads interact
 Current Java Memory Model (JMM)
•
•
•
•
Chap 17 of Java Language Specification
Thread-local execution engine and working memory
Threads interact via shared main memory
Sets of actions constrained by different rules
Current JMM is broken
Too strong
• Prohibits important compiler optimizations
Too weak
• Object escaping from construction
• No specification for final fields
Example – Object Escape Problem
Initially, p = null
Thread 1
synchronized (this) {
p = new Point(1, 2);
}
Thread 2
if (p != null) {
a = p.x;
}
Finally, can it result in a = 0?
Result: possible under the existing JMM
• Thread 2 is not synchronized  Race Condition
• Some aggressive architecture allows p to be
fetched from a stale cache line
The Bad Consequence
 Immutable objects are not truly immutable
• Changing the field type to “final” does not help
 “/tmp/system” might be read as “/system”
• Serious security hole
 Popular programming patterns are broken
• e.g., double-checked locking algorithm
Challenging JMM Issues
 Maintain safety guarantees
 Support multiple architectures
• JMM designers - identify reasonable requirements
• JVM implementers - ensure compliance
 Cover all related language semantics
• Final / volatile fields, constructors, finalizers, etc.
 Deal with run-time complexities
• Aliasing, dynamic method invocation, etc.
New Replacement Proposals
Bill Pugh’s model
The CRF model
• By Maessen, Shen, and Arvind at MIT
CRF JMM Overview
 CRF stands for Commit / Reconcile / Fence
 Java memory operations are translated into
fine-grained CRF instructions
 Java memory model is specified by CRF
rewrite rules and reordering rules
CRF Instructions
Instruction
Description
Loadl
Load value from local cache
Storel
Store value to local cache
Commit
Ensure write back from cache to memory
Reconcile
Ensure update from memory to cache
Fence
Ensure ordering restrictions
Lock
Acquire a lock
Unlock
Release a lock
Freeze
Complete a final field operation
Java to CRF Translation
Two kinds of memory operations
• Read / Write operations
 Defined based on variable types: Regular / Final / Volatile
• Synchronization operations
 Enter lock / Exit lock / EndCon
Example:
Java Operation
Translation
Write a, v;
Storel a, v;
Commit a;
v = Read a;
Reconcile a;
v = Loadl a;
CRF Rewrite Rules
CRF local rules
• Operational semantics for CRF instructions
• Only affect local cache
CRF background rules
• Synchronize cache and shared memory
CRF Ordering Rules
(Blank entries may be reordered)
Our Formal Executable Model
Inspired by Dill and Park’s work on SPARC
Implemented as Mur rules and functions
Two logical components
• The CRF JMM engine
 Acts as a black box that defines thread semantics
• A test suite
 Each test is designed to reveal a specific property
The CRF JMM Engine
Local rules
• Randomly choose one eligible instruction
 Guarding conditions enforce reordering rules
• Execute it according to the CRF local rules
Background rules
•
•
•
•
Purge (unmap a cache entry)
Cache (update cache from memory)
Write Back (update memory from cache)
Acquire/Release locks
The Test Suite
 Add test cases via Mur Startstates
• Setup thread instructions for each test case
• Java to CRF translation is automated by
Procedure AddInstruction
 Two ways to check results
• Output single violation trace (use Mur invariants)
• Output all interleaving results (use special
completion rules)
Analysis of the CRF JMM
Ordering properties
Constructor properties
Synchronization idioms
Ordering properties of CRF
Ordering Properties
Results
Comparison with Coherence
Coherence is not enforced by CRF
Comparison with PRAM
PRAM is not enforced by CRF
Prescient Store
Allowed only for non-aliased variables
Write Atomicity
Guaranteed by CRF
Causality
Not enforced by CRF
Example: Test of Coherence
Initially, A = 0
Thread 1
Thread 2
A = 1;
A = 2;
X = A;
Y = A;
Finally, can it result in X = 2 & Y = 1?
Result: Yes
• Coherence is not enforced by CRF
Constructor Properties of CRF
(Models the object escape scenario)
Initially, A = B = 0 (A: reference, B: field)
Thread 1
B = 1;
EndCon;
A = 1;
Thread 2
X = A;
Y = B;
Finally, can it result in X = 1 & Y = 0?
 Result: it works only under certain conditions
• Must enforce data dependency for dereference
• EndCon must be ahead of the reference assignment
The Double-Checked Locking Algorithm
public static Helper get() {
if (helper == null) {
synchronized (this) {
if (helper == null)
helper = new Helper();
}
}
return helper;
}
Commonly used for Singleton (created once) objects
Tries to limit locking overhead to the constructing thread
Broken under the current JMM (object escape problem)
Test for Double-Checked Locking
Initially, A = B = 0 (A: reference, B: field)
Thread 1
EnterMonitor;
X = A;
B = 1;
EndCon;
A = 1;
ExitMonitor;
Thread 2
Y = A;
Z = B;
Finally, can it result in X = 0 & Y = 1 & Z = 0?
• Result: test successfully passed
• The presence of EndCon is essential
 A closely related version (without EndCon) would be broken
Usage of Our Framework
 Helpful for understanding JMM
• JMM designers: can use it as a powerful debug tool
• Users: can treat the JMM as a black box
 Gaining extra confidence
• Checking programming idioms
• Checking compiler transformation patterns
• Comparison with conventional models
 A well designed test suite can be served as a
valuable QA benchmark
Discussion - Advantages
Executable model
• See effects of changes immediately
Exhaustive enumeration
• Reveal subtle corner cases
Rigorous specification
• Reduce ambiguities
Discussion - Limitations
State explosion
More complex language features not
supported yet
• Thread creation, termination,
interruption, etc.
Future Directions
JMM implication for compiler optimizations
• Synchronization optimizations
• Dependency Analysis
JMM implication for hardware architectures
Targeting real Java code
• Abstraction / slicing techniques
• Pattern annotation / recognition techniques
Links to Related Resources
JMM discussion group
• http://www.cs.umd.edu/~pugh/java/memoryModel
JMM and Thread Specification Revision
• JSR-133 (http://jcp.org/jsr/detail/133.jsp)
 Our Mur program
• http://www.cs.utah.edu/~yyang/research/crf.m
 Our email: [email protected]
Thank You!