Find information:
[4-29]Relational Reasoning about Concurrent Program Transformation
Date:2011-04-22
Title: Relational Reasoning about Concurrent Program Transformation
Speaker: Xinyu Feng(冯新宇), USTC, Hefei, China
Time: 2:30pm, April 29th, 2011.
Venue: Lecture Room, Level 3, Building No. 5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract:
Verifying program transformations usually requires proving that the resulting program (the target) refines or is equivalent to the original one (the source). Simulations and logical relations are common techniques to prove the refinement relation.
However, the relation between individual sequential threads cannot be preserved in general with the presence of parallel compositions, due to instruction reordering and the different granularities of atomic operations at the source and the target.
On the other hand, the refinement relation defined based on fully abstract semantics of concurrent programs assumes arbitrary parallel environments, which is too strong and cannot be satisfied by many well-known transformations.
In this paper, we propose a relational reasoning method for compositional verification of concurrent program transformations. We define a simulation relation between the target and the source. The relation is parameterized with constraints of the environments that the source and the target programs may compose with.
It considers the interference between threads and their environments, thus less permissive than relations over sequential programs. It is compositional with respect to parallel compositions as long as the constraints are satisfied. Also, it does not require semantics preservation under all possible environments, and can incorporate the assumptions about environments made by specific program transformations in the form of rely and guarantee conditions.
We have used this relational reasoning approach to verify the atomicity of several fine-grained concurrent algorithms.
Verifying program transformations usually requires proving that the resulting program (the target) refines or is equivalent to the original one (the source). Simulations and logical relations are common techniques to prove the refinement relation.
However, the relation between individual sequential threads cannot be preserved in general with the presence of parallel compositions, due to instruction reordering and the different granularities of atomic operations at the source and the target.
On the other hand, the refinement relation defined based on fully abstract semantics of concurrent programs assumes arbitrary parallel environments, which is too strong and cannot be satisfied by many well-known transformations.
In this paper, we propose a relational reasoning method for compositional verification of concurrent program transformations. We define a simulation relation between the target and the source. The relation is parameterized with constraints of the environments that the source and the target programs may compose with.
It considers the interference between threads and their environments, thus less permissive than relations over sequential programs. It is compositional with respect to parallel compositions as long as the constraints are satisfied. Also, it does not require semantics preservation under all possible environments, and can incorporate the assumptions about environments made by specific program transformations in the form of rely and guarantee conditions.
We have used this relational reasoning approach to verify the atomicity of several fine-grained concurrent algorithms.
A short bio of speaker:
Xinyu Feng is Professor in Computer Science at University of Science and Technology of China (USTC). Before joining USTC, he got his PhD at Yale University in 2007, and worked as a research assistant professor at Toyota Technological Institute at Chicago from 2007 to 2010.
His research interest is in programming languages and formal program verification. In particular, he is interested in developing theories, programming languages and tools to build formally certified system software, with rigorous guarantees of safety and correctness.
Xinyu Feng is Professor in Computer Science at University of Science and Technology of China (USTC). Before joining USTC, he got his PhD at Yale University in 2007, and worked as a research assistant professor at Toyota Technological Institute at Chicago from 2007 to 2010.
His research interest is in programming languages and formal program verification. In particular, he is interested in developing theories, programming languages and tools to build formally certified system software, with rigorous guarantees of safety and correctness.