Galois is pleased to host the following tech talk.
These talks are open to the interested public–please join us!
(There is no need to pre-register for the talk.)
Please note the unusual time for this talk, it is on Wednesday,
11 January 2012
title:
Model-based Code Generation and Debugging of Concurrent Programs
speaker:
Borzoo Bonakdarpour
time:
Wednesday, 11 January 2012, 10:30am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
Design and implementation of distributed systems often involve many subtleties due to their complex structure, non-determinism, and low atomicity as well as occurrence of unanticipated physical events such as faults. Thus, constructing correct distributed systems has always been a challenge and often subject to serious errors. We propose a method for generating distributed implementations from high-level component-based models that only employ simple synchronization primitives. The method is a sequence of three transformations preserving observational equivalence: (1) A transformation from a global state to a partial state model, (2) a transformation which replaces multi-party strong synchronization primitives in atomic components by point-to-point send/receive primitives based on asynchronous message passing, and (3) a final transformation to concrete distributed implementation based on platform and architecture. We study the properties of different transformations, in particular, performance criteria such as degree of parallelism and overhead for coordination.
The second part of the talk will focus on an automated technique for optimal instrumentation of multi-threaded programs for debugging and testing of concurrent data structures. We define a notion of observability that enables debuggers to trace back and locate errors through data-flow instrumentation. Observability in a concurrent program enables a debugger to extract the value of a set of desired variables through instrumenting another (possibly smaller) set of variables. We formulate an optimization problem that aims at minimizing the size of the latter set. Our experimental results on popular concurrent data structures (e.g., linked lists and red-black trees) show significant performance improvement in optimally-instrumented programs using our method as compared to ad-hoc over-instrumented programs.
bio:
Borzoo Bonakdarpour is currently a research assistant professor at the School of Computer Science at University of Waterloo, Canada. He was a post-doctoral researcher at the Verimag Laboratory, France, working on the BIP project led by the 2007 Turing Award recipient, Joseph Sifakis. The aim of the project is to develop theory, methods, and tools for building real-time and distributed systems consisting of heterogeneous components. His other research interests include runtime verification, compositional verification of embedded systems, model synthesis and, in particular, automated model repair. He is the main developer of the tool SYCRAFT which is capable of synthesizing fault-tolerant distributed programs of the size 10^80 reachable states and beyond. Borzoo Bonakdarpour obtained his Ph.D. from the Department of Computer Science and Engineering at Michigan State University in 2009. His Ph.D. dissertation, “Automated Revision of Distributed and Real-Time Programs”, studies a wide range of model repair problems in closed an open systems and was nominated for the 2010 ACM Doctoral Dissertation Award.