Tutorials Program -- Sunday, June 6
Please choose one tutorial from the morning (M1 or M2) and one from the afternoon (A1 or A2).
| Morning Session | ||
| 8:30 am - 12:00 pm | M1 | Decision Engines for Software Analysis using Satisfiability Modulo Theories Solvers |
| Leonardo de Moura and Nikolaj Bjørner (Microsoft Research) | ||
| 8:30 am - 12:00 pm | M2 | Semantics of shared variables and synchronization (a.k.a. memory models) |
| Sarita V. Adve (University of Illinois at Urbana-Champaign) and Hans-J. Boehm (HP Labs) | ||
| Afternoon Session | ||
| 1:30 pm - 5:00 pm | A1 | Static and Dynamic Program Analysis using WALA (T.J. Watson Libraries for Analysis) |
| Manu Sridharan and Julian Dolby (IBM T.J. Watson Research Center) | ||
| 1:30 pm - 5:00 pm | A2 | Parallelizing Irregular Applications through the Exploitation of Amorphous Data-Parallelism |
| Keshav Pingali (University of Texas at Austin), Milind Kulkarni (Purdue University), Mario Mendez-Lojo, and Donald Nguyen (University of Texas at Austin) |
Breaks: There will be short breaks with snacks at 10:00 am and 3:00 pm. A continental breakfast will precede the morning session. Lunch is not provided by the conference.
M1: Decision Engines for Software Analysis using Satisfiability Modulo Theories Solvers
Presenters: Leonardo de Moura and Nikolaj Bjørner
Sunday, June 6, 2010. 8:30 AM - 12:00 PM
Theorem proving technologies for checking satisfiability of logical formulas are crucial for many program analysis and verification applications. Of particular recent interest are solvers for Satisfia- bility Modulo Theories (SMT). We will describe how theorem provers, with emphasis on Microsoft’s Z3 solver, are used in program analysis and verification. Several concrete applications from program analysis at Microsoft will be presented. We will also give a brief introduction on the theory and technology behind SMT solvers.
Nikolaj Bjørner is a researcher at Microsoft Research, Redmond, WA. He received his Ph.D. from Stanford University in 1998 where he worked on integrating decision procedures in the context of verifying temporal properties of concurrent programs. He is currently working on making SMT solvers an integral part of program analysis tools at Microsoft.
Leonardo de Moura is a researcher at Microsoft Research, Redmond, WA. He obtained his Ph.D. in Computer Science from PUC-Rio (Brazil) in 2000. From 2001-2006, he was a Computer Scientist at SRI International. He is currently working on SMT solvers and theorem proving technology in general. He was also the main designer of the Yices SMT solver.
M2: Semantics of shared variables and synchronization (a.k.a. memory models)
Presenters: Sarita V. Adve and Hans-J. Boehm
Sunday, June 6, 2010. 8:30 AM - 12:00 PM
For at least three decades we have had programming languages that support threads communicating via shared variables. Unfortunately, a large amount of confusion has surrounded the semantics of those shared variables and associated synchronization mechanisms. The confusion has become visible as widely differing assumptions about the basics of thread programming, software bugs, and conflicting assumptions made by different PLDI research papers.
Recent efforts have resulted in revised language specifications for Java, C++, and C that more carefully address these "memory model" issues. Some hardware specifications have been revised to ensure implementability of these specifications. This tutorial will present an overview of these changes, the issues they addressed and failed to address, and remaining issues that are likely to continue to occupy researchers.
Sarita V. Adve is Professor in Computer Science at the University of Illinois at Urbana-Champaign. Her research interests are in computer architecture, systems, and parallel computing. She co-developed the memory models for Java and C++, which are based on her early work on data-race-free models. She received the ACM SIGARCH Maurice Wilkes award in 2008, was named an Illinois University Scholar in 2004, and received an Alfred P. Sloan Research Fellowship in 1998.
Hans Boehm is perhaps best known as the primary author of a commonly used garbage collection library. That experience convinced him that there was a need to address fundamental shared memory parallel programming issues. He was involved in the revision of the Java memory model, and led the analogous effort for C++. He was awarded the PLDI 2003 most influential paper award and the SIGPLAN 2006 Distinguished Service Award. He is an ACM Distinguished Scientist.
A1: Static and Dynamic Program Analysis using WALA
(T.J. Watson
Libraries for Analysis)
Presenters: Manu Sridharan and Julian Dolby
Sunday, June 6, 2009. 1:30 PM - 5:00 PM
The T. J. Watson Libraries for Analysis (WALA) provide static and dynamic analysis capabilities for Java bytecode and related languages. WALA has been developed over several years at the IBM T.J. Watson Research Center. WALA-based analyses have been presented in over 35 published papers, and WALA has also been incorporated into several IBM products. In 2006, IBM donated WALA to the community under the open source Eclipse Public License. WALA features include bytecode analysis, pointer analyses and call graph construction, an interprocedural dataflow analysis framework, a context-sensitive slicing framework, and a source code analysis framework (currently supporting Java, JavaScript, and X10). For more details, see http://wala.sf.net.
This tutorial will present the design of WALA and show how to best make use of its features. We will present several example programs using WALA that attendees can run themselves and experiment with. Our goal is to provide a helpful introduction to WALA both for those seeking to use existing analyses and for those who want to develop new analyses using the framework.
Manu Sridharan is a Research Staff Member at the IBM Thomas J. Watson Research Center. He has done research on various topics in static analysis, dynamic analysis, and software engineering. His current projects include work on security, pointer analysis, and refactoring for multicores.
Julian Dolby is a Research Staff Member at the IBM Thomas J. Watson Research Center. He has worked in the past on virtual machines and on parallel programming systems, and his current projects include dynamic program analysis and testing focused on Web applications, semantics and ontology reasoning, and static program analysis.
A2: Parallelizing Irregular Applications through the Exploitation of Amorphous Data-Parallelism
Presenters: Keshav
Pingali, Milind Kulkarni, Mario Mendez-Lojo, and Donald Nguyen
Sunday, June 6, 2010. 1:30 PM - 5:00 PM
The goal of this tutorial is to teach attendees how to systematically and effectively parallelize irregular applications for modern multicore systems. Irregular applications use pointer-based data structures like graphs and trees - some important examples are finite-element mesh generators and partitioners, SAT solvers, maxflow algorithms, and event-driven simulation. Until recently, relatively little was known about how to parallelize irregular applications systematically, in spite of their central role in many problem domains.
In this tutorial, we will first present a concept called amorphous data-parallelism (ADP), which captures the patterns of parallelism in irregular applications, and which includes the data-parallelism found in regular algorithms. Second, we will introduce ParaMeter, a tool that automatically extracts and analyzes the available ADP in Java programs. Third, we will demonstrate how to use ParaMeter to investigate parallelism of irregular algorithms. This analysis will show that applications from a broad range of domains exhibit large amounts of ADP and therefore lots of potential for parallelization. Fourth, we will explain how this parallelism can be exploited in a general way on multicore machines. Fifth, we will present several optimization strategies to reduce the overhead of the general parallelization approach, including data partitioning, fast conflict detection, and locality improvement. Attendees will be encouraged to experiment with ParaMeter during the tutorial, and they will receive a free copy for their own use.
For more information, see the ParaMeter tutorial web site.
Keshav Pingali is the W.A. "Tex" Moncrief Chair of Computing in the Department of Computer Science at the University of Texas, Austin. He was on the faculty of the Department of Computer Science at Cornell University from 1986 to 2006, where he held the India Chair of Computer Science. Pingali’s research has focused on programming languages and compiler technology for program understanding, restructuring, and optimization. His group is known for its contributions to memory-hierarchy optimization; some of these have been patented. Algorithms and tools developed by his projects are used in many commercial products such as Intel’s IA-64 compiler, SGI’s MIPSPro compiler, and HP’s PA-RISC compiler. His current research is focused on programming languages and tools for multicore processors. He is a Fellow of the IEEE, Fellow of the American Association for the Advancement of Science, and is the Editor-in-chief of the ACM Transactions on Programming Languages and Systems. He also serves on the NSF CISE Advisory Committee (2009-2011).
Milind Kulkarni is an assistant professor in the School of Electrical and Computer Engineering at Purdue University. Before joining Purdue, he was a postdoctoral research associate at the University of Texas at Austin from May 2008 to August 2009. His research focuses on developing languages, compilers and systems that can be used to effectively parallelize applications for multicore processors. He received his Ph.D. in Computer Science from Cornell University in 2008. Prior to that, he received his M.S. in Computer Science from Cornell University in 2005, and BS degrees in Computer Science and Computer Engineering from North Carolina State University in 2002. While at Cornell, he was a Department of Energy High Performance Computer Science (HPCS) Fellow from 2004 to 2008. He is a member of the ACM and the IEEE Computer Society.
Mario Mendez-Lojo is a post-doctoral researcher working at the University of Texas at Austin, having received his Ph.D. in Computer Science at the University of New Mexico.
Donald Nguyen is a Ph.D. student at the Univeristy of Texas at Austin.
