Transcript Coqa: a Concurrent Programming Model with Ubiquitous Atomicity

Coqa: Concurrent Objects with Quantized Atomicity
Yu David Liu, Xiaoqi Lu, Scott Smith
Johns Hopkins University
April 4, 2008 @ CC’08
Why and What?
• Demand: Multi-Core Programming
– Complex interleaving scenarios need language-level atomicity
support.
– Widespread use of multi-core CPUs needs simple and intuitive
programming abstractions.
• Supply: Coqa
– A correctness-oriented language: all Coqa code ubiquitously
preserves a flavor of atomicity.
• Fewer interleaving scenarios make less error-prone code for programmers.
• Fewer interleaving scenarios allow for new program analysis techniques.
– Additional correctness guarantees:
• no race conditions exist for field access.
• default mutual exclusive object access for threads.
– Deeply embedding concurrency into a familiar Java-like object
model.
Why and What?
• Demand: Multi-Core Programming
– Complex interleaving scenarios need language-level atomicity
support.
– Widespread use of multi-core CPUs needs simple and intuitive
programming abstractions.
• Supply: Coqa
– A correctness-oriented language: all Coqa code ubiquitously
preserves a flavor of atomicity.
• Fewer interleaving scenarios make less error-prone code for programmers.
• Fewer interleaving scenarios allow for new program analysis techniques.
– Additional correctness guarantees:
• no race conditions exist for field access.
• default mutual exclusive object access for threads.
– Deeply embedding concurrency into a familiar Java-like object
model.
Coqa Object Model
A Minimalistic Model with Three Messaging Expressions.
expression
usage
o.m(v)
Intra-task synchronous messaging
o=>m(v)
Subtasking
o->m(v)
Task creation
* Threads in Coqa are called “tasks”.
class Bank{
void transfer (String from, String to, int bal){
L1
Acct afrom = (Acct)htable.get(from);
L2
afrom.withdraw(bal);
L3
Acct ato = (Acct)htable.get(to);
L4
ato.deposit(bal);
}
private HashTable htable = new HashTable();
}
t1
transfer("Alice", "Bob", 300)
t2
transfer(“Cathy”,”Alice”, 500)
htable
L1
L2
t1
Alice
t2
t1
Bob
t1
t2
L1
L2
Time
L3
L3
L4
Cathy
read lock
write lock
t2
L4
Synchronous Messaging and
Atomicity
• Philosophically, Coqa represents an inversion of the
default mode from Java: each and every task (as it is
now) is atomic.
• Stronger than Java’s “synchronized’’ declaration in that
Coqa atomicity is deep.
• With the design as it is, a method might run too long so
that long wait of object release is possible; programs are
prone to deadlocks.
public void openAccount(String n, int bal) {
L5
Acct newAcct= new Acct(n, bal);
L6
htable.put(n, newAcct);
}
t1
t2
htable
transfer("Alice", "Bob", 300);
openAccount(“Dan”, 1000);
t1
t1
Alice
Bob
t2
L5
Time
L6
L6
t1
Dan
Subtasking for More Concurrency
class Bank{
void transfer (String from, String to, int bal){
L1
Acct afrom = (Acct)htable => get(from);
L2
afrom.withdraw(bal);
L3
Acct ato = (Acct)htable => get(to);
L4
ato.deposit(bal);
}
}
t
transfer("Alice",
"Bob", 300);
openAccount(“Dan”, 1000);
1
t2
t3
htable
t3
t2
L1
void openAccount(String n, int bal) {
L5
Acct newAcct = new Acct(n, bal);
L6
htable.put(n.newAcct);
}
L5
Time
L6
Alice
Bob
Dan
Subtasking
• Subtasking captures the high-level intuition of a relatively
independent “subtask” that can independently claim
victory by freeing objects early.
• Subtasking is synchronous.
• Subtasking to Coqa is open nesting to some STM
systems.
• A Coqa subtask can access the objects locked by its
“parent” task.
• Subtasking encourages more concurrency at the
expense of breaking whole-task atomicity.
Quantized Atomicity
• Does a loss of whole-task atomicity imply that no
atomicity property can be preserved?
• A task is a sequence of atomic zones, quanta. Each
quantum consists of a sequence of serializable
execution steps.
…
…
quantum1
…
……
…
…
Equivalent quantum2
quantum
……
quantum2
quantum1
Time
…
……
…
Why Quantized Atomicity?
• It significantly reduces the number of interleavings: an
application is usually composed of few tasks, each with a
very limited number of quanta.
– If two Java threads each have 100 steps of execution, there are
C200100 interleaving scenarios.
– If the two threads are modeled by Coqa tasks, each formed by 3
quanta, there are only C63 = 20 scenarios.
• For next-generation program analysis tool designers:
enumerating all interleavings are now possible.
• For programmers,
– Each quantum is still atomic, so it is easy to understand.
– Across quanta, objects accessed by subtasks might not be
atomically accessed, but mutual exclusive access still holds for
all other objects.
Why Quantized Atomicity?
• It significantly reduces the number of interleavings: an
application is usually composed of few tasks, each with a
very limited number of quanta.
– If two Java threads each have 100 steps of execution, there are
C200100 interleaving scenarios.
– If the two threads are modeled by Coqa tasks, each formed by 3
quanta, there are only C63 = 20 scenarios.
• For next-generation program analysis tool designers:
enumerating all interleavings are now possible.
• For programmers,
– Each quantum is still atomic, so it is easy to understand.
– Across quanta, objects accessed by subtasks might not be
atomically accessed, but mutual exclusive access still holds for
all other objects.
Task Creation
class Bank{
void main(String args[]){
…
bank -> transfer ("Alice", "Bob", 300);
bank -> transfer ("Cathy", "Alice", 500);
}
}
• Tasking creation via asynchronous messaging
• Non-blocking, return immediately
Theoretical Results
• Theorem: Quantized atomicity holds for all Coqa
programs.
– For any execution path, there exists an equivalent quantized
path, i.e. with every quantum serialized.
– Proof technique: moving interleaved execution steps to obtain an
equivalent non-interleaved execution path. [Lipton 75]
• Corollary: Race conditions of fields never happens.
• Corollary: If an object is accessed via synchronous
messaging, then mutual exclusive access to that object
is guaranteed for that task, across quanta.
Implementation: CoqaJava
• A Java extension built using Polyglot. Java core features
are included.
• Benchmark programs
– Contention-intensive: “sliding blocks” puzzle solver.
– Computation-intensive: JavaGrande RayTracer.
• Preliminary optimizations
– Task object pool and immutable fields.
– Manually annotated task-local objects.
• Preliminary Result: 15-60% slower than Java.
On-going Efforts
• Performance improvement
– Inferring task-local objects.
– JVM modifications.
• Toward deadlock freedom
– Coqa, like other lock-based strategies, can lead to deadlocks.
– Subtasking provides a partial solution to alleviate deadlocks.
– New design: a “typed” version of Coqa with regions.
• Object types include information on which task (region) the object belongs to.
• A freed object can be obtained by other tasks by type casting.
Existing Technologies
• Java
– Mutual exclusion is supported. No atomicity support.
– Properties preserved only if programmers declare them.
– Not building concurrency at the core leads to a somewhat
complex memory model.
• Actors
– Minimalistic model with atomicity guarantees.
– Asynchronous messaging: difficult to program.
– Atomicity holds for code blocks typically shorter than Coqa ones.
• Software Transactional Memory (STM) Systems
– No deadlocks, but livelocks are possible.
– No atomicity unless declared. Weak atomicity when transactional
code runs with non-transactional code.
– I/Os (GUIs, networking) can not rollback.
– Coqa could be implemented by replacing locking with rollbacks.
Existing Technologies
• Java
– Mutual exclusion is supported. No atomicity support.
– Properties preserved only if programmers declare them.
– Not building concurrency at the core leads to a somewhat
complex memory model.
• Actors
– Minimalistic model with atomicity guarantees.
– Asynchronous messaging: difficult to program.
– Atomicity holds for code blocks typically shorter than Coqa ones.
• Software Transactional Memory (STM) Systems
– No deadlocks, but livelocks are possible.
– No atomicity unless declared. Weak atomicity when transactional
code runs with non-transactional code.
– I/Os (GUIs, networking) can not rollback.
– Coqa could be implemented by replacing locking with rollbacks.
Existing Technologies
• Java
– Mutual exclusion is supported. No atomicity support.
– Properties preserved only if programmers declare them.
– Not building concurrency at the core leads to a somewhat
complex memory model.
• Actors
– Minimalistic model with atomicity guarantees.
– Asynchronous messaging: difficult to program.
– Atomicity holds for code blocks typically shorter than Coqa ones.
• Software Transactional Memory (STM) Systems
– No deadlocks, but livelocks are possible.
– No atomicity unless declared. Weak atomicity when transactional
code runs with non-transactional code.
– I/Os (GUIs, networking) can not rollback.
– Coqa could be implemented by replacing locking with rollbacks.
Conclusion
• A correctness-oriented model:
– ubiquitous quantized atomicity: both good for programmer
comprehension and for designing new program analysis
techniques.
– automatic mutual exclusion.
– race condition freedom.
• A minimalistic object model very similar to Java.
• End goal: A model toward simple and correct multi-core
programming.
Thank you!