|
|
 |
About
|
Current practices for developing concurrent systems are rather
limited. Directly using low-level concurrency constructs is the
realm of experts, and is extremely error-prone. Generic
higher-level constructs (e.g., transactional memory) are
currently 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
and is potentially broken beyond repair.
As concurrent programming becomes prevalent, it is critical
that programmers are given better tools and methodologies for
developing concurrent systems. We propose a "radical"
alternative to existing approaches: generate provably correct
concurrent systems from higher-level specifications.
To obtain this goal, we have implemented a tool called PARAGLIDER that aids a designer in a systematic derivation process of fine-grained concurrent systems.
This project involves significant challenges in concurrency, verification, and related areas. If you are interested in an internship in this area, please contact us over e-mail (mtvechev@us.ibm.com, eyahav@us.ibm.com). |
Publications
| Deriving Linearizable Fine-Grained Concurrent
Objects Vechev M., Yahav E PLDI '08: ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation. [bib] [abstract][ps][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. [bib][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. [bib][abstract][ps][pdf][slides] |