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.