This project includes a technique and tool in which we
- Encode the semantics of relaxed consistency models operationally
- Using the encoding, from a relaxed transactional program program written in C, obtain a regular concurrent C program encoded with VCC annotations, such that verifying assertions and invariants in encoded program is equivalent to verifying them on program running under a relaxed consistency semantics
- Statically, using VCC, verify properties of relaxed transactional programs whose executions may not necessarily be serializable
QED consists of a proof system and a supporting tool for the static verification of concurrent programs. QED is a tool that mechanizes correctness proofs in the QED method. The QED method is a novel approach to verifying concurrent programs. QED runs on top of the Boogie system and uses the Z3 theorem prover. The tool is open source and available for download :
» more information on the QED project can be found at theorem.ku.edu.tr/QED
» download source code from qed.codeplex.com
Our research on race detection has been driven by our new lockset-based algorithm, called Goldilocks, for precisely computing the happens-before relation. This algorithm allowed us to detect data-races at runtime in a precise and efficient manner. Using the Goldilocks algorithm, we developed a race-aware Java runtime that throws a runtime exception called DataRaceException when a race is about to occur. In January 2009, the Goldilocks project appeared in the SIGPLAN CACM Research Highlights Nominations.
In this project our goal was to develop runtime verification tools for global correctness criteria for concurrent software. Among those are atomicity and refinement. Our research group developed a runtime verification tool prototype, Vyrd, for complex, highly concurrent software components. We used Vyrd to verify several industrial-scale software designs, including storage infrastructure software developed at Microsoft Research, a file system, and Java class libraries. Vyrd was able to find subtle errors in these systems that their developers were not aware of. We extended our prototype to a fully automated easy-to-use verification framework that also uses a model checker to verify the entire state space of the program.
Numerous runtime analysis tools are designed to observe the concurrency bugs in parallel programs (i.e. heisenbugs). Whereas the usability of these tools is hurt by their performance, slowdowns may reach several thousand times the application only run. Overhead of these tools can be divided to two tightly coupled jobs: tracing and analyzing. Simply put, we allow the parallel runtime analysis to run concurrently in another runtime.
» read more
Use of Software Transactional Memory, with hardware support, is a promising parallel programming paradigm. It can be used to separate conflict detection into a separate thread from normal application execution thread. As a result, both application and conflict detection execute in parallel. This improves performance of the application while maintaining data consistency.
» read more
VCC is a mechanical verifier for concurrent C programs. VCC takes a C program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries to prove these annotations correct. If it succeeds, VCC promises that your program actually meets its specifications.
» read more
Verifying STM Implementations
We are currently working on a hierarchical method for verifying implementations of software transactional memory. We will try to apply this method to verify Bartok STM. This approach is as follows: First, we will define correspondence between algorithm-level and implementation-level executions. Then, we will prove this correspondence between these two levels of executions.
» read more