|
Navigation
Home People Publications |
 |
About
|
Current practices for developing concurrent systems are rather limited.
Manual constructions using low-level concurrency constructs (e.g. CAS) is the realm of experts,
is extremely error-prone and leads to significant non-repeatable effort in both the construction and the
verification process. Generic higher-level constructs (e.g., transactional memory) are also limited, and are not
clearly easier to use. Analytic techniques (e.g., race detection) only address a fraction of the problems, and can
only be applied after the code is written at which point it may be broken beyond repair.
The goal of the Paraglide project is to provide fundamental construction mechanisms and practical tools that assist
the designer in building both correct and efficient concurrent systems. Towards this, we have done constructions of
key and complex concurrent algorithms, starting from simple sequential implementations. To assist us in this process we have also
built a tool called PARAGLIDER. Using our techniques, we have obtained new and practical highly-concurrent algorithms.
This project involves significant challenges in concurrency, verification, and related areas. If you are interested in an internship, please contact us over e-mail: Martin Vechev (mtvechev@us.ibm.com) Eran Yahav (eyahav@us.ibm.com) |
Publications
Position Papers
| Computer-Assisted Construction of Efficient Concurrent Algorithms Vechev M., Yahav E., Michael M., Attiya H., Yorsh G. EC2: Exploiting Concurrency Efficiently and Correctly -- CAV 2008 Workshop to appear [pdf] |
Conference Publications
| Deriving Linearizable Fine-Grained Concurrent
Objects Vechev M., Yahav E PLDI '08: ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation. [pdf][slides] |
| CGCExplorer: A Semi-Automated Search Procedure for Provably
Correct Concurrent Collectors Vechev M., Yahav E., Bacon D.F., and Rinetzky N. PLDI '07: ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation. [abstract][ps][pdf][slides] |
| Correctness-Preserving Derivation of Concurrent Garbage Collection Algorithms Vechev M., Yahav E., and Bacon D.F. PLDI '06: ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation. [abstract][ps][pdf][slides] |
Talks
| Computer-assisted construction of linearizable algorithms. Workshop on the Verification of Concurrent Algorithms. Microsoft Research Cambridge, UK. 1st – 2nd May 2008. [slides] |