Project

Back to overview

Practical Synthesis for Concurrent Systems

Applicant Vechev Martin
Number 141001
Funding scheme Project funding
Research institution Professur für Informatik ETH Zürich
Institution of higher education ETH Zurich - ETHZ
Main discipline Information Technology
Start/End 01.09.2012 - 31.03.2016
Approved amount 325'032.00
Show all

Keywords (4)

synthesis; analysis; concurrency; verification

Lay Summary (English)

Lead
Lay summary

All computers today embedded, mainstream, and high-end are being built using heterogeneous chips with an increasing number of processor cores. To effectively exploit these changes in technology, all future software will have to be concurrent. The fundamental difficulty in building reliable, robust and efficient concurrent programs arises from the fact that programmers must manually discover how to efficiently and correctly synchronize a potentially massive number of interfering parallel processes. Using too much synchronization leads to wasted hardware resources, while using too little synchronization leads to incorrect programs. Manually balancing this act is extremely difficult, error-prone and time consuming. Despite significant progress in the areas of automated program analysis, testing and verification, these approaches can only be applied after the software has already been written, and do not address the problem of helping programmers with tasks that arise during software construction, such as discovery of how to synchronize parallel threads.

The goal of this project is to develop new scalable tools and techniques that can automatically synthesize difficult and critical aspects of concurrent programs and even synthesize entire realistic concurrent algorithms. These techniques would enable programmers to focus on the core aspects of the application logic, while letting the tool deal with all of the low level details The proposal will attack the problem at multiple scales. We will develop and evaluate synthesis techniques targeting:

i) Large application level concurrent programs. The basic idea is to build a dynamic synthesizer that scales by leveraging dynamic information from counterexamples in order to iteratively repair a program. The dynamic synthesizer will operate as follows: after discovering a set of failing executions, the executions will be analyzed and possible repairs will be synthesized. The program is then repaired accordingly and further program paths are exercised which may in turn lead to more incorrect traces. Several key research innovations are required to make such a dynamic synthesis approach scale to realistic concurrent programs. First, an effective trace explorer is needed, one that aims to produce program paths leading to an error. Second, a trace analyzer will need to compute all possible ways in which the traces can be repaired. Here, the analyzer will need to deal with various heterogeneous synchronization mechanisms, optimality requirements, efficient encoding of repairs and with multiple optimal solutions. Finally, a realization phase will implement the possibly heterogeneous repairs, potentially obtaining multiple new optimal solutions: these can be realized either in the program (offline) or in the actual runtime (online).

ii) System-level concurrent algorithms. Highly-concurrent algorithms are a fundamental
part of today’s language runtimes, libraries and kernels. Current practices for developing
these algorithms are extremely error-prone and often lead to solutions that are either incorrect or inefficient. Instead, we propose to develop techniques that will automatically synthesize concurrent implementations of quality comparable or exceeding those produced by domain experts. In our approach, the designer will only express a sequential or a coarse-grained implementation, and the synthesizer will discover equivalent highly concurrent implementations. The enabling insight is that highly concurrent algorithms differ from their coarse-grained counterparts via carefully introduced observability that each process has about the actions of other processes. The key innovation in the synthesizer then will be how to automatically discover and express such fine-grained observability. If successful, these techniques will provide new insights towards breaking the synchronization barrier, and yield a procedure that will allow designers to quickly explore a massive space of possible implementations and even derive novel algorithms with minimal effort.
Direct link to Lay Summary Last update: 21.02.2013

Responsible applicant and co-applicants

Employees

Publications

Publication
Effective abstractions for verification under relaxed memory models
Dan Andrei, Meshman Yuri, Vechev Martin, Yahav eran (2015), Effective abstractions for verification under relaxed memory models, in Verification, Model Checking and Abstract Interpretation, Mumbai, India.
Predicting program properties from ”big code”.
Raychev Veselin, Vechev Martin, Krause Andreas (2015), Predicting program properties from ”big code”., in Principles of Programming Languages.
Scalable race detection for android applications
Bielik Pavol, Raychev Veselin, Vechev Martin (2015), Scalable race detection for android applications, in ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Pittsburgh.
Stateless model checking of event-driven applications.
Jensen Casper, Moller Anders, Raychev Veselin, Dimitrov Dimitar, Vechev Martin (2015), Stateless model checking of event-driven applications., in ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications.
Code completion with statistical language models
Raychev Veselin, Vechev Martin, Yahav Eran (2014), Code completion with statistical language models, in Programming Language Design and Implementation.
Synthesis of memory fences via refinement propagation
Meshman Yuri, Dan Andrei, Vechev Martin, Yahav Eran (2014), Synthesis of memory fences via refinement propagation, in Static Analysis Symposium.
Automatic Synthesis of Deterministic Concurrency
Raychev Veselin, Vechev Martin, Yahav Eran (2013), Automatic Synthesis of Deterministic Concurrency, in Static Analysis Symposium, Seattle, Washington.
Effective Race Detection for Event-Driven Programs
Raychev Veselin, Vechev Martin, Sridharan Manu (2013), Effective Race Detection for Event-Driven Programs, in ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Indianapolis, USA.
Predicate Abstraction for Relaxed Memory Models
Dan Andrei, Meshman Yuri, Vechev Martin, Yahav Eran (2013), Predicate Abstraction for Relaxed Memory Models, in Static Analysis Symposium, Seattle, Washington.
Modeling and analysis of remote memory access programming
Dan Andrei, Lam Patrick, Hoefler Torsten, Vechev Martin, Modeling and analysis of remote memory access programming, in ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Holland.

Collaboration

Group / person Country
Types of collaboration
Samsung Research United States of America (North America)
- Publication
Dr. Maged Michael (Facebook) United States of America (North America)
- Publication
Anders Moeller Denmark (Europe)
- Publication
Prof. Andreas Krause Switzerland (Europe)
- Publication
Prof. Eran Yahav (Technion) Israel (Asia)
- in-depth/constructive exchanges on approaches, methods or results
- Publication

Awards

Title Year
Facebook Faculty Award 2015
Outstanding Artifact Award, OOPSLA'13, for best system out of all accepted papers. 2013

Abstract

All computers today --- embedded, mainstream, and high-end --- are being built using heterogeneous chips with an increasing number of processor cores. To effectively exploit these changes in technology, all future software will have to be concurrent. The fundamental difficulty in building reliable, robust and efficient concurrent programs arises from the fact that programmers must manually discover how to efficiently and correctly synchronize a potentially massive number of interfering parallel processes. Using too much synchronization leads to wasted hardware resources, while using too little synchronization leads to incorrect programs. Manually balancing this act is extremely difficult, error-prone and time consuming.Despite significant progress in the areas of automated program analysis, testing and verification, these approaches can only be applied after the software has already been written, and do not address the problem of helping programmers with tasks that arise during software construction, such as discovery of how to synchronize parallel threads.The goal of this project is to develop new scalable tools and techniques that can automatically synthesize difficult and critical aspects of concurrent programs and even synthesize entire realistic concurrent algorithms. These techniques would enable programmers to focus on the core aspects of the application logic, while letting the tool deal with all of the low level details. The proposal will attack the problem at multiple scales. We will develop and evaluate synthesis techniques targeting:-- Large application level concurrent programs: the basic idea is to build a dynamic synthesizer that scales by leveraging dynamic information from counterexamples in order to iteratively repair a program. The dynamic synthesizer will operate as follows: after discovering a set of failing executions, the executions will be analyzed and possible repairs will be synthesized. The program is then repaired accordingly and further program paths are exercised which may in turn lead to more incorrect traces. Several key research innovations are required to make such a dynamic synthesis approach scale to realistic concurrent programs.First, an effective trace explorer is needed, one that aims to produce program paths leading to an error. Second, a trace analyzer will need to compute all possible ways in which the traces can be repaired. Here, the analyzer will need to deal with various heterogeneous synchronization mechanisms, optimality requirements, efficient encoding of repairs and with multiple optimal solutions. Finally, a realization phase will implement the possibly heterogeneous repairs, potentially obtaining multiple new optimal solutions: these can be realized either in the program (offline) or in the actual runtime (online).-- System-level concurrent algorithms: highly-concurrent algorithms are a fundamental part of today's language runtimes, libraries and kernels.Current practices for developing these algorithms are extremely error-prone and often lead to solutions that are either incorrect or inefficient. Instead, we propose to develop techniques that will automatically synthesize concurrent implementations of quality comparable or exceeding those produced by domain experts. In our approach, the designer will only express a sequential or a coarse-grained implementation, and the synthesizer will discover equivalenthighly concurrent implementations. The enabling insight is that highly concurrent algorithms differ from their coarse-grained counterparts via carefully introduced observability that each process has about the actions of other processes. The key innovation in the synthesizer then will be how to automatically discover and express such fine-grained observability. If successful, these techniques will provide new insights towards breaking the synchronization barrier, and yield a procedure that will allow designers to quickly explore a massive space of possible implementations and even derive novel algorithms with minimal effort.The research will contribute to the theory and practice of automated concurrency analysis and synthesis.
-