IBM Research welcomes members of the research community to our seminars. To ensure compliance with IBM security guidelines, we request you to contact the seminar host in advance. When you arrive at the Research lab, please provide the host's name to the receptionist.
| A Taste of Erlang | ||||
| Bard Bloom | On: | 21-May-2008 10:00 AM - 11:30 AM | ||
| IBM Research | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
Abstract: Sequentially, Erlang is a simple functional language of concrete data structures and pattern matching, not far from pure Scheme. With a few distributed constructs and a few good libraries, it's a slick and powerful tool for reliable distributed computing. It's getting popular: major companies are starting to use it for high-performance message services. Come see what it's about. | ||||
| Declarative Object Identity Using Relation Types | ||||
| Mandana Vaziri | On: | 27-May-2008 10:00 AM - 11:30 AM | ||
| IBM Research | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
Abstract: This talk is based on an ECOOP'07 paper by Mandana Vaziri, Frank Tip, Stephen Fink, and Julian Dolby. Object-oriented languages define the identity of an object to be an address-based object identifier. The programmer may customize the notion of object identity by overriding the equals() and hashCode() methods following a specified contract. This customization often introduces latent errors, since the contract is unenforced and at times impossible to satisfy, and its implementation requires tedious and error-prone boilerplate code. Relation types are a programming model in which object identity is defined declaratively, obviating the need for equals() and hashCode() methods. This entails a stricter contract: identity never changes during an execution. We formalize the model as an adaptation of Featherweight Java, and implement it by extending Java with relation types. Experiments on a set of Java programs show that the majority of classes that override equals() can be refactored into relation types, and that most of the remainder are buggy or fragile. | ||||
| Online Phase-Adaptive Data Layout Selection | ||||
| Martin Hirzel | On: | 1-Jul-2008 10:00 AM - 11:30 AM | ||
| IBM Research | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
Abstract: This talk is based on an ECOOP'08 paper by Chengliang Zhang and Martin Hirzel. Good data layouts improve cache and TLB performance of object-oriented software, but unfortunately, selecting an optimal data layout a priori is NP-hard. This talk introduces layout auditing, a technique that selects the best among a set of layouts online (while the program is running). Layout auditing randomly applies different layouts over time and observes their performance. As it becomes confident about which layout performs best, it selects that layout with higher probability. But if a phase shift causes a different layout to perform better, layout auditing learns the new best layout. We implemented our technique in a product Java virtual machine, using copying generational garbage collection to produce different layouts, and tested it on 20 long-running benchmarks and 4 hardware platforms. Given any combination of benchmark and platform, layout auditing consistently performs close to the best layout for that combination, without requiring offline training. | ||||
| Liquid Metal: Object-Oriented Programming Across the Hardware/Software Boundary | ||||
| Rodric Rabbah | On: | 15-Jul-2008 10:00 AM - 11:30 AM | ||
| IBM Research | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
Abstract: The paradigm shift in processor design from monolithic processors to multicore has renewed interest in programming models that facilitate parallelism. While multicores are here today, the future is likely to witness architectures that use reconfigurable fabrics (FPGAs) as coprocessors. FPGAs provide an unmatched ability to tailor their circuitry per application, leading to better performance at lower power. Unfortunately, the skills required to program FPGAs are beyond the expertise of skilled software programmers. This paper shows how to bridge the gap between programming software vs. hardware. We introduce Lime, a new Object-Oriented language that can be compiled for the JVM or into a synthesizable hardware description language. Lime extends Java with features that provide a way to carry OO concepts into efficient hardware. We detail an end-to-end system from the language down to hardware synthesis and demonstrate a Lime program running on both a conventional processor and in an FPGA. | ||||
Past seminars
| Fortran Development Tools: Providing a RoadMap for Application Development on Advanced Computer Architectures | ||||
| Dr. Craig E. Rasmussen | On: | 8-May-2008 10:00 AM - 11:30 AM | ||
| Los Alamos National Labs | At: | Watson Research Center (Hawthorne), Room GNF15 | ||
| Host: | Greg Watson | |||
Abstract: The Fortran Development Tools (FDT) project is dedicated to delivering productivity enhancing and program correctness tools to the scientific application developer. The FDT project also provides an important vehicle for source-to-source transformations, enabling research in the mapping of high-level language constructs on to advanced computer architectures like RoadRunner. The goal of this research is to allow the programmer to "write once," while relying on the source-to-source compiler to target the disparate variety of computer architectures that are available today. We describe initial results from this auto-vectorizing and auto-parallelizing, "data-parallel" Fortran compiler showing a factor of ten speedup on the IBM Cell/B.E. processor. Speaker biography: Craig E Rasmussen, Ph.D, is a staff member of the Advanced Computing Laboratory (ACL) at Los Alamos National Laboratory. He has an extensive publication record in space plasma physics, medical physics, and computational and computer sciences. His current research interests include studying ways in which computer languages and programming environments can improve productivity in scientific computing. As a member of the Common Component Architecture (CCA) forum, he has worked to make component technology easier to use by developing the Dune CCA/Python framework and experimenting with it as a rapid prototyping environment for scientific computing. As a member of the J3 Fortran standards body, he has worked on the Fortran Bind(C) interoperability standard and on other ways to improve the parallel expressiveness and performance of the Fortran language. At the University of Michigan, Craig was lead programmer on the Upper Atmospheric Research Collaboratory (UARC), which enabled scientists to view, steer, and collaborate remotely over data gathered in real time from instruments located at Sondrestrom, Greenland. The UARC project was inducted into the Smithsonian Institution's Permanent Research Collection on Information Technology Innovation. He is currently working on a source-to-source compiler for Fortran 2003. | ||||
| Fighting concurrency bugs | ||||
| Shan Lu | On: | 30-Apr-2008 10:00 AM - 11:30 AM | ||
| University of Illinois, Urbana-Champagne | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
| Host: | Evelyn Duesterwald | |||
Abstract: Driven by the hardware shift to multi-core architectures, concurrency is being brought into mainstream software development. Unfortunately, concurrent programs are prone to concurrency bugs, because of the inherent complexity of concurrency and the sequential thinking habits of programmers. Concurrency bugs' non-deterministic property also brings a lot of trouble to developers. Improving the reliability of concurrent programs is a critical and urgent task. This talk presents recent work on understanding, detecting, and exposing concurrency bugs. I will first present two techniques that detect concurrency bugs from the angle of programmers' synchronization intention. The first one is AVIO (technology transfer to Intel). AVIO automatically infers programmers' atomicity intentions from correct execution. It detects violations to the inferred intentions and reports concurrency bugs. The second technique is MUVI. MUVI automatically infers variable correlation relationship from the source code and detects unsynchronized concurrent accesses to correlated variables. During this talk, I will also briefly discuss some findings from our characteristics study of real-world concurrency bugs. These findings have motivated the above bug detection work and inspired us to improve concurrent program testing. | ||||
| Flexible Task Graphs: A Unified Restricted Thread Programming Model for Java | ||||
| Jesper Honig Spring | On: | 29-Apr-2008 10:00 AM - 11:30 AM | ||
| EPFL | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
| Host: | Josh Auerbach | |||
Abstract: The disadvantages of unconstrained shared-memory multi-threading in Java have given rise to a variety of language extensions that place restrictions on how threads allocate, share, and communicate memory, leading to order-of-magnitude reductions in latency and jitter. Examples of such extensions include Eventrons (PLDI '06) and Exotasks (LCTES '07) from IBM Research, and Reflexes (VEE '07) and StreamFlex (OOPSLA '07) from Purdue University/EPFL. Each of these models makes different trade-offs with respect to expressiveness, efficiency, enforcement, and latency, and thus no single model is best suited for all applications scenarios. A common motivation for restricted thread programming models is real-time behavior. Recent advances in real-time garbage collection algorithms have reduced GC-related latency to around 1ms, but some applications have latency and throughput requirements that go beyond what can be achieved with current real-time garbage collection algorithms. For applications with sub-millisecond latency requirements, any synchronous interaction between real-time code and the GC or a time-oblivious task will cause a deadline miss. In this talk, we will present Flexible Task Graphs (Flexotasks), a research collaboration between IBM Research, Purdue University and EPFL. Flexotasks provide a restricted thread programming model that unifies the four previous models and allows different isolation policies and mechanisms to be combined in an orthogonal manner, making it possible to use the best suited combination to meet the specific applications needs. An article describing the work was accepted at LCTES '08 and will be presented at the conference in July. Note, however, this is not a preparatory talk | ||||
| Challenges and Approaches in Providing Quality of Service in Chip Multi-Processor Systems | ||||
| Prof. Yan Solihin | On: | 28-Apr-2008 10:00 AM - 11:30 AM | ||
| Associate Professor | At: | Watson Research Center (Hawthorne), Room GNF15 | ||
| NCSU | Host: | Erik Altman | ||
Abstract: The talk consists of two parts. The first part discusses the trend in increasing the number of cores on a chip in multicore architectures has produced new challenges in achieving scalable performance. We examine bandwidth as a source of scalability bottlenecks and show the relationship between cache size, bandwidth requirement, and the number of cores on a chip. We project the effectiveness of various bandwidth reduction techniques on improving the scalability of multicore designs. In the second part, we look at a problem related to the impact of sharing fine-grain platform resources among cores, for example the lowest level cache. We will show how different applications are affected by cache sharing. In particular, we will highlight the types and severity of pathological performance cases that can arise when applications run together on different cores but sharing the lowest level cache. The trends in enterprise IT toward service-oriented computing, server consolidation, and virtual computing point to a future in which workloads are becoming increasingly diverse in terms of performance, reliability, and availability requirements. In this environment, it is desirable to have microarchitecture and software support that can provide a guarantee of a certain level of performance (Quality of Service or QoS). We will present a framework for multicore architectures to fully provide QoS. We found that in addition to the ability to partition platform resources, a full QoS framework also needs an appropriate way to specify a QoS target, and an admission control policy that accepts jobs only when their QoS targets can be satisfied. We also found that providing strict QoS often leads to a significant reduction in throughput due to resource fragmentation. We will show throughput optimization techniques that include: (1) exploiting various QoS execution modes, and (2) a microarchitecture technique that steals excess resources from a job while still meeting its QoS target. Speaker biography: Yan Solihin is an associate professor at the Department of Electrical and Computer Engineering at North Carolina State University. He obtained his PhD from the University of Illinois at Urbana-Champaign in 2002. He is a recipient of 2006 IBM Faculty Partnership Award and 2004 NSF Faculty Early Career Award. He has graduated two PhD students and is currently advising eight PhD students. His research interests include parallel programming and parallel computer architectures, performance modeling, and architecture support for software reliability and computer security. | ||||
| Program Synthesis by Sketching | ||||
| Armando Solar-Lezama | On: | 21-Apr-2008 10:00 AM - 11:30 AM | ||
| UC Berkeley | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
| Host: | Vijay Saraswat | |||
Abstract: For over thirty years, software synthesis has promised to automate the chore of writing programs. But only recently, the power of modern computers and the growing maturity of verification technology have combined to make practical synthesis possible. One of the biggest challenges for practical synthesis is to establish a synergy between the synthesizer and the programmer. There is potential for synergy because, while the synthesizer needs human insight to produce acceptable implementations, programmers actually want control over the implementation strategy, so they want to be able to guide the synthesis process. Thus, both the programmer and the synthesizer benefit when programmers are allowed to provide insight in a natural way. Sketching is my answer to the challenges of practical synthesis. It is a form of synthesis whose key novelty is the use of partial programs (sketches) to communicate insight to the synthesizer. The talk will describe sketching as implemented in the SKETCH language, and the innovations in inductive synthesis that made sketching possible. The talk will also describe our experience using SKETCH to synthesize complex implementations of ciphers, scientific codes, and even concurrent lock-free data-structures. | ||||
| Cartesian computations and the high cost of moving data | ||||
| Larry Carter | On: | 15-Apr-2008 01:00 PM - 02:30 PM | ||
| Emeritus | At: | Watson Research Center (Hawthorne), Room GN-F15 (backup: 1S-F40) | ||
| UCSD | Host: | Bowen Alpern | ||
Abstract: In this talk, we identify and analyze a class of algorithms that includes many familiar and important scientific computations. A ""2-D Cartesian computation"" is characterized by having two very large data structures, A and B (perhaps A is the input and B the output), and for each suitably chosen chunk of A and chunk of B, there is a chunk of computation that must be performed. When neither A nor B fits in the fast memory of a computer, the time (or energy) needed to move bits between cores, chips, nodes and levels of the memory hierarchy can dominate the computation. Static Partitioning, Tiling, Inspector/Executor strategies, and Bucketizing are some well-known programming techniques that reduce data movement. We present a methodology that, for many Cartesian computations, allows one to decide which is the best of these techniques. Our results elegantly relate three orthogonal aspects of a computer -- computation speed, memory capacity, and communication or memory bandwidth -- and show that different techniques are needed at different levels of architectural granularity. Speaker biography: Larry Carter worked at as a Research Staff Member and manager at the Watson Research Center for nearly 20 years in the areas of probabilistic algorithms, compilers, VLSI testing, and high-performance computation. From 1994 to 2004, Dr. Carter was a professor in the Computer Science and Engineering Department of the University of California at San Diego. Between 1996 and 2000, he served as Vice Chair and then Chair of the department. His current research interests include scientific computation, performance programming, parallel computation, and computer architecture. Prof. Carter is a Senior Fellow at the San Diego Supercomputing Center, a Fellow of the IEEE, and a Professor Emeritus at UCSD. | ||||
| A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications | ||||
| Emina Torlak | On: | 14-Apr-2008 10:00 AM - 11:30 AM | ||
| MIT | At: | Watson Research Center (Hawthorne), Room GNF15 | ||
| Host: | Mandana Vaziri | |||
Abstract: Relational logic is an attractive candidate for a software description language, because both the design and implementation of software often involve reasoning about relational structures, whether in the problem domain (organizational structure, for example), in the high level design (architectural configurations, for example) or in low level code (graphs and linked lists). Until recently, however, frameworks for solving relational constraints (such as Alloy3) have had limited applicability. While powerful enough to analyze relatively small, hand-crafted models of software systems, current frameworks perform poorly on large and automatically generated specifications. In this talk, I will describe Kodkod, an efficient constraint solver for relational logic, with recent applications to design analysis, code checking, test-case generation, and declarative configuration. The Kodkod system includes a finite model finder and a minimal unsatisfiable core extractor, both based on SAT solving technology. I will present the key ideas and contributions behind these analyses, discuss how they compare to existing approaches, and conclude with an overview of future work. Speaker biography: Emina Torlak is a Ph.D. candidate in Computer Science at MIT. Her main research interests are in software engineering and lightweight formal methods. She is currently working on a scalable relational engine with applications to design analysis, code checking, test-case generation, and declarative configuration. Emina received her B.S. and M.Eng. in Computer Science from MIT. | ||||
| Synthesis of highly concurrent data structures | ||||
| Martin Vechev | On: | 10-Apr-2008 10:00 AM - 11:30 AM | ||
| IBM Research | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
Abstract: Highly concurrent algorithms are difficult to design, test, and verify. This motivates the need for systematic construction techniques. Unfortunately, existing universal construction techniques are not applicable for creating efficient practical algorithms. This leads to a myriad of problems: repeated effort per algorithm (both construction and verification), suboptimal and incorrect solutions, inability to differentiate inherent complexity from implementation complexity, and difficulties in adapting algorithms to new architectures are only a small sample. In this talk I will present some of the latest work we have done towards addressing these problems. I will show how starting from a sequential implementation, we construct a space of concurrent data structure algorithms, representing various design choices with different tradeoffs. Some of the algorithms we discover are novel and of practical value. In particular, one of the algorithms uses only the compare-and-swap (CAS) synchronization primitive, and provides a wait-free contains() operation. The current construction process combines manual steps that correspond to high-level insights with automatic exploration of implementation details. We have implemented the exploration procedure in a new tool called Paraglider | ||||
| Intel Architecture Memory Ordering | ||||
| Rick Hudson | On: | 3-Apr-2008 01:30 PM - 02:30 PM | ||
| Intel Research | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
| Host: | Maged Michael | |||
Abstract: Intel recently published more precise memory ordering principles for the IA32 and Intel Architecture 64 (aka x86) processors. This talk discusses the key principles embodied in this memory ordering and explains some of the software driven motivation behind them. Along the way we discuss issues such as publication safety and how to use the principles to implement the memory models found in high level programming languages. The presentation is aimed at developers of concurrent shared memory software and will provide a presentation of the principles as well as guidance on how to reason about them. This is joint work with Bratin Saha and many others both inside as well as outside Intel. Speaker biography: Richard L. Hudson is best known for his work in memory management including the invention of both the Train Algorithm and the Sapphire Algorithm. Richard joined Intel in 1998 where he has worked on memory management, concurrency, synchronization, and memory model related issues. He went to Shortridge, holds a B.A. degree from Hampshire College and an M.S. degree from the University of Massachusetts. | ||||
| All Patterns Great and Small | ||||
| Jason Smith | On: | 2-Apr-2008 10:00 AM - 11:30 AM | ||
| IBM Research | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
Abstract: Design patterns have proven to be a useful tool for describing and thinking about software design issues. Their abstract nature makes them appropriate for conceptual noodling, but difficult to work with on a concrete basis. In this talk I will describe a class of design patterns, the Elemental Design Patterns, that describe the lowest level of design issues available in programming, and illustrate how they form the basic language for design. In addition, I will discuss how these EDPs have a simple formal basis which makes them statically detectable in source code, as demonstrated by the System for Pattern Query and Recognition. SPQR is a semantic decompiler that efficiently detects instances of high-level design patterns in source code without human intervention by using EDPs as a core language, and applying simple inference techniques. By treating design patterns not as abstractions far removed from the foundations of programming language theory, but as a natural consequence of them, new opportunities for round-trip engineering and governance appear. | ||||
| Reasoning about Software in the Presence of Transient Faults | ||||
| Frances Perry | On: | 24-Mar-2008 10:30 AM - 12:00 PM | ||
| Princeton University | At: | Watson Research Center (Hawthorne), Room GN-K35 | ||
| Host: | John Field | |||
Abstract: A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. Although transient faults do not permanently damage the hardware, they may corrupt computations by altering stored values and signal transfers. Existing solutions can detect transient faults by duplicating computations and comparing the results, however these solutions lack any formal reasoning about their behavior. In this talk, I will show how to use low-level type systems to cleanly express invariants about redundant computations and to formally reason about code behavior, even when execution may be affected by transient faults. In particular, I will present a typed assembly language named TAL_FT and use it to prove that well-typed programs will always detect any single fault before the fault causes a change in the program output. | ||||
| Towers of Multicore: Concurrency, Synchronization, and Locality | ||||
| Vugranam Sreedhar | On: | 17-Mar-2008 10:00 AM - 11:30 AM | ||
| IBM Research | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
Abstract: Transitor growth in 2011 will reach over 32 Billion transitors. Massive multicore chips with over 500+ cores will soon become commodity processors. Killers applications continues to challenge massive multicore processing. In this talk I will present three Towers of Multicore: Concurrency, Synchronization, and Locality. To fully harness the power of massive multicore we have to climb the three towers in a careful and holistic manner. For the past four years I have worked with CAPSL group led by Prof. Guang Gao to address some of the challenges of massive multicore. One important observation is that computer architects, system software designers and application scientists must work closely together to address Concurrency, Synchronization, and Locality challenges in order to improve performance and scalability of large-scale applications (both regular and irregular applications). I will present some of our results in addressing these three challenges. | ||||
| Intelligent speculation for pipelined multithreading | ||||
| Neil Vachharajani | On: | 13-Mar-2008 10:00 AM - 11:30 AM | ||
| PhD Student | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
| Princeton University | Host: | Erik Altman | ||
Abstract: In recent years, microprocessor manufacturers have shifted their focus from single-core to multicore processors. To avoid burdening programmers with the responsibility of parallelizing their applications, some researchers have advocated automatic thread extraction. Within the scientific computing domain automatic parallelization techniques have been successful, but in the general purpose computing domain few, if any, techniques have achieved comparable success. Despite this, recent progress hints at mechanisms to unlock parallelism from general purpose applications. In particular, two promising proposals exist in the literature. The first, a group of techniques loosely classified as thread-level speculation (TLS), attempts to adapt techniques successful in the scientific domain, such as DOALL and DOACROSS parallelization, to the general purpose domain by using speculation to overcome complex control flow and data access patterns not easily analyzed statically. The second, a non-speculative technique called Decoupled Software Pipelining, partitions loops into long-running, fine-grained threads organized into a pipeline (pipelined multithreading or PMT). DSWP effectively extends the reach of conventional software pipelining to codes with complex control flow and variable latency operations. Unfortunately, both techniques suffer key limitations. TLS techniques either suffer from over speculation, in an attempt to speculatively transform a loop into a DOALL loop, or realize little parallelism in practice because DOACROSS parallelization puts core-to-core communication latency on the critical path. DSWP avoids these pitfalls with its pipeline organization and decoupled execution using inter-core communication queues. However, its non-speculative nature and restrictions needed to ensure a pipeline organization prevent DSWP from achieving balanced parallelism on many key application loops. In this talk, I present two key contributions that advance the state of automatic paralellization of general purpose applications. First, I propose extending pipelined multithreaded execution with intelligent speculation. Rather than speculating all loop-carried dependences to transform loops into DOALL loops, I propose speculating only key predictable dependences that inhibit balanced, pipelined execution. I will present results from our automatic compiler transformation, Speculative DSWP, demonstrating the efficacy of this technique. Second, to support decoupled speculative execution, I will describe an extension to a multi-core architecture's memory subsystem allowing it to support memory versioning. The proposed memory systems resemble those present in TLS architectures, but provide efficient execution in the presence of large transactions, many simultaneous outstanding transactions, and eager data forwarding between uncommitted transactions. In addition to supporting usage patterns exhibited by speculative pipelined multithreading, the proposed memory system facilitates existing and future speculative threading techniques. Speaker biography: Neil Vachharajani is a Ph.D. student in the Department of Computer Science at Princeton University. His research interests include compilers, computer architecture, and programming languages, particularly focused on concurrency and multi-core architectures. Neil is a NSF graduate fellow, has a BSE in Electrical Engineering from Princeton University, and a MA in Computer Science from Princeton University. | ||||
| Socio-Technical Studies of Open Source Projects | ||||
| Prem Devanbu and Christian Bird | On: | 12-Mar-2008 10:00 AM - 11:30 AM | ||
| UC-Davis | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
| Host: | Clay Williams | |||
Abstract: We have been studying the communication and collaboration patterns of open source software community members and the relationship between these activities and the structure of the technical artifact itself in the hope of understanding how large communities are able to operate and produce high quality software while facing many of the same organizational issues that their commercial counterparts also have to overcome. In this talk we present the results of two quantitative studies examining the social processes in OSS. In the first study we examine what factors lead to a project participant becoming a full fledged developer for the project. We find that significant factors include community social status, demonstration of technical expertise, and the amount of time spent participating in the community. In our second study we quantitatively evaluate the notion that OSS communities are bazaars with very little organizational structure. We observe that in large projects, task oriented teams within the social network organically emerge from the "chaos" and that the emergent organization of the teams is strongly related to the technical activities of the participants | ||||
| Experience using TIDE - a language independent debugging environment | ||||
| Jurgen Vinju | On: | 10-Mar-2008 10:00 AM - 11:30 AM | ||
| CWI; visitor at IBM until April 2008 | At: | Watson Research Center (Hawthorne), Room GN-K35 | ||
| Host: | Robert Fuhrer | |||
Abstract: In this talk I will report on the design and use of a generic debugging environment called TIDE. TIDE was designed and developed by Pieter Olivier in 2000 as a research experiment. It as since been used to construct debuggers for domain specific languages that have been implemented on different types of run-times | ||||
| Programming Language Design and Analysis Motivated by Hardware Evolution | ||||
| Prof. Alan Mycroft | On: | 3-Mar-2008 10:00 AM - 11:30 AM | ||
| Professor | At: | Watson Research Center (Hawthorne), Room GNF15 | ||
| Cambridge, UK | Host: | Frank Tip | ||
Abstract: Silicon chip design has passed a threshold whereby exponentially increasing transistor density (Moore's Law) no longer translates into increased processing power for single-processor architectures. Moore's Law now expresses itself as an exponentially increasing number of processing cores per fixed-size chip. We survey this process and its implications on programming language design and static analysis. Particular aspects addressed include the reduced reliability of ever-smaller components, the problems of physical distribution of programs and the growing problems of providing shared memory. Recent work centred on our C3D (Communication-Centric Computer Design) project http://www.cl.cam.ac.uk/research/comparch/research-c3d.html will also be surveyed for possible discussion afterward. Speaker biography: Alan Mycroft is Professor of Computing in the Computer Laboratory of Cambridge University where he leads the Cambridge Programming Research Group. He obtained a BA in Mathematics from Cambridge in 1977, followed by a PhD in Computer Science from Edinburgh in 1981. His research interests span an arc from semantic models of programming languages to actually building optimising compilers, but a constant theme has been language analysis and transformation for efficiency or correctness. Find out more at www.cl.cam.ac.uk/users/am or http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/m/Mycroft:Alan.html | ||||
| Cell GC: Using the Cell Synergistic Processor as a Garbage Collection Coprocessor | ||||
| Chen-Yong Cher | On: | 27-Feb-2008 02:00 PM - 03:00 PM | ||
| IBM Research | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
Abstract: This talk is based on a VEE'08 paper by Chen-Yong Cher and Michael Gschind. In recent years, scaling of single-core superscalar processor performance has slowed due to complexity and power considerations. To improve program performance, designs are increasingly adopting chip multiprocessing with homogeneous or heterogeneous CMPs. By trading off features from a modern aggressive superscalar core, CMPs often offer better scaling characteristics in terms of aggregate performance, complexity and power, but often require additional software investment to rewrite, retune or recompile programs to take advantage of the new designs. The Cell Broadband Engine is a modern example of a heterogeneous CMP with coprocessors (accelerators) which can be found in supercomputers (Roadrunner), blade servers (IBM QS20/21), and video game consoles (SCEI PS3). A Cell BE processor has a host Power RISC processor (PPE) and eight Synergistic Processor Elements (SPE), each consisting of a Synergistic Processor Unit (SPU) and Memory Flow Controller (MFC). In this work, we explore the idea of offloading Automatic Dynamic Garbage Collection (GC) from the host processor onto accelerator processors using the coprocessor paradigm. Offloading part or all of GC to a coprocessor offers potential performance benefits, because while the coprocessor is running GC, the host processor can continue running other independent, more general computations. We implement BDW garbage collection on a Cell system and offload the mark phase to the SPE co-processor. We show mark phase execution on the SPE accelerator to be competitive with execution on a full fledged PPE processor. We also explore object-based and block-based caching strategies for explicitly managed memory hierarchies, and explore to effectiveness of several prefetching schemes in the context of garbage collection. Finally, we implement Capitulative Loads using the DMA by extending software caches and quantify its performance impact on the coprocessor | ||||
| Experience in scalable SMMP systems software construction: Programming Language Aspects | ||||
| Jonathan Appavoo | On: | 26-Feb-2008 10:00 AM - 11:30 AM | ||
| IBM Research | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
Abstract: This talk will be broken into two parts. The first will be a brief review of the motivation, techniques, and practices we developed for the construction of scalable shared memory multiprocessor system software. These approaches were developed over several year spanning 3 OS project. The second half of the talk will be more informal and discuss how language features had a role to play in the construction of our systems that targeted scalable performance. | ||||
| From Dirt to Shovels: Fully Automatic Tool Generation from Ad Hoc Data | ||||
| Kenny Zhu | On: | 25-Feb-2008 10:00 AM - 11:30 AM | ||
| Post Doctoral Researcher | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
| Princeton University | Host: | Satish Chandra | ||
Abstract: An ad hoc data source is any semistructured data source for which useful data analysis and transformation tools are not readily available. Such data must be queried, transformed and displayed by systems administrators, computational biologists, financial analysts and hosts of others on a regular basis. In this work, we demonstrate that it is possible to generate a suite of useful data processing tools, including a semi-structured query engine, several format converters, a statistical analyzer and data visualization routines directly from the ad hoc data itself, without any human intervention. The key technical contribution of the work is a multiphase algorithm that automatically infers the structure of an ad hoc data source and produces a format specification in the PADS data description language. Programmers wishing to implement custom data analysis tools can use such descriptions to generate printing and parsing libraries for the data. Alternatively, our software infrastructure will push these descriptions through the PADS compiler, creating format-dependent modules that, when linked with format-independent algorithms for analysis and transformation, result in fully functional tools. We evaluate the performance of our inference algorithm, showing it scales linearly in the size of the training data and completes in seconds, as opposed to the hours or days it takes to write a description by hand. We also evaluate the correctness of the algorithm, demonstrating that generating accurate descriptions often requires less than 5% of the available data. This is joint work with Kathleen Fisher (AT&T Labs Research), David Walker (Princeton) and Peter White (Galois Inc.). A paper (POPL'08) is available here: http://www.cs.princeton.edu/~kzhu/papers/learningpopl08.pdf An online demo can be viewed off the PADS website: http://www.padsproj.org/cgi-bin/learning-demo.cgi Speaker biography: Kenny Zhu is a postdoctoral researcher at Princeton University. He graduated with Ph.D in Computer Science from National University of Singapore. He is primarily interested in programming languages and systems, distributed systems, and artificial intelligence. His current research is focused on the PADS ad-hoc data processing language. | ||||
| Discovering Heap Anomalies in the Wild | ||||
| Maria Jump | On: | 21-Feb-2008 10:00 AM - 11:30 AM | ||
| UT Austin | At: | Watson Research Center (Hawthorne), Room GN-F15 | ||
| Host: | Edith Schonberg | |||
Abstract: Despite the best efforts of programmers, programs still ship with bugs. Many of these bugs manifest as anomalies the heap. This talk discusses two low-overhead synergistic techniques for discovering heap anomalies by exploiting the underlying runtime system. The first, dynamic object sampling, is a technique for selectively tagging objects with characteristics. Summarization graphs provide a compact representation of collecting heap characteristics. We show that these techniques can stand alone or work together to provide ways to discover heap-based bugs with low enough overhead to consider using them in production systems. Speaker biography: Maria Jump is a Ph.D. Candidate in the Department of Computer Sciences at The University of Texas at Austin graduating in 2008. Her primary research interests are programming languages, compilers, runtime systems, and software reliability. Her dissertation work focuses on exploiting the runtime system of modern programming languages to increase software reliability. In her spare time, she enjoys hiking and the great outdoors. | ||||
| Turning Source Code Comments into Waypoints for Source Code Navigation | ||||
| Margaret-Anne Storey | On: | 30-Jan-2008 01:00 PM - 02:30 PM | ||
| Associate Professor | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
| University of Victoria | Host: | Harold Ossher | ||
Abstract: There exists a variety of user interface mechanisms that support navigation in software space, such as tree-based views, hypertext and search widgets A specific subset of these tools include mechanisms that support the user in defining personalized navigational structures over the software system. Personalized navigation structures include bookmarks, source code annotations, saved queries and source code comments. In our work, we have been investigating the advantages and limitations of the popular mechanisms in development environments for supporting navigation of annotations during software maintenance. This investigation led us to suggest a new approach for navigation called TagSEA (Tagging of Software Engineering Activities). TagSEA combines the notion of waypointing with social tagging. In this talk we present the TagSEA tool, as well as an extension of TagSEA called Tours, a presentation tool for programmers. We also report on a number of empirical studies to investigate how source code annotations are used to support the work practices of software engineers. Speaker biography: Dr. Margaret-Anne Storey is an associate professor of computer science at the University of Victoria, a Visiting Scientist at the IBM Centre for Advanced Studies in Toronto and a Canada Research Chair in Software and Knowledge Visualization. She is one of the principal investigators for CSER (Centre for Software Engineering Research in Canada) and an investigator for the National Center for Biomedical Ontology, US. Her research goal is to understand how technology can help people explore, understand and share complex information and knowledge. She applies and evaluates techniques from knowledge engineering, social software and visual interface design to applications such as collaborative software development, program comprehension, medical ontology development, and learning in web-based environments. | ||||
| No Ifs, Ands, or Buts: Uncovering the Simplicity of Conditionals | ||||
| Jonathan Edwards | On: | 23-Jan-2008 10:00 AM - 11:30 AM | ||
| MIT CSAIL | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
| Host: | Mandana Vaziri | |||
Abstract: Schematic tables are a new representation for conditionals. Roughly a cross between decision tables and data flow graphs, they represent computation and decision-making orthogonally. They unify the full range of conditional constructs, from if statements through pattern matching to polymorphic predicate dispatch. Program logic is maintained in a declarative canonical form that enforces completeness and disjointness among choices. Schematic tables can be used either as a code specification/generation tool, or as a self-contained diagrammatic programming language. They give program logic the clarity of truth tables, and support high-level direct manipulation of that logic, avoiding much of the mental computation demanded by conventional conditionals. Speaker biography: Jonathan Edwards is a Research Fellow with the Software Design Group at MIT CSAIL. He co-founded and was CTO of IntraNet. He worked on the type system of the Alloy 3 modeling language. Currently he is working on the non-textual programming language Subtext. His research goal is to better understand the creative act of programming, and to develop new languages and tools that facilitate it. | ||||
| Policies and Mechanisms for Secure Information Release | ||||
| Aslan Askarov | On: | 15-Jan-2008 10:00 AM - 11:30 AM | ||
| PhD Student | At: | Watson Research Center (Hawthorne), Room GNF15 | ||
| Chalmers University, Sweden | Host: | Marco Pistoia | ||
Abstract: Security assurance is an important challenge for modern computing. Intentional information release (declassification) is often crucial for such assurance. Security-critical systems demand expressive policies for information release that are beyond what conventional security models may offer. In this talk we discuss practical and theoretical aspects of information release. We start with a case study of implementation a declassification-intensive security protocol in a security-typed language. This, largest up to the publication date, case study suggests patterns for secure programming and demonstrates the multifaceted nature of declassification: from near-innocent relabeling of a ciphertext to dangerous release of secret keys. As confirmed by the case study, declassifications of encrypted data before sending it on a public channel are ubiquitous in security protocols. These declassifications are justified by the usage of strong encryption primitives and secret encryption keys. Next, we introduce cryptographically-masked flows that enable reasoning about information flow in the presence of encryption, decryption, and key generation. We propose a type system that enforces security for a small imperative language with cryptographic primitives, which prevents dangerous program behavior such as giving away a secret key or confusing keys and non-keys. This approach is exemplified with secure implementations of cryptographic protocols. To facilitate reasoning about released keys, we suggest an attacker-centric model of gradual release. The attacker's knowledge is modeled by the sets of possible secret inputs as functions of publicly observable events. Among the latter we distinguish special release events; the essence of gradual release is that the knowledge must remain constant between releases. Gradual release turns out to be a powerful foundation for release policies, which we demonstrate by formally connecting revelation-based and encryption-based declassification. We also show how gradual release can be enforced by security types and effects. As a next step in combining defense along different aspects of information release we present a combination of what and where information release policies. Moreover, we show that a minor modification of a security type system from the literature (which was designed for treating the what dimension) in fact enforces the combination of what and where policies. The talk is based on joint work with Andrei Sabelfeld and, in part, with Daniel Hedin. The corresponding papers have appeared in ESORICS'05, SAS'06, S&P'07, and PLAS'07. Speaker biography: Aslan Askarov is a PhD student working with Andrei Sabelfeld at the Department of Computer Science and Engineering at Chalmers University of Technology in Gothenburg, Sweden. His work focuses on practical and theoretical aspects of information release and programming language-based techniques for enforcement of information-flow policies. | ||||
| Toward a Practical Transactional Programming Model | ||||
| Prof. Michael Scott | On: | 14-Jan-2008 10:00 AM - 11:30 AM | ||
| Professor | At: | Watson Research Center (Hawthorne), Room GN-F15 | ||
| University of Rochester | Host: | Maged Michael | ||
Abstract: Over the past several years, researchers have developed an increasingly detailed understanding of both semantic issues and implementation options for transactional memory (TM). In the process, what started out as an attempt to simplify concurrent programming has begun to look disturbingly complex. Particularly thorny issues include how to accommodate lock-based libraries and irreversible operations (e.g., I/O); what to do when a propagating exception reaches the boundary of a transaction (particularly when transactions are nested); how to avoid transactional overhead on private accesses (without requiring the programmer to statically partition data and possibly code as well); how to move data back and forth between private and shared mode (the ""privatization problem""); and what to do about potentially concurrent accesses to the same data in private and shared mode. This talk will survey the current state of TM work at Rochester, with a focus on how TM researchers might hope to develop a programming model that accommodates (and reveals to expert programmers) the complexity we've been discovering, while retaining the simplicity (in the common case) that was our original motivation. Speaker biography: Michael L. Scott is a Professor of Computer Science and past Department Chair at the University of Rochester. He received his Ph.D. from the University of Wisconsin-Madison in 1985. His research interests span operating systems, languages, architecture, and tools, with a particular emphasis on parallel and distributed systems. He is best known for work in synchronization algorithms and concurrent data structures, in recognition of which he shared the 2006 SIGACT/SIGOPS Edsger W. Dijkstra Prize. Other widely cited work has addressed parallel operating systems and file systems, software distributed shared memory, and energy-conscious operating systems and microarchitecture. His textbook on programming language design and implementation (Programming Language Pragmatics, second edition, Morgan Kaufmann, Nov. 2005) has become a standard in the field. In 2003 he served as General Chair for SOSP; more recently he has been Program Chair for TRANSACT'07 and PPoPP'08. In 2001 he received the University of Rochester's Robert and Pamela Goergen Award for Distinguished Achievement and Artistry in Undergraduate Teaching. | ||||
| The TILE64 Processor: Architecture and Programming | ||||
| Richard Schooler | On: | 12-Dec-2007 02:00 PM - 03:30 PM | ||
| Software VP | At: | Watson Research Center (Hawthorne), Room GNF15 | ||
| Tilera | Host: | Evelyn Duesterwald | ||
Abstract: Tilera's TILE64 processor is a 64-core multicore system-on-chip, inspired by the MIT Raw architecture, and intended for high-performance embedded applications such as intelligent networking and digital multimedia. Speaker biography: Richard Schooler is VP of Software Engineering at Tilera Corp., responsible for system software including software development tools and operating system runtime software. Richard has worked for many years on high-performance systems, notably in compiler optimization and parallel systems. Previously-held positions include Director of Windows Build at Microsoft, CTO of InCert Software, Compiler Architect at Hewlett-Packard, and engineering positions at BB&N (commercializing the Butterfly parallel processor) and Intermetrics. | ||||
| Recent Developments in the Linux Kernel | ||||
| Theodore Tso | On: | 11-Dec-2007 02:00 PM - 03:30 PM | ||
| IBM Linux Technology Center | At: | Watson Research Center (Hawthorne), Room GNF15 | ||
| Host: | David Bacon | |||
Abstract: Ted will be discussing recent kernel developments, with an emphasis on real-time and ext4 features. Speaker biography: Ted is a leading Linux kernel developer and real-time Chief Engineering Manager, and is about to begin an assignment as a Linux Foundation Fellow and Chief Platform Strategist. | ||||
| Adventures in Extensibility -- Of Languages and Compilers | ||||
| Robert Grimm | On: | 30-Nov-2007 11:00 AM - 12:30 PM | ||
| Assistant Professor | At: | Watson Research Center (Hawthorne), Room GN-F15 | ||
| NYU | Host: | Martin Hirzel | ||
Abstract: Programming language technologies help reduce software complexity. But they are hard to realize, since compilers are complex systems themselves. To simplify compiler construction, the xtc project explores how to make languages and their compilers more easily extensible and to thus encourage the reuse of compiler components. This talk presents the resulting toolkit, which focuses on source-to-source transformers that translate extended languages to more basic versions. The xtc toolkit includes a parser generator, a type checker generator, and a code generator generator. I illustrate xtc with examples from the Jeannie language, which extends both Java and C by nesting Java and C code within each other at the level of individual statements and expressions. By fully combining the two languages' syntax and semantics, Jeannie eliminates verbose boiler-plate code, enables static error detection across the language boundary, and simplifies dynamic resource management. xtc makes this novel language composition practical, while also demonstrating the power of language technologies for reducing software complexity. Speaker biography: Robert Grimm received his B.S. and M.Eng. degrees from MIT and his PhD from the University of Washington. He is currently on the faculty at New York University. His research focuses on operating systems and distributed systems, using programming languages to improve both. | ||||
| Software Reliability Research at Microsoft | ||||
| Thomas Ball | On: | 28-Nov-2007 10:00 AM - 11:30 AM | ||
| Group Manager | At: | Watson Research Center (Hawthorne), Room GNF15 | ||
| Microsoft Research | Host: | Eran Yahav | ||
Abstract: I'll give a high-level overview of activities going on in the Software Reliability Research group and partner groups at Microsoft, including work on empirical software engineering, automatic test generation, and verification of sequential and concurrent programs. | ||||
| PyPy - automatic generation of VMs for dynamic languages - JIT included | ||||
| Laura Creighton, Armin Rigo, Samuele Pedroni, and Jacob Hallén | On: | 5-Nov-2007 10:00 AM - 11:30 AM | ||
| At: | Watson Research Center (Hawthorne), Room GN-F15 (backup: GN-K35) | |||
| Host: | Martin Hirzel | |||
Abstract: PyPy is a framework written in Python for generating virtual machines for dynamic languages. The VMs are flexibly produced from a high-level ""specification"" in the form of a simple interpreter for the dynamic language. The interpreters are written in a high-level static subset of Python. Low-level details like memory allocation and object layout and stack inspection are not encoded manually, but inserted by the VM generation process. This allows us to produce VMs that run within a wide range of execution environments (from C-like to JVM/.NET). The framework has the ability to automatically generate a dynamic compiler from the interpreter too. A pragmatic application of partial evaluation techniques guided by a few hints is used for the task. Crucial for the effectiveness of dynamic compilation is the use of run-time information to improve compilation results: in our approach, a powerful primitive called ""promotion"" that ""promotes"" run-time values to compile-time is used to that effect. | ||||
| Transactional Memory: From Semantics to Silicon | ||||
| Ali-Reza Adl-Tabatabai | On: | 1-Nov-2007 10:00 AM - 11:30 AM | ||
| Corporate Technology Group, Intel Corporation | At: | Watson Research Center (Hawthorne), Room 1SF40 | ||
| Host: | Evelyn Duesterwald | |||
Abstract: Multi-core architectures bring parallel programming into the mainstream. Parallel programming poses many new challenges to the developer, one of which is synchronizing concurrent access to shared memory by multiple threads. Programmers have traditionally used locks for synchronization, but locks have well-known pitfalls: Simplistic coarse-grained locking does not scale well, while more sophisticated fine-grained locking risks introducing deadlocks and data races. Furthermore, scalable libraries written using fine-grained locks cannot be easily composed in a way that retains scalability and avoids deadlock and data races. Transactional memory provides new synchronization constructs that alleviate many of the pitfalls of lock-based synchronization. In this talk, I will present our recent research on transactional memory. I will describe the transactional memory stack we have developed at Intel's programming systems lab. This stack includes new transactional memory language constructs for C and Java, compiler optimizations for these constructs, and high-performance transactional memory runtimes. I will also describe how hardware acceleration can improve the performance of transactional memory. Finally, I will discuss the challenges we face in bringing transactional memory into the mainstream. Speaker biography: Ali-Reza Adl-Tabatabai is a Senior Principal Engineer in Intel's Programming Systems Lab. He leads a team of researchers working on compilers and scalable runtimes for future Intel Architectures. Ali has spent most of his career building high-performance programming language implementations, including static and dynamic optimizing compilers and language runtime systems. His current research concentrates on language features that make it easier for the mainstream developer to build reliable and scalable parallel programs for future multi-core architectures and on architectural support for those features. Most recently he has worked on transactional memory, a new concurrency control mechanism that avoids many of the pitfalls of lock-based synchronization. Ali holds 13 patents and has published over 20 papers in leading conferences and journals. He received his PhD in Computer Science from Carnegie Mellon University. | ||||
| Roles and Relationships | ||||
| Prof. James Noble | On: | 29-Oct-2007 10:00 AM - 11:30 AM | ||
| Victoria University of Wellington, New Zealand | At: | Watson Research Center (Hawthorne), Room GNF15 | ||
| Host: | Mandana Vaziri | |||
Abstract: Relationships are well-known as a weak point in object-oriented modeling. In a UML diagram, a relationship or association can be drawn as a line connected two (or more) classes --- but implementing these relationships in OO programing languages s is rather more difficult. In this talk, I'll give a survey of approaches to designing relationships (including C# 3.0s LINQ), suggest a set of goals for relationship support, and present some potential directions for future work. (A version of this talk was an invited keynote at the ECOOP 2007 Workshop on Roles and Relationships in Object-Oriented Programming, Multiagent Systems, and Ontologies.) | ||||
| The State of the Heap, in Summary | ||||
| Nick Mitchell | On: | 19-Oct-2007 10:00 AM - 11:00 AM | ||
| Research Staff Member | At: | Watson Research Center (Hawthorne), Room GN-F15 | ||
| IBM Research | ||||
Abstract: The scale and complexity of Java heaps these days is a sight to behold. Or, better yet, it's a sight to behold carefully, and in small doses. Most servers require gigantic heaps in order to function, or meet performance goals. This seems to be a consequence of insufficient system support for memory management, poor guidance for policy decisions on caches and pools, bugs, and a distinct lack of appreciation for good data model and data structure design. We present our work on summarizing and visualizing graphs to facilitate memory-conscious design. I will explain how to infer interesting data structures from a graph; how the notion of backbones can be used to summarize data structures, and how we infer which data types serve the role of backbones; how shared ownership foils the dominator relation and our solution, the ownership graph; how to compare two graphs to track how a data structure changes within a run, and also throughout the development lifecycle; and, finally, how to determine whether a data structure is bloated, by distinguishing actual data from infrastructural overhead. All of this work has been automated, and is, principally, based on structural analysis of graphs. Our tool, Yeti, generates a summary of a 36 million object graph in about 6 minutes. This work has appeared in ECOOP 2003, ECOOP 2006, WODA 2007, and OOPSLA 2007. Speaker biography: Nick has been at IBM since 2000. He keeps busy with dynamic analysis tools, visualization, graph algorithms, the study of bloat, solving customer problems, and poking fun at benchmarks. He mostly enjoys literature, cats, and very long hikes. | ||||
| Probabilistic Calling Context | ||||
| Michael Bond | On: | 18-Oct-2007 10:30 AM - 12:00 PM | ||
| UT Austin | At: | Watson Research Center (Hawthorne), Room GN-K35 | ||
| Host: | Martin Hirzel | |||
Abstract: Growing software complexity (1) often makes whole-program static analysis and exhaustive testing infeasible and (2) limits developers' ability to have complete program knowledge. Due to these factors, programmers are turning to dynamic analyses to assist with programming understanding. Previous work shows that calling context enhances program understanding and dynamic analyses by providing a rich representation of program location. Compared to imperative programs, object-oriented programs use more interprocedural and less intraprocedural control flow, increasing the importance of context sensitivity for analysis. However, prior online methods for computing calling context, such as stack-walking or maintaining the current location in a calling context tree, are expensive in time and space. In this talk, I'll introduce a new online approach called probabilistic calling context (PCC) that continuously maintains a probabilistically unique value representing the current calling context. For millions of unique contexts, a 32-bit PCC value has few conflicts. Computing the PCC value adds 3% average overhead to a Java virtual machine. PCC is well-suited to clients that detect new or anomalous behavior since PCC values from training and production runs can be compared easily to detect new context-sensitive behavior; clients that query the PCC value at every system call, Java utility call, and Java API call add 0-9% overhead on average. PCC adds space overhead proportional to the distinct contexts stored by the client (one word per context). Our results indicate PCC is efficient and accurate enough to use in deployed software for residual testing, bug detection, and intrusion detection. I'll also present an online approach for diagnosing null and undefined value errors, called origin tracking. Both PCC and origin tracking will appear at OOPSLA 2007; both papers are available online: http://www.cs.utexas.edu/~mikebond/papers.html Speaker biography: Michael Bond is a fifth-year PhD student working with Kathryn McKinley at UT Austin. His work focuses on improving software reliability by detecting and tolerating bugs in deployed systems. | ||||
| Dependencies in Geographically Distributed Software Development: Overcoming the Limits of Modularity | ||||
| Marcelo Cataldo | On: | 17-Oct-2007 10:00 AM - 11:30 AM | ||
| Carnegie Melon University | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
| Host: | Clay Williams / Kate Ehrlich | |||
Abstract: Geographically distributed teams do better when their work is almost independent from each other. The modular design approach argues that by reducing the technical dependencies among modules, the work dependencies between teams developing interdependent modules are reduced. This argument assumes a simple and obvious relationship between the product structure and the structure of the tasks required to develop the product. However, in software development such relationship is not as simple as anticipated. Software modularization techniques use a subset of all technical dependencies. Consequently, identifying all relevant work dependencies is a challenge. In this presentation, I propose a method for determining work dependencies from multiple types of technical dependencies. The technique also assesses how those work dependencies are matched by the coordination activity carried out by developers. I define such relationship as congruence. Two empirical studies measured and assessed the impact of congruence on product quality and development productivity. Higher levels of congruence were associated with lower levels of customer defects. In addition, the amount of work dependencies associated with each developer had a detrimental effect to the quality of the system. The results also showed that higher levels of congruence were associated with higher levels of development productivity. Moreover, the most productive developers exhibited two distinct characteristics: they coordinated their work more congruently than less productive developers and they played a critical role in coordination across teams and geographical locations. Collectively, these results have important implications for the design of collaborative tools as well as for organizing GDSD teams. Speaker biography: Marcelo Cataldo is a doctoral candidate in the Institute for Software Research at Carnegie Mellon University’s School of Computer Science. His research interests are in geographically distributed software development and collaborative software engineering. Marcelo’s current research effort focuses on the development and empirical evaluation of mechanisms to measure socio-technical congruence and assess its impact on technical work. Marcelo received a BSc in Information Systems Engineering from Universidad Tecnólogica Nacional (Argentina) in 1996 and an MSc in Information Networking from Carnegie Mellon University in 2000. He also received an MSc in Computation, Organizations and Society from Carnegie Mellon University in 2007. | ||||
| Correcting the Dynamic Call Graph Using Control Flow Constraints | ||||
| Byeongcheol "BK" Lee | On: | 11-Oct-2007 10:30 AM - 12:00 PM | ||
| UT Austin | At: | Watson Research Center (Hawthorne), Room GNK35 | ||
| Host: | Kathryn McKinley | |||
Abstract: To reason about whole-programs, dynamic optimizers and analysis tools sample to collect a dynamic call graph. Sampling has not achieved high accuracy with low runtime overhead. As object-oriented programmers compose increasingly complex programs, inaccurate call graphs will inhibit analysis and optimizations. This talk demonstrates how to use static and dynamic control flow graph (CFG) constraints to improve the accuracy of the dynamic call graph (DCG). We introduce the frequency dominator (FDOM), a novel CFG relation that extends the dominator relation to expose static relative execution frequencies of basic blocks. We combine conservation of flow and dynamic CFG basic block profiles to further improve the accuracy of the DCG. Together these approaches add minimal overhead (1%) and achieve 85% accuracy compared to a perfect call graph for SPEC JVM98 and DaCapo benchmarks. Compared to sampling alone, accuracy improves by 12 to 36%. These results demonstrate that static and dynamic control-flow information offer accurate information for efficiently improving the DCG. Speaker biography: Byeongcheol (*BK*) Lee is a Ph.D student at The University of Texas at Austin working with Kathryn McKinley | ||||
| Programming Language Concepts for Malleable Software | ||||
| Prof. Bill Harrison | On: | 1-Oct-2007 11:00 AM - 12:30 PM | ||
| Professor | At: | Watson Research Center (Hawthorne), Room GN-F15 | ||
| Trinity College Dublin | Host: | Harold Ossher | ||
Abstract: Much of the software we write today embodies many logically unnecessary dependencies on other software it uses, and makes many latent presumptions about that software. When selecting a component for reuse, designers have in the past tended to chose a component implementation and then to build their use around its discovered or informally-expressed characteristics. But this is changing. One of the technological bases for service-oriented software is service-finding, the success of which depends on eliminating this kind of latent presumption, and it is time to re-examine how languages and middleware interact. It is the concept structure of the languages we use and the way they guide our use of them that lead to many undesirable characteristics. This talk illustrates some of the bad things our languages lead us to do, and describes concepts for a language that could allow the software we write to be more malleable in its use for components in modern systems. Speaker biography: Bill Harrison is an SFI Research Professor at Trinity College, Dublin, and a retired IBM Research Staff Member. His research career has included work in programming languages, compilers and optimization, and software development, and he was one of the original researchers behind what is now termed ""Aspect-Oriented Software Development"". He and his team at Trinity College are developing a programming language called ""Continuum"" as a test-bed for ideas in language features that encourage malleable software. | ||||
| Exploring Systems and Algorithms for Distributed Continuous Quality Assurance | ||||
| Prof. Adam Porter | On: | 24-Sep-2007 10:00 AM - 11:30 AM | ||
| Professor | At: | Watson Research Center (Hawthorne), Room GN-F15 | ||
| University of Maryland | Host: | Cemal Yilmaz | ||
Abstract: Software engineers increasingly emphasize agility and flexibility in their designs and development approaches. They increasingly use distributed development teams, rely on component assembly and deployment rather than green field code writing, rapidly evolve the system through incremental development and frequent updating, and use flexible product designs supporting extensive end-user customization. While agility and flexibility have many benefits, they also create an enormous number of potential system configurations built from rapidly changing component implementations. Since today's quality assurance (QA) techniques do not scale to handle highly configurable systems, we are developing and validating novel software QA processes and tools that leverage the extensive computing resources of user and developer communities in a distributed, continuous manner to significantly improve software quality. Speaker biography: Adam A. Porter is a professor with the Department of Computer Science, University of Maryland and is the Associate Director of the Institute for Advanced Computer Studies. He is a winner of a National Science Foundation CAREER Award and the Dean's Award for Teaching Excellence in the College of Computer, Mathematical and Physical Sciences at the University of Maryland. He is currently a member of the editorial board of the IEEE Transactions on Software Engineering and served previously on the editorial board of the ACM Transactions on Software Engineering and Methodology. He is a senior member of both the IEEE and ACM. His current research interests include empirical methods for identifying and eliminating bottlenecks in industrial development processes, experimental evaluation of fundamental software engineering hypotheses, and development of tools that demonstrably improve the software development process. | ||||
| Gedae | ||||
| Bill Lundgren and team | On: | 24-Sep-2007 10:00 AM - 12:00 PM | ||
| At: | Watson Research Center (Hawthorne), Room GNF15 | |||
| Host: | Eugen Schenfeld | |||
Abstract: Gedae is a productivity tool for multithreaded and multiprocessor application development which provides performance that often equals or exceeds hand-coded/hand-tuned implementations. The core of Gedae is its high level programming language, multithreading compiler and thread scheduler. The language is based on stream processing. While this stream-based programming model makes the language ideally suited to real-time applications with continuous data sources, the language has evolved from the basics of stream processing to include Gedae-specific concepts like stream segmentation that make it useful for any application, from small performance benchmarks to large, complex, deployed applications. The code created using the Gedae language is completely platform-independent. The platform-specific nature of the implementation is added through simple dialogs, and from these two components - the code and the implementation settings - the Gedae compiler generates threads of execution and manages all the issues involved in creating the multithreaded implementation on the target hardware, including planning the order of execution inside each thread, managing the concurrency between the threads, planning the memory (including heterogeneous memories), and vectorizing for highest efficiency (including optimizing for cache). Our salable product, built on top of this core technology, is a suite of tools. The tool suite is made up of a graphical editor for programming, dialogs for implementation specification and all of the analysis and debugging tools necessary for development. Included in this suite of debugging and analysis tools are features like the Trace Table for displaying timing information for each component in each thread in the multiprocessor implementation, debugging dialog for setting breakpoints and single stepping through each processor's execution, and memory maps for viewing the footprint during compilation and monitoring for problems during runtime. These tools can be used on all the targets Gedae supports, and Gedae targets a wide variety of multiprocessor, FPGA and multicore systems, including the Cell Broadband Engine processor, Intel Core Duo and other x86-based multicore processors, Power PC and TigerSHARC-based DSPs from vendors like Mercury and Curtiss-Wright, and a development kit is available to easily add support for new or proprietary platforms. Gedae has been used to develop real products on a variety of platforms, from a single Intel x86 processor to a custom multiboard DSP chassis with dozens of processors, and Gedae scales naturally to address architectures with even higher orders of magnitudes of processors. | ||||
| A Taste of SNOBOL | ||||
| Bard Bloom | On: | 21-Sep-2007 10:00 AM - 11:30 AM | ||
| IBM Research | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
Abstract: Can your favorite string pattern matching engine match:
| ||||
| Dynamic Bug Detection for Managed Languages | ||||
| Prof. Kathryn McKinley | On: | 20-Sep-2007 10:30 AM - 12:00 PM | ||
| Professor | At: | Watson Research Center (Hawthorne), Room GN-K35 | ||
| University of Texas, Austin | Host: | Martin Hirzel | ||
Abstract: Although managed languages preclude and help prevent some software errors, deployed programs still have errors and crash. In this talk, we discuss approaches for detecting bugs and making deployed software more reliable. Our work focuses on on-line techniques, and we present an approach for detecting data structures that are growing. We show how to piggyback on the garbage collector to summarize efficiently (in time and space) the heap by its type relations. Experimental results show this approach is effective at finding memory leaks, i.e., data structure errors of omission. We include a brief discussion of in progress work on tolerating leaks. These results indicate promise for inexpensive approaches that help programs run longer. Speaker biography: Kathryn McKinley is an IBM Academic Visitor and a professor at the University of Texas. Her research interests include compiler optimization, memory management, and software engineering. She now serves as the Editor-and-Chief of TOPLAS. She has graduated eight PhD students and is currently supervising eight graduate students. | ||||
| Tiptoe: A Compositional Real-Time Operating System | ||||
| Prof. Christoph Kirsch | On: | 13-Sep-2007 10:30 AM - 12:00 PM | ||
| Professor, Head of the Computational Systems Group | At: | Watson Research Center (Hawthorne), Room GN-K35 | ||
| U. Salzburg | Host: | Joshua Auerbach | ||
Abstract: This talk is about an open-source, hard real-time operating system called Tiptoe, which aims at providing a process model that is fully compositional and (constant-time) predictable in a temporal and spatial sense. The goal is to have Tiptoe processes read sensors, compute something, allocate and free memory, write actuators but also access disks and networks, all in real time, without affecting each others' real-time behavior. Moreover, the Tiptoe system is meant to predict in constant time remaining resource capacities such as the available memory and I/O bandwidth for end-to-end real-time guarantees on all relevant process activities. The strong temporal and spatial isolation of Tiptoe processes will enable more principled and scalable real-time and embedded software engineering. We have already obtained encouraging research results in our prototype implementation with a compositional and (constant-time) predictable, real-time memory management system, which, unlike existing approaches, also guarantees low bounds on memory fragmentation in real time. The talk will focus on the memory management but will also provide some general insight in the challenges of designing a compositional real-time operating system. Speaker biography: Christoph Kirsch received the Dr.Ing. degree from Saarland University, Saarbruecken, Germany, in 1999 while at the Max Planck Institute for Computer Science in Saarbruecken. He then worked as Postdoctoral Researcher at the Department of Electrical Engineering and Computer Sciences of the University of California, Berkeley. Since 2004, he is a full professor at the Department of Computer Sciences of the University of Salzburg, Austria. His research interests are in concurrent programming and systems, virtual execution environments, and embedded real-time software. Dr. Kirsch co-invented the Giotto and HTL languages, and leads the JAviator unmanned-aerial-vehicle project for which he recently received an IBM faculty award. He is a member of the ACM and IEEE, co-founded the ACM/SIGBED International Conference on Embedded Software (EMSOFT), chairs the Embedded Systems Week (ESWEEK) Organizing Committee, and is PC co-chair of EMSOFT in 2007. He has served on program committees of Coordination, DATE, EMSOFT, EuroSys, LCTES, OOPSLA, RTAS, and VEE. Christoph Kirsch received the Dr.Ing. degree from Saarland University, Saarbruecken, Germany, in 1999 while at the Max Planck Institute for Computer Science in Saarbruecken. He then worked as Postdoctoral Researcher at the Department of Electrical Engineering and Computer Sciences of the University of California, Berkeley. Since 2004, he is a full professor at the Department of Computer Sciences of the University of Salzburg, Austria. His research interests are in concurrent programming and systems, virtual execution environments, and embedded real-time software. Dr. Kirsch co-invented the Giotto and HTL languages, and leads the JAviator unmanned-aerial-vehicle project for which he recently received an IBM faculty award. He is a member of the ACM and IEEE, co-founded the ACM/SIGBED International Conference on Embedded Software (EMSOFT), chairs the Embedded Systems Week (ESWEEK) Organizing Committee, and is PC co-chair of EMSOFT in 2007. He has served on program committees of Coordination, DATE, EMSOFT, EuroSys, LCTES, OOPSLA, RTAS, and VEE. | ||||
| Enforcing and Validating User-Defined Programming Disciplines | ||||
| Prof. Todd Millstein | On: | 10-Sep-2007 10:00 AM - 11:30 AM | ||
| Assistant Professor | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
| UCLA | Host: | Frank Tip | ||
Abstract: One way that programmers manage the complexity of building and maintaining software systems is by adhering to "programming disciplines" of various sorts. For example, locking disciplines are used to prevent concurrency errors and ownership disciplines are used to enforce strong object encapsulation. While researchers have shown how to augment existing languages to statically enforce particular disciplines, language designers cannot anticipate all of the disciplines that programmers will want to employ. Therefore, it is desirable to allow programmers to specify and enforce their own disciplines. In this talk, I will describe an approach to supporting user-defined programming disciplines. The approach allows programmers to easily create new type annotations and to provide declarative rules that define the associated programming disciplines. These rules are then automatically enforced on programs statically. The approach also allows programmers to validate their programming disciplines against desired run-time invariants, thereby providing confidence in the correctness of the disciplines. Colleagues and I are exploring three instantiations of this approach: user-defined type qualifiers for C programs; user-defined type-and-effect systems; and "pluggable type systems" for Java. | ||||
| Expressive Declassification Policies and Modular Static Enforcement | ||||
| Prof. David Naumann | On: | 6-Sep-2007 10:30 AM - 12:00 PM | ||
| Associate Professor | At: | Watson Research Center (Hawthorne), Room GN-K35 | ||
| Stevens Institute of Technology | Host: | Marco Pistoia | ||
Abstract: This talk describes a way to specify expressive declassification policies, in particular, when, what, and where policies that include conditions under which downgrading is allowed. Secondly, an end-to-end semantic property is introduced, based on a model that allows observations of intermediate low states as well as termination. An attacker's knowledge only increases at explicit declassification steps, and within limits set by policy. Thirdly, practical means of enforcement is provided, by combining type-checking with program verification techniques applied to the small subprograms that carry out declassifications. Verification exploits a novel logic of regions. Joint work with Anindya Banerjee and Stan Rosenberg. Speaker biography: David Naumann is on the faculty of Computer Science at Stevens Institute of Technology and he chairs the Theory Panel of the Verified Software Initiative. His current research focus is on how to exploit established verification technologies for modular static analysis of security properties. His current musical focus is Rebetika. | ||||
| Blended Analysis for Performance Understanding of Framework-based Applications | ||||
| Barbara G. Ryder | On: | 29-Aug-2007 10:00 AM - 11:30 AM | ||
| Professor | At: | Watson Research Center (Hawthorne), Room GNF-15 | ||
| Rutgers University | Host: | Frank Tip | ||
Abstract: A new analysis paradigm, blended program analysis, enables practical, effective analysis of large framework-intensive Java applications for performance diagnosis. Blended analysis combines a dynamic representation of program calling structure with a static analysis applied to a region of that calling structure with observed performance problems. Performance ottlenecks stemming from overuse of temporary objects are common in these applications. A blended escape analysis, which approximates object effective lifetimes, will be presented with experiments demonstrating its utility in explaining the usage of newly created objects in a program region. A case study on the Trade benchmark shows how blended escape analysis helped to locate the single call path responsible for a performance problem involving objects created at 9 distinct sites and as far away as 6 levels of call, in a region which calls 223 distinct methods with a maximum call depth of 20. (This work is in collaboration with Bruno Dufour of Rutgers and Gary Sevitstky of IBM Research | ||||
| The IBM-Berkeley Collaborative Research in Programming Languages | ||||
| Ras Bodik | On: | 29-Aug-2007 11:00 AM - 12:00 PM | ||
| Associate Professor | At: | Watson Research Center (Hawthorne), Room GN F15 | ||
| UC Berkeley | Host: | Frank Tip | ||
Abstract: IBM's Open Collaborative Research (OCR) effort started last year as a pioneering example of tight-knit industry-academia collaboration whose results are open-sourced for the benefit of the entire community. Rutgers and Berkeley were the first two collaborators in programming languages. In this talk, I will first describe my group's recent OCR results, pointing out why OCR makes us approach the research differently. I will then try to infect you with our vision, hoping to draw more IBM collaborators into our plans. (After the talk, I volunteer to be similarly infected, of course.) I will talk about refinement pointer analysis and how it may change dynamically typed languages; about sketching-based synthesis and how it may change compiler design; and about incrementalization and how it may motivate programmers to provide specifications. | ||||
| Hardware Atomicity for Reliable Software Speculation | ||||
| Naveen Neelakantam | On: | 16-Aug-2007 10:00 AM - 11:30 AM | ||
| Graduate Student | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
| UIUC | Host: | Martin Hirzel | ||
Abstract: Speculative compiler optimizations are effective in improving both single-thread performance and reducing power consumption, but their implementation introduces significant complexity, which can limit their adoption, limit their optimization scope, and negatively impact the reliability of the compilers that implement them. To eliminate much of this complexity, as well as increase the effectiveness of these optimizations, we propose that microprocessors provide architecturally-visible hardware primitives for atomic execution. These primitives provide to the compiler the ability to optimize the program's hot path in isolation, allowing the use of non-speculative formulations of optimization passes to perform speculative optimizations. Atomic execution guarantees that if a speculation invariant does not hold, the speculative updates are discarded, the register state is restored, and control is transferred to a non-speculative version of the code, thereby relieving the compiler from the responsibility of generating compensation code. We demonstrate the benefit of hardware atomicity in the context of a Java virtual machine. We find incorporating the notion of atomic regions into an existing compiler intermediate representation to be natural, requiring roughly 3,000 lines of code (~3% of a JVM's optimizing compiler), most of which were for region formation. Its incorporation creates new opportunities for existing optimization passes, as well as greatly simplifying the implementation of additional optimizations (e.g. partial inlining, partial loop unrolling, and speculative lock elision). These optimizations reduce dynamic instruction count by 11% on average and result in a 12-15% average speedup, relative to a baseline compiler with a similar degree of inlining. | ||||
| Tortola: Addressing Tomorrow's Computing Challenges through Hardware/Software Symbiosis | ||||
| Prof. Kim Hazelwood | On: | 6-Aug-2007 10:00 AM - 11:30 AM | ||
| Assistant Professor | At: | Watson Research Center (Hawthorne), Room GN-F15 | ||
| University of Virginia | Host: | Peter Sweeney | ||
Abstract: The vast majority of research efforts in optimizing computer systems have targeted a single layer in the system stack: application code, operating systems, virtual machines, microarchitecture, or circuits. Yet, existing technology is reaching the limits of the solutions that can be provided by targeting a single layer in isolation. An important class of computing challenges is better suited for more holistic approaches. These challenges can be solved much more easily using reactive techniques, whereby the hardware can detect a problem, and a virtual execution environment (VEE) can use its global knowledge about the executing workload to correct the problem. In fact, this solution has the potential to outperform each of its constituent hardware-only or software-only solutions. We explore this potential by interjecting a virtualization layer between the application software and the underlying machine architecture. This virtual environment communicates bi-directionally with the microprocessor and operating system via feedback channels, allowing us to investigate combined hardware-software techniques for solving many future computing challenges. In this talk, I will motivate our notion of symbiotic program optimization, discuss various applications, and detail our experiences in solving the two modern issues using holistic techniques: the di/dt problem and heterogeneous multicore scheduling. Speaker biography: Kim Hazelwood is an Assistant Professor of Computer Science at the University of Virginia. Her research lies at the interface of compilers and computer architecture, where she focuses on virtual execution environments, their applications, and their implementation. Her recent work focuses on the notion of symbiotic optimization – using feedback from hardware and the OS to guide run-time code transformations. Prior to joining UVa in 2005, Kim was a post-doc with the Pin dynamic instrumentation team at Intel. She has also contributed to several dynamic optimization projects over the past ten years, including Dynamo, CarbonFire, DELI, DynamoRIO, and Jikes RVM. Kim received her Ph.D. from Harvard University in 2004, where she worked under the direction of Michael D. Smith. | ||||
| Abstract Error Projection | ||||
| Akash Lal | On: | 3-Aug-2007 10:00 AM - 11:30 AM | ||
| Graduate Student | At: | Watson Research Center (Hawthorne), Room GN-K35 | ||
| University of Wisconsin, Madison | Host: | Eran Yahav | ||
Abstract: In this paper, we extend model-checking technology with the notion of an error projection. Given a program abstraction, an error projection divides the program into two parts: the part outside the error projection is guaranteed to be correct, while the part inside the error projection can have bugs. Subsequent au- tomated or manual verification effort need only be concentrated on the part inside the error projection. We present novel algorithms for computing error projections using weighted pushdown systems that are sound and complete for the class of Boolean programs and discuss additional applications for these algorithms. | ||||
| Precise Enforcement of User-defined Security Policies | ||||
| Michael W. Hicks | On: | 30-Jul-2007 10:00 AM - 11:30 AM | ||
| Assistant Professor | At: | Watson Research Center (Hawthorne), Room GN-F15 | ||
| University of Maryland, College Park | Host: | Marco Pistoia | ||
Abstract: Existing security-oriented programming languages are highly specialized towards enforcing specific noninterference-like properties. In this paper, we define a new intermediate language that utilizes a dependent, substructural type system to ensure that user-defined custom security policies are properly enforced. Our approach has the following salient features: 1. A wide variety of security policies can be specified and provably enforced. We give example encodings of information flow, access control, downgrading, stack inspection and data provenance policies, and show, in general, how any safety property can be enforced. Each of these policies can be composed with others. 2. The form of the security labels and the policy language is user-defined. This allows our framework to interface with the rich body of work on policy languages. 3. The granularity of the security-relevant actions in the program is also user-defined. This permits the user to flexibly map policy level abstractions to program level elements, without arbitrarily choosing, say, functions, classes or modules to be the unit of program abstraction. Our approach stratifies programs into three layers: a high-level security policy that focuses on principals, privileges and trust relationships; a low-level policy in which the semantics of policy enforcement mechanism is made manifest; and the application program. We contend that this approach is an important contribution in its own right as it forms simple, understandable bridge from policy specifications to their enforcement. This is work-in-progress with my student, Nikhil Swamy Speaker biography: Michael W. Hicks is an assistant professor in the Computer Science department and UMIACS at the University of Maryland, College Park. His research focuses on using programming languages and analyses to improve the security, availability, and reliability of software. For the last several years he has developed several analyses and transformations that permit software to be updated while it runs, to fix bugs and security flaws, and to add new features. With his students, he developed Ginseng, a compiler and runtime system for C based on these ideas. His group has used Ginseng to successfully update several popular open source programs with dynamic patches based on three years' worth of actual releases. He has worked on several tools and languages toward improving the quality of C programs. He is a core designer and implementor of Cyclone, a safe C-like language for building systems software, with a focus on support for safe and efficient manual memory management to complement garbage collection. He also co-developed Locksmith, a static analysis tool for automatically proving the absence of data races in multi-threaded C programs. Most recently he co-developed C-Mod, a wrapper for the C compiler and linker that enforces safe practices for modular programming in C. He has recently begun to look at compiler and language-based solutions to software security problems. He is working on language-based techniques to ensure web-based applications enforce confidentiality and integrity policies by carefully considering administrative models. He is also looking at how to monitor operating system kernel integrity to detect malicious modifications. His approach is to develop checkable properties that focus on attacker goals and not on particular attack vectors. | ||||
| Compositional Verification and 3-Valued Abstractions Join Forces | ||||
| Sharon Shoham | On: | 25-Jul-2007 10:00 AM - 11:30 PM | ||
| PhD Candidate | At: | Watson Research Center (Hawthorne), Room 1S-F40 | ||
| Technion, Israel Institute of Technology | Host: | Eran Yahav | ||
Abstract: Two of the most promising approaches to fighting the state explosion problem in model checking are abstraction and compositional verification. In this work we join their forces to obtain a novel fully automatic compositional technique that can determine the truth value of the full mu-calculus with respect to a given system. Given a system M = M_1 || M_2, we view each component M_i as an abstraction \lifted{M_i} of the global system M. The abstract component \lifted{M_i} is defined using a 3-valued semantics so that whenever a mu-calculus formula \varphi has a definite value (true or false) on \lifted{M_i}, the same value holds also for M. Thus, \varphi can be checked on either \lifted{M_1} or \lifted{M_2} (or both), and if any of them returns a definite result, then this result holds also for M. If both checks result in an indefinite value, the composition of the components needs to be considered. However, instead of constructing the composition of \lifted{M_1} and \lifted{M_2}, our approach identifies and composes only the parts of the components in which their composition is necessary in order to conclude the truth value of \varphi. It ignores the parts which can be handled separately. The resulting model is often significantly smaller than the full system. We explain how our compositional approach can be combined with abstraction, in order to further reduce the size of the checked components. The result is an incremental compositional abstraction-refinement framework, which resembles automatic Assume-Guarantee reasoning. Joint work with Orna Grumberg (Technion). | ||||
| Games for Formal Design and Analysis of Reactive Systems | ||||
| Prof. Rajeev Alur | On: | 23-Jul-2007 10:00 PM - 11:30 AM | ||
| Zisman Family Professor, Graduate Group Chair | At: | Watson Research Center (Hawthorne), Room GN-F15 | ||
| University of Pennsylvania | Host: | Satish Chandra | ||
Abstract: This talk briefly reviews two-player games and their relevance to system analysis, and then describes 2 applications: ATL model checking for security protocols and interface synthesis for Java classes. | ||||
| Rational Build Forge - Product Overview & Strategy | ||||
| Leigh Williamson | On: | 19-Jul-2007 11:30 AM - 12:30 PM | ||
| IBM Rational | At: | Watson Research Center (Hawthorne), Room GN-F15 | ||
| Host: | Peter Santhanam | |||
Abstract: This presentation describes the recently acquired Build Forge product. The architecture for this mult | ||||