Abstract: Atomicity is an important generic specification that assures that a programmer can pretend that blocks occur sequentially in any execution. We define a notion of atomicity based on causality. We model the control flow of a program with threads using a Petri net that naturally abstracts data, and faithfully captures the independence and interaction between threads. The causality between events in the partially ordered executions of the Petri net is used to define the notion of causal atomicity. We show that causal atomicity is a robust notion that many correct programs adopt, and show how we can effectively check causal atomicity using Petri net tools based on unfoldings, which exploit the concurrency in the net to yield automatic partial-order reduction in the state-space.
Azadeh Farzan
a post-doctoral researcher at the School of Computer
Science at Carnegie-Mellon University. She earned her B.S. degree in
computer engineering from Sharif University of Technology at Tehran
in 2000, and her Ph.D. in computer science from University of
Illinois at Urbana-Champaign in January 2007. Her research interests
are in the areas of software verification, concurrency, programming
languages and security.
Appointments: dcm@cs.cmu.edu |
Maintainer | [ Home > Seminar ] |
`Last modified: Mon Feb 26 11:09:10 EDT 2007 |