IC Colloquium : Concurrent Data Representation Synthesis
Event details
| Date | 07.10.2013 |
| Hour | 16:15 › 17:30 |
| Speaker | Mooly Sagiv - School of Computer Science, Tel Aviv University |
| Location | |
| Category | Conferences - Seminars |
Abstract :
I will first describe our experience with testing composed concurrent Java operations which exposed many bugs in public domain software.
I will also describe two approaches avoiding these bugs. The first approach combines a simple compilation scheme with runtime synchronizations.
The second approach is completely static. We build a compiler that takes as input a program written using concurrent relations and synthesizes a representation of the relations as sets of cooperating data structures as well as the placement and acquisition of locks to synchronize concurrent access to those data structures. The resulting code is correct by construction: individual relational operations are implemented correctly and the aggregate set of operations is serializable and deadlock free. The relational specification also permits a high-level optimizer to choose the best performing of many possible legal data representations and locking strategies.
This is joint work with Alex Aiken, Nathan Bronson, and Peter Hawkins(Stanford University), Katleen Fisher(DARPA),
Guy Golan-Gueta, Ohad Shacham, and Ofri Ziv (Tel Aviv University), G. Ramalingam (Microsoft Research), Martin Rinard(MIT) and Eran Yahav (Technion)
Parts of this work appear in Petrer Hawkins thesis http://theory.stanford.edu/~hawkinsp/ (Honorable mention for the ACM doctoral dissertation award)
Bio:
Mooly Sagiv is Professor of Computer Science at Tel Aviv University. His research focuses on program analysis and verification, in particular reasoning about imperative programs manipulating dynamic data structures. His current work includes shape analysis and reasoning about software defined networks. Sagiv is a recipient of a 2013 senior ERC research grant for Verifying and Synthesizing Software Composition.
Sagiv was a visiting professor at UC Berkeley and Stanford University in 2010-2011, and was a Postdoc with Tom Reps at The University of Wisconsin in 1994-1995. He spent 3 years at IBM as a researcher after earning his PhD from the Technion Israel in 1991.
I will first describe our experience with testing composed concurrent Java operations which exposed many bugs in public domain software.
I will also describe two approaches avoiding these bugs. The first approach combines a simple compilation scheme with runtime synchronizations.
The second approach is completely static. We build a compiler that takes as input a program written using concurrent relations and synthesizes a representation of the relations as sets of cooperating data structures as well as the placement and acquisition of locks to synchronize concurrent access to those data structures. The resulting code is correct by construction: individual relational operations are implemented correctly and the aggregate set of operations is serializable and deadlock free. The relational specification also permits a high-level optimizer to choose the best performing of many possible legal data representations and locking strategies.
This is joint work with Alex Aiken, Nathan Bronson, and Peter Hawkins(Stanford University), Katleen Fisher(DARPA),
Guy Golan-Gueta, Ohad Shacham, and Ofri Ziv (Tel Aviv University), G. Ramalingam (Microsoft Research), Martin Rinard(MIT) and Eran Yahav (Technion)
Parts of this work appear in Petrer Hawkins thesis http://theory.stanford.edu/~hawkinsp/ (Honorable mention for the ACM doctoral dissertation award)
Bio:
Mooly Sagiv is Professor of Computer Science at Tel Aviv University. His research focuses on program analysis and verification, in particular reasoning about imperative programs manipulating dynamic data structures. His current work includes shape analysis and reasoning about software defined networks. Sagiv is a recipient of a 2013 senior ERC research grant for Verifying and Synthesizing Software Composition.
Sagiv was a visiting professor at UC Berkeley and Stanford University in 2010-2011, and was a Postdoc with Tom Reps at The University of Wisconsin in 1994-1995. He spent 3 years at IBM as a researcher after earning his PhD from the Technion Israel in 1991.
Links
Practical information
- General public
- Free
- This event is internal
Contact
- Host : Viktor Kuncak