|
FLoC
MEETINGS
PROGRAM
FACILITIES
SEATTLE
ORGANIZATION
MISCELLANEOUS
OUT-OF-DATE
|
TV on Tuesday, August 22nd
| 08:30‑09:00 |
Lisa Higham (The University of Calgary)
LillAnne Jackson (University of Victoria, The University of Calgary)
Jalal Kawash (American University of Sharjah, The University of Clagary)
What is Itanium Memory Consistency from the Programmers Point of View?
A programmer-centric model describes the memory consistency rules as a collection, one for each processor, of ‘views’
of instructions and some agreements between these views. It also requires the natural notion of validity: the value
read from a shared memory location is the one that was most recently stored, according to a given view. This allows
reasoning about programs at a non-operational level in the natural way, not obscured by the implementation details of
the underlying architecture. In this paper, we formulate a programmer-centric description of the memory consistency
model provided by the Itanium architecture. However, our definition is not tight. We provide two very similar definitions
and prove that the specification of the Itanium memory model lies between the two. These two definitions are
motivated by slightly different implementations of load-acquire instructions. A further entertainment of a handful of
other load-acquire rules leads us to question whether the specification of the Itanium memory order [6] is indeed faithful
to the Itanium architecture intentions.
|
| 09:00‑09:30 |
Jan-Willem Maessen
(Sun Microsystems Laboratories)
Arvind Arvind
(MIT CSAIL)
Store Atomicity for Transactional Memory
We extend the notion of Store Atomicity to a
system with atomic transactional memory. This gives a fine-grained
graph-based framework for defining and reasoning about transactional
memory consistency. The memory model is defined in terms of
thread-local Instruction Reordering axioms and Store
Atomicity, which describes inter-thread communication via memory. A
memory model with Store Atomicity is serializable: there is a unique
global interleaving of all operations which respects the reordering
rules and serializes all the operations in a transaction together. We
extend Store Atomicity to capture this ordering requirement by
requiring dependencies which cross a transaction boundary to point in
to the initiating instruction or out from the committing instruction.
We sketch a weaker definition of transactional serialization which
accounts for the ability to interleave transactional operations which
touch disjoint memory. We give a procedure for enumerating the
behaviors of a transactional program---noting that a safe enumeration
procedure permits only one transaction to read from memory at a time.
We show that more realistic models of transactional execution require
speculative execution. We define the conditions under which
speculation must be rolled back, and give criteria to identify which
instructions must be rolled back in these cases.
|
| 11:00‑11:15 |
Jeff Napper (The University of Texas at Austin)
Lorenzo Alvisi (The University of Texas at Austin)
Robust Multithreaded Applications
Currently, MT applications are only as robust as the weakest
thread---if a single thread fails, the entire application must
restart. We explore very lightweight application-aware MT recovery
policies where fault containment encompasses only single threads
rather than the entire process, which we call thread-fault
tolerance. Robust MT applications retain the advantages of shared data
among threads such as simple programming and fast context switches
without losing the advantage of failure independence. Further,
threads can be intentionally cancelled at any time, allowing
fine-grained bounds on resource usage. For example, threads may be
leased resources (such as CPU cycles) to prevent leaks or to mitigate
the damage of erroneous threads (such as malware). To create robust MT
applications, we design and build 1) a lock-free transactional
interface to shared objects to provide progress guarantees when
threads fail while accessing shared data, 2) lock-free garbage
collection of user-level thread resources such as stack space and
shared objects to recover resources from dead threads, and 3)
mechanisms to manage the lifecycle of threads---a fault notification
mechanism tracking thread failures and routines to cancel threads.
|
| 11:15‑11:30 |
John Regehr
(University of Utah)
Thread Verification vs. Interrupt Verification
Interrupts are superficially similar to threads, but there are subtle
semantic differences between the two abstractions. This paper compares and contrasts threads and interrupts from the point of view of verifying the absence of race conditions. We identify a small set of extensions that permit thread verification tools to also verify interrupt-driven software, and we present examples of source-to-source transformations that turn interrupt-driven code into semantically equivalent thread-based code that can be checked by a thread verifier.
|
| 11:30‑11:45 |
Muhammad Umar Janjua (Computer Laboratory, Cambridge University,UK)
Alan Mycroft (Computer Laboratory, Cambridge University, UK)
Automatic Correcting transformations for Safety property violations
Our goal is an automatic, compile-time and incremental technique to compute source-level corrections to safety property violations in a program. For a program P containing a set of violating traces V with respect to a user-given safety property, our method incrementally transforms P into a new program P' such that P' no longer contains the same behaviour as in V. While making these series of "Correcting Transformations", we ensure that firstly, previous correct behaviours in the erroneous program are preserved in the corrected program, and secondly, no new erroneous behaviours are introduced.
In this paper, we address those safety property violations resulting from incorrect interleavings of threads in the program. We analyse partial program computation tree and insert thread blocking primitives in the program in such a way that only erroneous program paths are pruned.
|
| 11:45‑12:00 |
Yosi Ben Asher (University of Haifa)
Yaniv Eytani (UIUC)
Eitan Farchi (IBM HRL)
Shmuel Ur (IBM HRL)
Noise Makers Need to Know Where to be Silent – Producing Schedules that Find Bugs
A noise maker is a tool that seeds a concurrent program with conditional synchronization primitives (such as yield()) for the purpose of increasing the likelihood that a bug manifest itself. This work explores the theory and practice of choosing where in the program to induce such thread switches at runtime. We introduce a novel fault model that classifies locations as “good”, “neutral”, or “bad,” based on the effect of a thread switch at the location. Using the model we explore the terms in which efficient search for real-life concurrent bugs can be carried out. We accordingly justify the use of probabilistic algorithms for this search and gain a deeper insight of the work done so far on noise-making. We validate our approach by experimenting with a set of programs taken from publicly available multi-threaded benchmark. Our empirical evidence demonstrates that real-life behavior is similar to one derived from the model.
|
| 12:00‑12:30 |
Shmuel Ur (IBM HRL)
Shady Copty (IBM Haifa Reserach Lab)
Toward Automatic Concurrent Debugging Via Minimal Program Mutant Generation with AspectJ
Debugging is one of the most time-consuming activities in program design. Work on automatic debugging has received a great deal of attention and there are a number of symposiums dedicated to this field. Automatic debugging is usually invoked when a test fails in one situation, but succeeds in another. For example, a test fails in one version of the program (or scheduler), but succeeds in another. Automatic debugging searches for the smallest difference that causes the failure. This is very useful when working to identify and fix the root cause of the bug.
A new testing method instruments concurrent programs with schedule-modifying instructions to reveal
concurrent bugs. This method is designed to increase the probability of concurrent bugs (such as races, deadlocks) appearing. This paper discusses
integrating this new testing technology with automatic debugging. Instead of just showing thata bug exists, we can pinpoint its location by finding the minimal set of instrumentations that reveal the bug.
In addition to explaining a methodology for this integration, we show an AspectJ-based implementation. We discuss the implementation in detail as it both demonstrates the advantage of the adaptability of open source tools
and how our specific change can be used for other testing tools.
|
|
|
